Version abc80222

abc.dsp

@@ -222,6 +222,10 @@ SOURCE=.\src\base\abci\abcDebug.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcDelay.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcDress.c
 # End Source File
 # Begin Source File
@@ -2962,6 +2966,10 @@ SOURCE=.\src\aig\aig\aigPart.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigPartReg.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigRepr.c
 # End Source File
 # Begin Source File

abc.rc

@@ -44,6 +44,7 @@ alias plat print_latch
 alias pio print_io
 alias pk print_kmap
 alias ps print_stats 
+alias psb print_stats -b
 alias psu print_supp
 alias psy print_symm
 alias pun print_unate
@@ -65,6 +66,7 @@ alias rvl read_verlib
 alias rsup read_super mcnc5_old.super
 alias rlib read_library
 alias rlibc read_library cadence.genlib
+alias rlut read_lut
 alias rw rewrite
 alias rwz rewrite -z
 alias rf refactor
@@ -104,7 +106,6 @@ alias choice      "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_r
 alias choice2     "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
 alias rwsat       "st; rw -l; b -l; rw -l; rf -l"
 alias rwsat2      "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l"
-alias shake       "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
 alias share       "st; multi -m; fx; resyn2"
 
 # resubstitution scripts for the IWLS paper

src/aig/aig/aig.h

@@ -519,6 +519,7 @@ extern void            Aig_ObjOrderAdvance( Aig_Man_t * p );
 /*=== aigPart.c =========================================================*/
 extern Vec_Ptr_t *     Aig_ManSupports( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManSupportsInverse( Aig_Man_t * p );
+extern Vec_Ptr_t *     Aig_ManSupportsRegisters( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
 extern Vec_Ptr_t *     Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
 extern Vec_Ptr_t *     Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );

src/aig/aig/aigDfs.c

@@ -46,11 +46,14 @@ void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
     assert( !Aig_IsComplement(pObj) );
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
+//    if ( Aig_ObjIsPi(pObj) )
+//        return;
 //    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
+    Aig_ObjSetTravIdCurrent(p, pObj);
     Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
     Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
-    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
-    Aig_ObjSetTravIdCurrent(p, pObj);
+//    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
+//    Aig_ObjSetTravIdCurrent(p, pObj);
     Vec_PtrPush( vNodes, pObj );
 }
 
@@ -113,7 +116,7 @@ Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Collects internal nodes in the DFS order.]
+  Synopsis    [Collects internal nodes and PIs in the DFS order.]
 
   Description []
                
@@ -125,14 +128,14 @@ Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p )
 Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
 {
     Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
+//    Aig_Obj_t * pObj;
     int i;
     assert( Aig_ManLatchNum(p) == 0 );
     Aig_ManIncrementTravId( p );
     // mark constant and PIs
     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
-    Aig_ManForEachPi( p, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
+//    Aig_ManForEachPi( p, pObj, i )
+//        Aig_ObjSetTravIdCurrent( p, pObj );
     // go through the nodes
     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
     for ( i = 0; i < nNodes; i++ )

src/aig/aig/aigPart.c

@@ -380,6 +380,58 @@ Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the register dependency matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManSupportsRegisters( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vSupports, * vMatrix;
+    Vec_Int_t * vSupp;
+    int iOut, iIn, k, m, i;
+    // get structural supports for each output
+    vSupports = Aig_ManSupports( p );
+    // transforms the supports into the latch dependency matrix
+    vMatrix = Vec_PtrStart( Aig_ManRegNum(p) );
+    Vec_PtrForEachEntry( vSupports, vSupp, i )
+    {
+        // skip true POs
+        iOut = Vec_IntPop( vSupp );
+        iOut -= Aig_ManPoNum(p) - Aig_ManRegNum(p);
+        if ( iOut < 0 )
+        {
+            Vec_IntFree( vSupp );
+            continue;
+        }
+        // remove PIs
+        m = 0;
+        Vec_IntForEachEntry( vSupp, iIn, k )
+        {
+            iIn -= Aig_ManPiNum(p) - Aig_ManRegNum(p);
+            if ( iIn < 0 )
+                continue;
+            assert( iIn < Aig_ManRegNum(p) );
+            Vec_IntWriteEntry( vSupp, m++, iIn );
+        }
+        Vec_IntShrink( vSupp, m );
+        // store support in the matrix
+        assert( iOut < Aig_ManRegNum(p) );
+        Vec_PtrWriteEntry( vMatrix, iOut, vSupp );
+    }
+    Vec_PtrFree( vSupports );
+    // check that all supports are used
+    Vec_PtrForEachEntry( vMatrix, vSupp, i )
+        assert( vSupp != NULL );
+    return vMatrix;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Start char-bases support representation.]
 
   Description []

src/aig/aig/module.make

@@ -12,6 +12,7 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigOper.c \
     src/aig/aig/aigOrder.c \
     src/aig/aig/aigPart.c \
+    src/aig/aig/aigPartReg.c \
     src/aig/aig/aigRepr.c \
     src/aig/aig/aigRet.c \
     src/aig/aig/aigRetF.c \

src/aig/cnf/cnfMan.c

@@ -223,7 +223,7 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
         return;
     }
     fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
-    fprintf( pFile, "p %d %d\n", p->nVars, p->nClauses );
+    fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
     for ( i = 0; i < p->nClauses; i++ )
     {
         for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )

src/aig/cnf/cnfMap.c

@@ -44,7 +44,8 @@ void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut, int * pAreaFlows )
     Aig_Obj_t * pLeaf;
     int i;
     pCut->Value = 0;
-    pCut->uSign = 100 * Cnf_CutSopCost( p, pCut );
+//    pCut->uSign = 100 * Cnf_CutSopCost( p, pCut );
+    pCut->uSign = 10 * Cnf_CutSopCost( p, pCut );
     Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
     {
         pCut->Value += pLeaf->nRefs;

src/aig/fra/fraHot.c

@@ -130,7 +130,7 @@ int Fra_OneHotNodesAreClause( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * p
 ***********************************************************************/
 Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
 {
-    int fSkipConstEqu = 0;
+    int fSkipConstEqu = 1;
     Vec_Int_t * vOneHots;
     Aig_Obj_t * pObj1, * pObj2;
     int i, k;

src/base/abc/abc.h

@@ -203,6 +203,7 @@ struct Abc_Ntk_t_
     void *            pData;         // misc
     Abc_Ntk_t *       pCopy;
     Hop_Man_t *       pHaig;         // history AIG
+    float *           pLutTimes;     // arrivals/requireds/slacks using LUT-delay model
     // node attributes
     Vec_Ptr_t *       vAttrs;        // managers of various node attributes (node functionality, global BDDs, etc)
 };
@@ -521,6 +522,7 @@ extern Abc_Obj_t *        Abc_AigXorLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Ab
 extern Abc_Obj_t *        Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * pT, Abc_Obj_t * pE, int * pType );
 extern Abc_Obj_t *        Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern Abc_Obj_t *        Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+extern Abc_Obj_t *        Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
 extern Abc_Obj_t *        Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs );
 extern void               Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel );
 extern void               Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
@@ -731,7 +733,7 @@ extern bool               Abc_NodeIsBuf( Abc_Obj_t * pNode );
 extern bool               Abc_NodeIsInv( Abc_Obj_t * pNode );    
 extern void               Abc_NodeComplement( Abc_Obj_t * pNode );
 /*=== abcPrint.c ==========================================================*/
-extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored );
+extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest );
 extern void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );

src/base/abc/abcAig.c

@@ -737,6 +737,22 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
     return Abc_AigOr( pMan, Abc_AigAnd(pMan, p0, Abc_ObjNot(p1)), 
                             Abc_AigAnd(pMan, p1, Abc_ObjNot(p0)) );
 }
+
+/**Function*************************************************************
+
+  Synopsis    [Implements Boolean XOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 )
+{
+    return Abc_AigOr( pMan, Abc_AigAnd(pMan, pC, p1), Abc_AigAnd(pMan, Abc_ObjNot(pC), p0) );
+}
  
 /**Function*************************************************************
 

src/base/abc/abcDfs.c

@@ -1031,7 +1031,7 @@ int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk )
   Synopsis    [Recursively detects combinational loops.]
 
   Description []
-               
+                
   SideEffects []
 
   SeeAlso     []

src/base/abc/abcNtk.c

@@ -1031,6 +1031,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Vec_PtrFree( pNtk->vAttrs );
     FREE( pNtk->pName );
     FREE( pNtk->pSpec );
+    FREE( pNtk->pLutTimes );
     free( pNtk );
 }
 

src/base/abci/abcDar.c

@@ -326,7 +326,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
-        if ( pTemp = pMan->pEquivs[pObj->Id] )
+        if ( (pTemp = pMan->pEquivs[pObj->Id]) )
         {
             Abc_Obj_t * pAbcRepr, * pAbcObj;
             assert( pTemp->pData != NULL );
@@ -1565,6 +1565,32 @@ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
     Aig_ManStop( pMan );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDarPartition( Abc_Ntk_t * pNtk )
+{
+    extern void Aig_ManRegPartitionRun( Aig_Man_t * pAig );
+    Aig_Man_t * pMan;
+
+    // convert to the AIG manager
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return;
+
+    Aig_ManRegPartitionRun( pMan );
+    Aig_ManStop( pMan );
+}
+
 
 
 #include "ntl.h"

src/base/abci/abcFpga.c

@@ -51,12 +51,13 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int
     Fpga_Man_t * pMan;
     Vec_Int_t * vSwitching;
     float * pSwitching = NULL;
+    int Num;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
     // print a warning about choice nodes
-    if ( Abc_NtkGetChoiceNum( pNtk ) )
-        printf( "Performing FPGA mapping with choices.\n" );
+    if ( (Num = Abc_NtkGetChoiceNum( pNtk )) )
+        printf( "Performing LUT mapping with %d choices.\n", Num );
 
     // compute switching activity
     fShowSwitching |= fSwitching;

src/base/abci/abcPrint.c

@@ -42,6 +42,66 @@ int s_ResynTime = 0;
 
 /**Function*************************************************************
 
+  Synopsis    [If the network is best, saves it in "best.blif" and returns 1.]
+
+  Description [If the networks are incomparable, saves the new network, 
+  returns its parameters in the internal parameter structure, and returns 1.
+  If the new network is not a logic network, quits without saving and returns 0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
+{
+    extern void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType );
+    static struct ParStruct {
+        char * pName;  // name of the best saved network
+        int    Depth;  // depth of the best saved network
+        int    Flops;  // flops in the best saved network 
+        int    Nodes;  // nodes in the best saved network
+        int    nPis;   // the number of primary inputs
+        int    nPos;   // the number of primary outputs
+    } ParsNew, ParsBest = { 0 };
+    // free storage for the name
+    if ( pNtk == NULL )
+    {
+        FREE( ParsBest.pName );
+        return 0;
+    }
+    // quit if not a logic network
+    if ( !Abc_NtkIsLogic(pNtk) )
+        return 0;
+    // get the parameters
+    ParsNew.Depth = Abc_NtkLevel( pNtk );
+    ParsNew.Flops = Abc_NtkLatchNum( pNtk );
+    ParsNew.Nodes = Abc_NtkNodeNum( pNtk );
+    ParsNew.nPis  = Abc_NtkPiNum( pNtk );
+    ParsNew.nPos  = Abc_NtkPoNum( pNtk );
+    // reset the parameters if the network has the same name
+    if ( ParsBest.pName == NULL || 
+         strcmp(ParsBest.pName, pNtk->pName) ||
+         ParsBest.Depth >  ParsNew.Depth || 
+         ParsBest.Depth == ParsNew.Depth && ParsBest.Flops >  ParsNew.Flops || 
+         ParsBest.Depth == ParsNew.Depth && ParsBest.Flops == ParsNew.Flops && ParsBest.Nodes >  ParsNew.Nodes )
+    {
+        FREE( ParsBest.pName );
+        ParsBest.pName = Extra_UtilStrsav( pNtk->pName );
+        ParsBest.Depth = ParsNew.Depth; 
+        ParsBest.Flops = ParsNew.Flops; 
+        ParsBest.Nodes = ParsNew.Nodes; 
+        ParsBest.nPis  = ParsNew.nPis; 
+        ParsBest.nPos  = ParsNew.nPos;
+        // writ the network
+        Io_Write( pNtk, "best.blif", IO_FILE_BLIF );
+        return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Print the vital stats of the network.]
 
   Description []
@@ -51,10 +111,13 @@ int s_ResynTime = 0;
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
+void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest )
 {
     int Num;
 
+    if ( fSaveBest )
+        Abc_NtkCompareAndSaveBest( pNtk );
+
 //    if ( Abc_NtkIsStrash(pNtk) )
 //        Abc_AigCountNext( pNtk->pManFunc );
 
@@ -220,6 +283,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 
 //    if ( Abc_NtkHasSop(pNtk) )
 //        printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) );
+   
 }
 
 /**Function*************************************************************

src/base/abci/module.make

@@ -9,6 +9,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcCut.c \
     src/base/abci/abcDar.c \
     src/base/abci/abcDebug.c \
+    src/base/abci/abcDelay.c \
     src/base/abci/abcDress.c \
     src/base/abci/abcDsd.c \
     src/base/abci/abcEspresso.c \

src/base/cmd/cmd.c

@@ -169,7 +169,7 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
 
     pAbc->TimeTotal += pAbc->TimeCommand;
     fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n",
-        (float)pAbc->TimeCommand / CLOCKS_PER_SEC, (float)pAbc->TimeTotal / CLOCKS_PER_SEC );
+        (float)(1.0 * pAbc->TimeCommand / CLOCKS_PER_SEC), (float)(1.0 * pAbc->TimeTotal / CLOCKS_PER_SEC) );
 /*
     {
         FILE * pTable;

src/base/main/mainInt.h

@@ -26,6 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "main.h"
+#include "port_type.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -60,8 +61,8 @@ struct Abc_Frame_t_
     FILE *          Err;
     FILE *          Hst;
     // used for runtime measurement
-    int             TimeCommand; // the runtime of the last command
-    int             TimeTotal;   // the total runtime of all commands
+    PORT_INT64_T    TimeCommand; // the runtime of the last command
+    PORT_INT64_T    TimeTotal;   // the total runtime of all commands
     // temporary storage for structural choices
     Vec_Ptr_t *     vStore;      // networks to be used by choice
     // decomposition package

src/misc/util/port_type.h

+// Portable Data Types
+
+#ifndef __PORT_TYPE__
+#define __PORT_TYPE__
+
+/**
+ * Pointer difference type; replacement for ptrdiff_t.
+ *
+ * This is a signed integral type that is the same size as a pointer.
+ *
+ * NOTE: This type may be different sizes on different platforms.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type PORT_PTRDIFF_T;
+#elif     defined(LIN64)
+typedef long PORT_PTRDIFF_T;
+#elif     defined(NT64)
+typedef long long PORT_PTRDIFF_T;
+#elif     defined(NT) || defined(LIN) || defined(WIN32)
+typedef int PORT_PTRDIFF_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+/**
+ * Unsigned integral type that can contain a pointer.
+ *
+ * This is an unsigned integral type that is the same size as a pointer.
+ *
+ * NOTE: This type may be different sizes on different platforms.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type PORT_PTRUINT_T;
+#elif     defined(LIN64)
+typedef unsigned long PORT_PTRUINT_T;
+#elif     defined(NT64)
+typedef unsigned long long PORT_PTRUINT_T;
+#elif     defined(NT) || defined(LIN) || defined(WIN32)
+typedef unsigned int PORT_PTRUINT_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+
+/**
+ * 64-bit signed integral type.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type PORT_INT64_T;
+#elif     defined(LIN64)
+typedef long PORT_INT64_T;
+#elif     defined(NT64) || defined(LIN)
+typedef long long PORT_INT64_T;
+#elif     defined(WIN32) || defined(NT)
+typedef signed __int64 PORT_INT64_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+#endif

src/opt/mfs/mfsCore.c

@@ -56,6 +56,7 @@ p->timeWin += clock() - clk;
     // compute the divisors of the window
 clk = clock();
     p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
+    p->nTotalDivs += Vec_PtrSize(p->vDivs);
 p->timeDiv += clock() - clk;
     // construct AIG for the window
 clk = clock();

src/opt/mfs/mfsDiv.c

@@ -253,7 +253,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
             if ( !Abc_ObjIsNode(pFanout) ) 
                 continue;
             // skip nodes with large level
-            if ( (int)pFanout->Level >= nLevDivMax )
+            if ( (int)pFanout->Level > nLevDivMax )
                 continue;
             // skip nodes whose fanins are not divisors
             Abc_ObjForEachFanin( pFanout, pFanin, m )

src/opt/mfs/mfsInt.h

@@ -83,6 +83,7 @@ struct Mfs_Man_t_
     int                 nMintsCare;
     int                 nMintsTotal;
     int                 nNodesBad;
+    int                 nTotalDivs;
     // node/edge stats
     int                 nTotalNodesBeg;
     int                 nTotalNodesEnd;

src/opt/mfs/mfsMan.c

@@ -115,8 +115,8 @@ void Mfs_ManPrint( Mfs_Man_t * p )
             p->nTotalEdgesBeg-p->nTotalEdgesEnd, 
             100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
         printf( "\n" );
-        printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n", 
-            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls );
+        printf( "Nodes = %d. Tried = %d. Resub = %d. Divs = %d. SAT calls = %d.\n", 
+            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls );
         if ( p->pPars->fSwapEdge )
             printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", 
                 p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );

src/opt/res/resDivs.c

@@ -109,7 +109,7 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
             if ( !Abc_ObjIsNode(pFanout) ) 
                 continue;
             // skip nodes with large level
-            if ( (int)pFanout->Level >= p->nLevDivMax )
+            if ( (int)pFanout->Level > p->nLevDivMax )
                 continue;
             // skip nodes whose fanins are not divisors
             Abc_ObjForEachFanin( pFanout, pFanin, m )