Version abc60407

abc.dsp

@@ -214,6 +214,10 @@ SOURCE=.\src\base\abci\abcFxu.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcGen.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcMap.c
 # End Source File
 # Begin Source File
@@ -262,6 +266,10 @@ SOURCE=.\src\base\abci\abcRewrite.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcRr.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcSat.c
 # End Source File
 # Begin Source File
@@ -282,6 +290,10 @@ SOURCE=.\src\base\abci\abcTiming.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcTrace.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcUnate.c
 # End Source File
 # Begin Source File
@@ -934,6 +946,10 @@ SOURCE=.\src\sat\asat\asatmem.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\asat\jfront.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\asat\solver.c
 # End Source File
 # Begin Source File
@@ -1310,6 +1326,10 @@ SOURCE=.\src\opt\cut\cutOracle.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\cut\cutPre22.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\cut\cutSeq.c
 # End Source File
 # Begin Source File
@@ -1738,6 +1758,10 @@ SOURCE=.\src\misc\extra\extraUtilReader.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\misc\extra\extraUtilTruth.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\misc\extra\extraUtilUtil.c
 # End Source File
 # End Group

abc.rc

@@ -14,6 +14,10 @@ set siswin sis.exe
 set sisunix sis
 set mvsiswin mvsis.exe
 set mvsisunix mvsis
+set capowin MetaPl-Capo10.1-Win32.exe
+set capounix MetaPl-Capo10.1
+set gnuplotwin wgnuplot.exe
+set gnuplotunix gnuplot
 
 # standard aliases
 alias b balance
@@ -60,6 +64,9 @@ alias st strash
 alias sw sweep
 alias ssw ssweep
 alias scl scleanup
+alias tr0 trace_start
+alias tr1 trace_check
+alias trt "r c.blif; st; tr0; b; tr1"
 alias u undo
 alias wb write_blif
 alias wl write_blif
@@ -84,10 +91,8 @@ alias shake       "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps;
 
 # resubstitution scripts for the IWLS paper
 alias src_rw      "st; rw -l; rwz -l; rwz -l" 
-alias src_rs1     "st; rs -K 6 -l; rs -K 9 -l; rs -K 12 -l" 
-alias src_rs2     "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" 
-alias src_rws1    "st; rw -l; rs -K 6 -l; rwz -l; rs -K 9 -l; rwz -l; rs -K 12 -l" 
-alias src_rws2    "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" 
+alias src_rs      "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" 
+alias src_rws     "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" 
 alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
 
 

examples/s444.blif

+.model s444
+.inputs G0 G1 G2
+.outputs G118 G167 G107 G119 G168 G108
+
+.latch     G11_in        G11  0
+.latch     G12_in        G12  0
+.latch     G13_in        G13  0
+.latch     G14_in        G14  0
+.latch     G15_in        G15  0
+.latch     G16_in        G16  0
+.latch     G17_in        G17  0
+.latch     G18_in        G18  0
+.latch     G19_in        G19  0
+.latch     G20_in        G20  0
+.latch     G21_in        G21  0
+.latch     G22_in        G22  0
+.latch     G23_in        G23  0
+.latch     G24_in        G24  0
+.latch     G25_in        G25  0
+.latch     G26_in        G26  0
+.latch     G27_in        G27  0
+.latch     G28_in        G28  0
+.latch     G29_in        G29  0
+.latch     G30_in        G30  0
+.latch     G31_in        G31  0
+
+.names G12 G13 [25]
+00 1
+.names G11 [25] [26]
+01 1
+.names G14 [26] [27]
+10 1
+.names G0 G11 [28]
+00 1
+.names [27] [28] G11_in
+01 1
+.names G11 G12 [30]
+11 1
+.names G12 [30] [31]
+10 1
+.names G11 [30] [32]
+10 1
+.names [31] [32] [33]
+00 1
+.names G0 [33] [34]
+00 1
+.names [27] [34] G12_in
+01 1
+.names G13 [30] [36]
+11 1
+.names G13 [36] [37]
+10 1
+.names [30] [36] [38]
+10 1
+.names [37] [38] [39]
+00 1
+.names G0 [39] [40]
+00 1
+.names [27] [40] G13_in
+01 1
+.names G12 G13 [42]
+11 1
+.names G11 [42] [43]
+11 1
+.names G14 [43] [44]
+11 1
+.names G14 [44] [45]
+10 1
+.names [43] [44] [46]
+10 1
+.names [45] [46] [47]
+00 1
+.names G0 [47] [48]
+00 1
+.names [27] [48] G14_in
+01 1
+.names G31 [27] [50]
+00 1
+.names G16 G17 [51]
+00 1
+.names G15 [51] [52]
+01 1
+.names [50] [52] [53]
+00 1
+.names G18 [53] [54]
+11 1
+.names G15 [50] [55]
+10 1
+.names G15 [55] [56]
+10 1
+.names [50] [55] [57]
+00 1
+.names [56] [57] [58]
+00 1
+.names G0 [58] [59]
+00 1
+.names [54] [59] G15_in
+01 1
+.names G16 [55] [61]
+11 1
+.names G16 [61] [62]
+10 1
+.names [55] [61] [63]
+10 1
+.names [62] [63] [64]
+00 1
+.names G0 [64] [65]
+00 1
+.names [54] [65] G16_in
+01 1
+.names G16 [50] [67]
+10 1
+.names G15 [67] [68]
+11 1
+.names G17 [68] [69]
+11 1
+.names G17 [69] [70]
+10 1
+.names [68] [69] [71]
+10 1
+.names [70] [71] [72]
+00 1
+.names G0 [72] [73]
+00 1
+.names [54] [73] G17_in
+01 1
+.names G15 G16 [75]
+11 1
+.names G17 [50] [76]
+10 1
+.names [75] [76] [77]
+11 1
+.names G18 [77] [78]
+11 1
+.names G18 [78] [79]
+10 1
+.names [77] [78] [80]
+10 1
+.names [79] [80] [81]
+00 1
+.names G0 [81] [82]
+00 1
+.names [54] [82] G18_in
+01 1
+.names G20 G21 [84]
+00 1
+.names G19 [84] [85]
+01 1
+.names [54] [85] [86]
+10 1
+.names G22 [86] [87]
+11 1
+.names G19 [54] [88]
+11 1
+.names G19 [88] [89]
+10 1
+.names [54] [88] [90]
+10 1
+.names [89] [90] [91]
+00 1
+.names G0 [91] [92]
+00 1
+.names [87] [92] G19_in
+01 1
+.names G20 [88] [94]
+11 1
+.names G20 [94] [95]
+10 1
+.names [88] [94] [96]
+10 1
+.names [95] [96] [97]
+00 1
+.names G0 [97] [98]
+00 1
+.names [87] [98] G20_in
+01 1
+.names G20 [54] [100]
+11 1
+.names G19 [100] [101]
+11 1
+.names G21 [101] [102]
+11 1
+.names G21 [102] [103]
+10 1
+.names [101] [102] [104]
+10 1
+.names [103] [104] [105]
+00 1
+.names G0 [105] [106]
+00 1
+.names [87] [106] G21_in
+01 1
+.names G19 G20 [108]
+11 1
+.names G21 [54] [109]
+11 1
+.names [108] [109] [110]
+11 1
+.names G22 [110] [111]
+11 1
+.names G22 [111] [112]
+10 1
+.names [110] [111] [113]
+10 1
+.names [112] [113] [114]
+00 1
+.names G0 [114] [115]
+00 1
+.names [87] [115] G22_in
+01 1
+.names G2 G23 [117]
+00 1
+.names G2 G23 [118]
+11 1
+.names [117] [118] [119]
+00 1
+.names G0 [119] G23_in
+01 1
+.names G20 G21 [121]
+01 1
+.names G0 G23 [122]
+01 1
+.names [121] [122] [123]
+11 1
+.names G19 [123] [124]
+01 1
+.names G21 G22 [126]
+10 1
+.names G19 G20 [125]
+10 1
+.names G23 [125] [127]
+01 1
+.names [126] [127] [128]
+11 1
+.names G0 G24 [129]
+01 1
+.names [128] [129] [130]
+01 1
+.names [124] [130] [131]
+00 1
+.names G22 G23 [132]
+00 1
+.names [125] [132] [133]
+11 1
+.names G24 [133] [134]
+10 1
+.names G19 G20 [135]
+00 1
+.names G23 [135] [136]
+11 1
+.names G22 G23 [137]
+11 1
+.names [136] [137] [138]
+00 1
+.names G0 G21 [139]
+01 1
+.names [138] [139] [140]
+11 1
+.names [134] [140] G25_in
+01 1
+.names G19 G22 [142]
+01 1
+.names G0 [142] [143]
+01 1
+.names G0 [108] [144]
+01 1
+.names [143] [144] [145]
+00 1
+.names [129] [139] [146]
+00 1
+.names [145] [146] G26_in
+11 1
+.names G21 G24 [148]
+00 1
+.names [125] [148] [149]
+11 1
+.names G21 G22 [150]
+00 1
+.names G24 [150] [151]
+01 1
+.names G0 [151] [152]
+00 1
+.names [149] [152] [153]
+01 1
+.names G0 G22 [154]
+01 1
+.names [135] [154] [155]
+11 1
+.names [146] [155] [156]
+10 1
+.names [131] [156] [157]
+00 1
+.names G17 [157] [158]
+01 1
+.names [131] [156] [159]
+10 1
+.names [158] [159] G28_in
+00 1
+.names [122] [126] [161]
+11 1
+.names G21 G22 [162]
+01 1
+.names G0 [162] [163]
+01 1
+.names [161] [163] [164]
+00 1
+.names G20 [164] [165]
+00 1
+.names G19 [165] [166]
+01 1
+.names [130] [166] [167]
+00 1
+.names [131] [167] [168]
+00 1
+.names G17 [168] [169]
+01 1
+.names [131] [167] [170]
+10 1
+.names [169] [170] G29_in
+00 1
+.names G20 G21 [172]
+10 1
+.names G0 G24 [173]
+00 1
+.names [172] [173] [174]
+11 1
+.names G19 [174] G30_in
+11 1
+.names G1 G31 [176]
+00 1
+.names G1 G31 [177]
+11 1
+.names [176] [177] [178]
+00 1
+.names G0 [178] G31_in
+01 1
+.names [131] G24_in
+0 1
+.names [153] G27_in
+0 1
+.names G27 G118
+1 1
+.names G29 G167
+0 1
+.names G25 G107
+1 1
+.names G28 G119
+0 1
+.names G30 G168
+1 1
+.names G26 G108
+1 1
+.end

src/base/abc/abc.h

@@ -154,6 +154,7 @@ struct Abc_Ntk_t_
     Abc_NtkFunc_t    ntkFunc;       // functionality of the network
     char *           pName;         // the network name
     char *           pSpec;         // the name of the spec file if present
+    int              Id;            // network ID
     // name representation 
     stmm_table *     tName2Net;     // the table hashing net names into net pointer
     stmm_table *     tObj2Name;     // the table hashing PI/PO/latch pointers into names
@@ -210,7 +211,7 @@ struct Abc_Ntk_t_
 // maximum/minimum operators
 #define ABC_MIN(a,b)      (((a) < (b))? (a) : (b))
 #define ABC_MAX(a,b)      (((a) > (b))? (a) : (b))
-#define ABC_INFINITY      (10000000)
+#define ABC_INFINITY      (100000000)
 
 // transforming floats into ints and back
 static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);               }
@@ -439,10 +440,10 @@ extern bool               Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 /*=== abcCollapse.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose );
+extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
 /*=== abcCut.c ==========================================================*/
-extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti );
-extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti );
+extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
+extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
 extern void               Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst );
 extern void *             Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
 extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
@@ -492,6 +493,8 @@ extern int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
 extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
+extern Abc_Ntk_t *        Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
+extern Abc_Ntk_t *        Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
 extern Abc_Ntk_t *        Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
 extern Abc_Ntk_t *        Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
 extern Abc_Ntk_t *        Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
@@ -554,7 +557,7 @@ extern Abc_Ntk_t *        Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk );
 /*=== abcNtbdd.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
 extern Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
-extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly );
+extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly, int fReorder, int fVerbose );
 extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcNtk.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
@@ -584,7 +587,7 @@ extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode,
 extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
 extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
 /*=== abcProve.c ==========================================================*/
-extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose );
+extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
 /*=== abcReconv.c ==========================================================*/
 extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
 extern void               Abc_NtkManCutStop( Abc_ManCut_t * p );
@@ -607,8 +610,8 @@ extern int                Abc_NodeRef_rec( Abc_Obj_t * pNode );
 extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
 extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
 /*=== abcSat.c ==========================================================*/
-extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose );
-extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFront, int fVerbose );
+extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
 extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
@@ -623,6 +626,7 @@ extern char *             Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
+extern char *             Abc_SopCreateMux( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateInv( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
 extern int                Abc_SopGetCubeNum( char * pSop );
@@ -672,6 +676,19 @@ extern void               Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
 extern void               Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
 extern int                Abc_NodeReadReverseLevel( Abc_Obj_t * pObj );
 extern int                Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj );
+/*=== abcTrace.c ==========================================================*/
+extern void               Abc_HManStart();
+extern void               Abc_HManStop();
+extern int                Abc_HManIsRunning();
+extern int                Abc_HManGetNewNtkId();
+extern void               Abc_HManAddObj( Abc_Obj_t * pObj );
+extern void               Abc_HManAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
+extern void               Abc_HManXorFaninC( Abc_Obj_t * pObj, int iFanin );
+extern void               Abc_HManRemoveFanins( Abc_Obj_t * pObj );
+extern void               Abc_HManAddProto( Abc_Obj_t * pObj, Abc_Obj_t * pProto );
+extern void               Abc_HManMapAddEqu( Abc_Obj_t * pObj, Abc_Obj_t * pEqu );
+extern int                Abc_HManPopulate( Abc_Ntk_t * pNtk );
+extern int                Abc_HManVerify( int NtkIdOld, int NtkIdNew );
 /*=== abcUtil.c ==========================================================*/
 extern void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );

src/base/abc/abcAig.c

@@ -807,6 +807,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
         Abc_AigAndDelete( pMan, pFanout );
         // remove the fanins of the old fanout
         Abc_ObjRemoveFanins( pFanout );
+        Abc_HManRemoveFanins( pFanout );
         // recreate the old fanout with new fanins and add it to the table
         Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
         assert( Abc_AigNodeIsAcyclic(pFanout, pFanout) );

src/base/abc/abcFanio.c

@@ -50,6 +50,7 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninR->vFanouts, pObj->Id    );
     if ( Abc_ObjIsComplement(pFanin) )
         Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
+    Abc_HManAddFanin( pObj, pFanin );
 }
 
 

src/base/abc/abcFunc.c

@@ -24,6 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define ABC_MUX_CUBES   100000
+
 static int         Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
 
 ////////////////////////////////////////////////////////////////////////
@@ -205,6 +207,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
 int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
 {
     Abc_Obj_t * pNode;
+    Extra_MmFlex_t * pManNew;
     DdManager * dd = pNtk->pManFunc;
     DdNode * bFunc;
     Vec_Str_t * vCube;
@@ -217,10 +220,8 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
 
     assert( Abc_NtkIsBddLogic(pNtk) ); 
     Cudd_zddVarsFromBddVars( dd, 2 );
-    // allocate the new manager
-    pNtk->pManFunc = Extra_MmFlexStart();
-    // update the network type
-    pNtk->ntkFunc = ABC_FUNC_SOP;
+    // create the new manager
+    pManNew = Extra_MmFlexStart();
 
     // go through the objects
     vCube = Vec_StrAlloc( 100 );
@@ -228,17 +229,30 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
     {
         assert( pNode->pData );
         bFunc = pNode->pData;
-        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode );
-        if ( pNode->pData == NULL )
+        pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode );
+        if ( pNode->pNext == NULL )
         {
+            Extra_MmFlexStop( pManNew, 0 );
+            Abc_NtkCleanNext( pNtk );
+//            printf( "Converting from BDDs to SOPs has failed.\n" );
             Vec_StrFree( vCube );
-            Cudd_Quit( dd );
             return 0;
         }
-        Cudd_RecursiveDeref( dd, bFunc );
     }
     Vec_StrFree( vCube );
 
+    // update the network type
+    pNtk->ntkFunc = ABC_FUNC_SOP;
+    // set the new manager
+    pNtk->pManFunc = pManNew;
+    // transfer from next to data
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Cudd_RecursiveDeref( dd, pNode->pData );
+        pNode->pData = pNode->pNext;
+        pNode->pNext = NULL;
+    }
+
     // check for remaining references in the package
     Extra_StopManager( dd );
     return 1;
@@ -339,6 +353,13 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
         assert( 0 );
     }
 
+    if ( nCubes > ABC_MUX_CUBES )
+    {
+        Cudd_RecursiveDerefZdd( dd, zCover );
+        printf( "The number of cubes exceeded the predefined limit (%d).\n", ABC_MUX_CUBES );
+        return NULL;
+    }
+
     // allocate memory for the cover
     if ( pMan )
         pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
@@ -468,6 +489,8 @@ void Abc_CountZddCubes_rec( DdManager * dd, DdNode * zCover, int * pnCubes )
         (*pnCubes)++;
         return;
     }
+    if ( (*pnCubes) > ABC_MUX_CUBES )
+        return;
     extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
     Abc_CountZddCubes_rec( dd, zC0, pnCubes );
     Abc_CountZddCubes_rec( dd, zC1, pnCubes );

src/base/abc/abcNetlist.c

@@ -62,7 +62,7 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pFanin)->pCopy );
     // collect the CO nodes
     Abc_NtkFinalize( pNtk, pNtkNew );
-    // fix the problem with CO pointing directing to CIs
+    // fix the problem with CO pointing directly to CIs
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     // duplicate EXDC 
     if ( pNtk->pExdc )
@@ -101,7 +101,8 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect )
     }
     else if ( Abc_NtkIsBddLogic(pNtk) )
     {
-        Abc_NtkBddToSop(pNtk, fDirect);
+        if ( !Abc_NtkBddToSop(pNtk, fDirect) )
+            return NULL;
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
         Abc_NtkSopToBdd(pNtk);
     }
@@ -157,7 +158,10 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
     assert( Abc_NtkLogicHasSimpleCos(pNtk) );
 
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk,0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk,0) )
+            return NULL;
+    }
 
     // start the netlist by creating PI/PO/Latch objects
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, pNtk->ntkFunc );

src/base/abc/abcNtk.c

@@ -50,6 +50,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     memset( pNtk, 0, sizeof(Abc_Ntk_t) );
     pNtk->ntkType     = Type;
     pNtk->ntkFunc     = Func;
+    pNtk->Id          = !Abc_HManIsRunning()? 0 : Abc_HManGetNewNtkId();
     // start the object storage
     pNtk->vObjs       = Vec_PtrAlloc( 100 );
     pNtk->vLats       = Vec_PtrAlloc( 100 );
@@ -136,6 +137,14 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
         Vec_PtrPush( pNtkNew->vCis, pObjNew );
         Vec_PtrPush( pNtkNew->vCos, pObjNew );
     }
+    if ( Abc_NtkIsStrash(pNtk) && Abc_HManIsRunning() )
+    {
+        Abc_HManAddProto( Abc_NtkConst1(pNtk)->pCopy, Abc_NtkConst1(pNtk) );
+        Abc_NtkForEachCi( pNtk, pObj, i )
+            Abc_HManAddProto( pObj->pCopy, pObj );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            Abc_HManAddProto( pObj->pCopy, pObj );
+    }
     // transfer the names
     Abc_NtkDupCioNamesTable( pNtk, pNtkNew );
     Abc_ManTimeDup( pNtk, pNtkNew );
@@ -407,6 +416,11 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
             Abc_ObjForEachFanin( pObj, pFanin, k )
                 Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     }
+    if ( Abc_NtkIsStrash(pNtk) && Abc_HManIsRunning() )
+    {
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            Abc_HManAddProto( pObj->pCopy, pObj );
+    }
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );

src/base/abc/abcObj.c

@@ -50,6 +50,8 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
     pObj->pNtk = pNtk;
     pObj->Type = Type;
     pObj->Id   = -1;
+    if ( pNtk->ntkType != ABC_NTK_NETLIST )
+        Abc_HManAddObj( pObj );
     return pObj;
 }
 

src/base/abc/abcSop.c

@@ -61,7 +61,7 @@ char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Creates the constant 1 cover with the given number of variables and cubes.]
 
   Description []
                
@@ -92,7 +92,7 @@ char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with 0 variables.]
+  Synopsis    [Creates the constant 1 cover with 0 variables.]
 
   Description []
                
@@ -108,7 +108,7 @@ char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with 0 variables.]
+  Synopsis    [Creates the constant 1 cover with 0 variables.]
 
   Description []
                
@@ -124,7 +124,7 @@ char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the AND2 cover.]
+  Synopsis    [Creates the AND2 cover.]
 
   Description []
                
@@ -147,7 +147,7 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input AND cover.]
+  Synopsis    [Creates the multi-input AND cover.]
 
   Description []
                
@@ -169,7 +169,7 @@ char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input NAND cover.]
+  Synopsis    [Creates the multi-input NAND cover.]
 
   Description []
                
@@ -191,7 +191,7 @@ char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input OR cover.]
+  Synopsis    [Creates the multi-input OR cover.]
 
   Description []
                
@@ -213,7 +213,7 @@ char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input OR cover.]
+  Synopsis    [Creates the multi-input OR cover.]
 
   Description []
                
@@ -238,7 +238,7 @@ char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input NOR cover.]
+  Synopsis    [Creates the multi-input NOR cover.]
 
   Description []
                
@@ -259,7 +259,7 @@ char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input XOR cover.]
+  Synopsis    [Creates the multi-input XOR cover.]
 
   Description []
                
@@ -276,7 +276,7 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input XOR cover (special case).]
+  Synopsis    [Creates the multi-input XOR cover (special case).]
 
   Description []
                
@@ -296,7 +296,7 @@ char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input XNOR cover.]
+  Synopsis    [Creates the multi-input XNOR cover.]
 
   Description []
                
@@ -313,7 +313,24 @@ char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the inv cover.]
+  Synopsis    [Creates the MUX cover.]
+
+  Description [The first input of MUX is the control. The second input
+  is DATA1. The third input is DATA0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateMux( Extra_MmFlex_t * pMan )
+{
+    return Abc_SopRegister(pMan, "11- 1\n0-1 1\n");
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the inv cover.]
 
   Description []
                
@@ -329,7 +346,7 @@ char * Abc_SopCreateInv( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the buf cover.]
+  Synopsis    [Creates the buf cover.]
 
   Description []
                

src/base/abci/abcAuto.c

@@ -51,7 +51,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
     int nOutputs, nInputs, i;
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL )
         return;
 
     // get information about the network

src/base/abci/abcBalance.c

@@ -29,6 +29,8 @@ static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode,
 static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate, bool fSelective );
 static int         Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate, bool fSelective );
 static void        Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk );
+static Vec_Ptr_t * Abc_NodeBalanceConeExor( Abc_Obj_t * pNode );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -227,6 +229,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
         return pNodeOld->pCopy;
     assert( Abc_ObjIsNode(pNodeOld) );
     // get the implication supergate
+//    Abc_NodeBalanceConeExor( pNodeOld );
     vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate, fSelective );
     if ( vSuper->nSize == 0 )
     { // it means that the supergate contains two nodes in the opposite polarity
@@ -260,6 +263,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
     assert( pNodeOld->pCopy == NULL );
     // mark the old node with the new node
     pNodeOld->pCopy = vSuper->pArray[0];
+    Abc_HManAddProto( pNodeOld->pCopy, pNodeOld );
     vSuper->nSize = 0;
     return pNodeOld->pCopy;
 }
@@ -351,6 +355,65 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst,
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeBalanceConeExor_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst )
+{
+    int RetValue1, RetValue2, i;
+    // check if the node occurs in the same polarity
+    for ( i = 0; i < vSuper->nSize; i++ )
+        if ( vSuper->pArray[i] == pNode )
+            return 1;
+    // if the new node is complemented or a PI, another gate begins
+    if ( !fFirst && (!pNode->fExor || !Abc_ObjIsNode(pNode)) )
+    {
+        Vec_PtrPush( vSuper, pNode );
+        return 0;
+    }
+    assert( !Abc_ObjIsComplement(pNode) );
+    assert( Abc_ObjIsNode(pNode) );
+    assert( pNode->fExor );
+    // go through the branches
+    RetValue1 = Abc_NodeBalanceConeExor_rec( Abc_ObjFanin0(Abc_ObjFanin0(pNode)), vSuper, 0 );
+    RetValue2 = Abc_NodeBalanceConeExor_rec( Abc_ObjFanin1(Abc_ObjFanin0(pNode)), vSuper, 0 );
+    if ( RetValue1 == -1 || RetValue2 == -1 )
+        return -1;
+    // return 1 if at least one branch has a duplicate
+    return RetValue1 || RetValue2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeBalanceConeExor( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vSuper;
+    if ( !pNode->fExor )
+        return NULL;
+    vSuper = Vec_PtrAlloc( 10 );
+    Abc_NodeBalanceConeExor_rec( pNode, vSuper, 1 );
+    printf( "%d ", Vec_PtrSize(vSuper) );
+    Vec_PtrFree( vSuper );
+    return NULL;
+}
+
 
 
 /**Function*************************************************************

src/base/abci/abcClpBdd.c

@@ -43,14 +43,14 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose )
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
 {
     Abc_Ntk_t * pNtkNew;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0, fReorder, fVerbose) == NULL )
         return NULL;
     if ( fVerbose )
         printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );

src/base/abci/abcCut.c

@@ -29,6 +29,9 @@
 static void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq );
 static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq );
 
+
+extern int nTotal, nGood, nEqual;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -46,6 +49,7 @@ static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq );
 ***********************************************************************/
 Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
 {
+    ProgressBar * pProgress;
     Cut_Man_t *  p;
     Abc_Obj_t * pObj, * pNode;
     Vec_Ptr_t * vNodes;
@@ -56,6 +60,8 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk );
     extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
 
+    nTotal = nGood = nEqual = 0;
+
     assert( Abc_NtkIsStrash(pNtk) );
     // start the manager
     pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
@@ -69,6 +75,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     // compute cuts for internal nodes
     vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs
     vChoices = Vec_IntAlloc( 100 );
+    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) );
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         // when we reached a CO, it is time to deallocate the cuts
@@ -81,8 +88,9 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
         // skip constant node, it has no cuts
         if ( Abc_NodeIsConst(pObj) )
             continue;
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
         // compute the cuts to the internal node
-        Abc_NodeGetCuts( p, pObj, pParams->fMulti );  
+        Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree );  
         // consider dropping the fanins cuts
         if ( pParams->fDrop )
         {
@@ -98,11 +106,16 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
             Cut_NodeUnionCuts( p, vChoices );
         }
     }
+    Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
     Vec_IntFree( vChoices );
 PRT( "Total", clock() - clk );
 //Abc_NtkPrintCuts_( p, pNtk, 0 );
 //    Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
+
+    // temporary printout of stats
+    if ( nTotal )
+    printf( "Total cuts = %d. Good cuts = %d.  Ratio = %5.2f\n", nTotal, nGood, ((double)nGood)/nTotal );
     return p;
 }
 
@@ -276,14 +289,14 @@ printf( "Converged after %d iterations.\n", nIters );
   SeeAlso     []
 
 ***********************************************************************/
-void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti )
+void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
 {
     void * pList;
     if ( pList = Abc_NodeReadCuts( p, pObj ) )
         return pList;
-    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fMulti );
-    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fMulti );
-    return Abc_NodeGetCuts( p, pObj, fMulti );
+    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fDag, fTree );
+    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fDag, fTree );
+    return Abc_NodeGetCuts( p, pObj, fDag, fTree );
 }
 
 /**Function*************************************************************
@@ -297,14 +310,28 @@ void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti )
   SeeAlso     []
 
 ***********************************************************************/
-void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti )
+void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
 {
-//    int fTriv = (!fMulti) || pObj->fMarkB;
-    int fTriv = (!fMulti) || (pObj->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pObj));
+    Abc_Obj_t * pFanin;
+    int fDagNode, fTriv, TreeCode = 0;
     assert( Abc_NtkIsStrash(pObj->pNtk) );
     assert( Abc_ObjFaninNum(pObj) == 2 );
+    // check if the node is a DAG node
+    fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj));
+    // increment the counter of DAG nodes
+    if ( fDagNode ) Cut_ManIncrementDagNodes( p );
+    // add the trivial cut if the node is a DAG node, or if we compute all cuts
+    fTriv = fDagNode || !fDag;
+    // check if fanins are DAG nodes
+    if ( fTree )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        TreeCode |=  (Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin));
+        pFanin = Abc_ObjFanin1(pObj);
+        TreeCode |= ((Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin)) << 1);
+    }
     return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
-        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv );  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv, TreeCode );  
 }
 
 /**Function*************************************************************

src/base/abci/abcDsd.c

@@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
     assert( Abc_NtkIsStrash(pNtk) );
 
     // perform FPGA mapping
-    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL )
         return NULL;
     if ( fVerbose )
         printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );

src/base/abci/abcEspresso.c

@@ -54,7 +54,13 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose )
     if ( Abc_NtkHasMapping(pNtk) )
         Abc_NtkUnmap(pNtk);
     else if ( Abc_NtkHasBdd(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return;
+        }
+    }
     // minimize SOPs of all nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( i ) Abc_NodeEspresso( pNode );

src/base/abci/abcFraig.c

@@ -684,7 +684,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
         // set the number of networks stored
         Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 );
     }
-    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
+//    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
     return 1;
 }
 

src/base/abci/abcFxu.c

@@ -57,7 +57,13 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
     if ( Abc_NtkIsMappedLogic(pNtk) )
         Abc_NtkUnmap(pNtk);
     else if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return 0;
+        }
+    }
     else
     { // to make sure the SOPs are SCC-free
 //        Abc_NtkSopToBdd(pNtk);

src/base/abci/abcGen.c

+/**CFile****************************************************************
+
+  FileName    [abc_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+void Abc_WriteLayer( FILE * pFile, int nVars, int fSkip1 );
+void Abc_WriteComp( FILE * pFile );
+void Abc_WriteFullAdder( FILE * pFile );
+
+void Abc_GenAdder( char * pFileName, int nVars );
+void Abc_GenSorter( char * pFileName, int nVars );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenAdder( char * pFileName, int nVars )
+{
+    FILE * pFile;
+    int i;
+
+    assert( nVars > 0 );
+
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# %d-bit ripple-carry adder generated by ABC on %s\n", nVars, Extra_TimeStamp() );
+    fprintf( pFile, ".model Adder%02d\n", nVars );
+
+    fprintf( pFile, ".inputs" );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " a%02d", i );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " b%02d", i );
+    fprintf( pFile, "\n" );
+
+    fprintf( pFile, ".outputs" );
+    for ( i = 0; i <= nVars; i++ )
+        fprintf( pFile, " y%02d", i );
+    fprintf( pFile, "\n" );
+
+    fprintf( pFile, ".names c\n" );
+    if ( nVars == 1 )
+        fprintf( pFile, ".subckt FA a=a00 b=b00 cin=c s=y00 cout=y01\n" );
+    else
+    {
+        fprintf( pFile, ".subckt FA a=a00 b=b00 cin=c s=y00 cout=%02d\n", 0 );
+        for ( i = 1; i < nVars-1; i++ )
+            fprintf( pFile, ".subckt FA a=a%02d b=b%02d cin=%02d s=y%02d cout=%02d\n", i, i, i-1, i, i );
+        fprintf( pFile, ".subckt FA a=a%02d b=b%02d cin=%02d s=y%02d cout=y%02d\n", i, i, i-1, i, i+1 );
+    }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" );
+
+    Abc_WriteFullAdder( pFile );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenSorter( char * pFileName, int nVars )
+{
+    FILE * pFile;
+    int i, k, Counter, nDigits;
+
+    assert( nVars > 1 );
+
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# %d-bit sorter generated by ABC on %s\n", nVars, Extra_TimeStamp() );
+    fprintf( pFile, ".model Sorter%02d\n", nVars );
+
+    fprintf( pFile, ".inputs" );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " x%02d", i );
+    fprintf( pFile, "\n" );
+
+    fprintf( pFile, ".outputs" );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " y%02d", i );
+    fprintf( pFile, "\n" );
+
+    Counter = 0;
+    nDigits = Extra_Base10Log( (nVars-2)*nVars );
+    if ( nVars == 2 )
+        fprintf( pFile, ".subckt Comp a=x00 b=x01 x=y00 y=y01\n" );
+    else
+    {
+        fprintf( pFile, ".subckt Layer0" );
+        for ( k = 0; k < nVars; k++ )
+            fprintf( pFile, " x%02d=x%02d", k, k );
+        for ( k = 0; k < nVars; k++ )
+            fprintf( pFile, " y%02d=%0*d", k, nDigits, Counter++ );
+        fprintf( pFile, "\n" );
+        Counter -= nVars;
+        for ( i = 1; i < nVars-2; i++ )
+        {
+            fprintf( pFile, ".subckt Layer%d", (i&1) );
+            for ( k = 0; k < nVars; k++ )
+                fprintf( pFile, " x%02d=%0*d", k, nDigits, Counter++ );
+            for ( k = 0; k < nVars; k++ )
+                fprintf( pFile, " y%02d=%0*d", k, nDigits, Counter++ );
+            fprintf( pFile, "\n" );
+            Counter -= nVars;
+        }
+        fprintf( pFile, ".subckt Layer%d", (i&1) );
+        for ( k = 0; k < nVars; k++ )
+            fprintf( pFile, " x%02d=%0*d", k, nDigits, Counter++ );
+        for ( k = 0; k < nVars; k++ )
+            fprintf( pFile, " y%02d=y%02d", k, k );
+        fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" );
+
+    Abc_WriteLayer( pFile, nVars, 0 );
+    Abc_WriteLayer( pFile, nVars, 1 );
+    Abc_WriteComp( pFile );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_WriteLayer( FILE * pFile, int nVars, int fSkip1 )
+{
+    int i;
+    fprintf( pFile, ".model Layer%d\n", fSkip1 );
+    fprintf( pFile, ".inputs" ); 
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " x%02d", i ); 
+    fprintf( pFile, "\n" ); 
+    fprintf( pFile, ".outputs" ); 
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " y%02d", i ); 
+    fprintf( pFile, "\n" ); 
+    if ( fSkip1 )
+    {
+        fprintf( pFile, ".names x00 y00\n" ); 
+        fprintf( pFile, "1 1\n" ); 
+        i = 1;
+    }
+    else
+        i = 0;
+    for ( ; i + 1 < nVars; i += 2 )
+        fprintf( pFile, ".subckt Comp a=x%02d b=x%02d x=y%02d y=y%02d\n", i, i+1, i, i+1 );
+    if ( i < nVars )
+    {
+        fprintf( pFile, ".names x%02d y%02d\n", i, i ); 
+        fprintf( pFile, "1 1\n" ); 
+    }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_WriteComp( FILE * pFile )
+{
+    fprintf( pFile, ".model Comp\n" );
+    fprintf( pFile, ".inputs a b\n" ); 
+    fprintf( pFile, ".outputs x y\n" ); 
+    fprintf( pFile, ".names a b x\n" ); 
+    fprintf( pFile, "11 1\n" ); 
+    fprintf( pFile, ".names a b y\n" ); 
+    fprintf( pFile, "1- 1\n" ); 
+    fprintf( pFile, "-1 1\n" ); 
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_WriteFullAdder( FILE * pFile )
+{
+    fprintf( pFile, ".model FA\n" );
+    fprintf( pFile, ".inputs a b cin\n" ); 
+    fprintf( pFile, ".outputs s cout\n" ); 
+    fprintf( pFile, ".names a b k\n" ); 
+    fprintf( pFile, "10 1\n" ); 
+    fprintf( pFile, "01 1\n" ); 
+    fprintf( pFile, ".names k cin s\n" ); 
+    fprintf( pFile, "10 1\n" ); 
+    fprintf( pFile, "01 1\n" ); 
+    fprintf( pFile, ".names a b cin cout\n" ); 
+    fprintf( pFile, "11- 1\n" ); 
+    fprintf( pFile, "1-1 1\n" ); 
+    fprintf( pFile, "-11 1\n" ); 
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abci/abcMap.c

@@ -522,7 +522,11 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
     // duplicate the network
     pNtkNew2 = Abc_NtkDup( pNtk );
     pNtkNew  = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1, 0 );
-    Abc_NtkBddToSop( pNtkNew, 0 );
+    if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
+    {
+        printf( "Converting to SOPs has failed.\n" );
+        return NULL;
+    }
 
     // set the old network to point to the new network
     Abc_NtkForEachCi( pNtk, pNode, i )

src/base/abci/abcMiter.c

@@ -282,7 +282,129 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
 
 
 
+/**Function*************************************************************
+
+  Synopsis    [Derives the AND of two miters.]
+
+  Description [The network should have the same names of PIs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+{
+    char Buffer[100];
+    Abc_Ntk_t * pNtkMiter;
+    Abc_Obj_t * pOutput1, * pOutput2;
+    Abc_Obj_t * pRoot1, * pRoot2, * pMiter;
+
+    assert( Abc_NtkIsStrash(pNtk1) );
+    assert( Abc_NtkIsStrash(pNtk2) );
+    assert( 1 == Abc_NtkCoNum(pNtk1) );
+    assert( 1 == Abc_NtkCoNum(pNtk2) );
+    assert( 0 == Abc_NtkLatchNum(pNtk1) );
+    assert( 0 == Abc_NtkLatchNum(pNtk2) );
+    assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
+
+    // start the new network
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
+    pNtkMiter->pName = Extra_UtilStrsav(Buffer);
+
+    // perform strashing
+    Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, 1 );
+    Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
+    Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
+//    Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, 1 );
+    pRoot1 = Abc_NtkPo(pNtk1,0);
+    pRoot2 = Abc_NtkPo(pNtk2,0);
+    pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot1)->pCopy, Abc_ObjFaninC0(pRoot1) );
+    pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, Abc_ObjFaninC0(pRoot2) );
+
+    // create the miter of the two outputs
+    pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 );
+    Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
+
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkMiter ) )
+    {
+        printf( "Abc_NtkMiterAnd: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkMiter );
+        return NULL;
+    }
+    return pNtkMiter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cofactor of the miter w.r.t. the set of vars.]
+
+  Description [The array of variable values contains -1/0/1 for each PI.
+  -1 means this PI remains, 0/1 means this PI is set to 0/1.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
+{
+    char Buffer[100];
+    Abc_Ntk_t * pNtkMiter;
+    Abc_Obj_t * pRoot, * pOutput1;
+    int Value, i;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( 1 == Abc_NtkCoNum(pNtk) );
+
+    // start the new network
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    sprintf( Buffer, "%s_miter", pNtk->pName );
+    pNtkMiter->pName = Extra_UtilStrsav(Buffer);
+
+    // get the root output
+    pRoot = Abc_NtkCo( pNtk, 0 );
+
+    // perform strashing
+    Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 );
+    // set the first cofactor
+    Vec_IntForEachEntry( vPiValues, Value, i )
+    {
+        if ( Value == -1 )
+            continue;
+        if ( Value == 0 )
+        {
+            Abc_NtkCi(pNtk, i)->pCopy = Abc_ObjNot( Abc_NtkConst1(pNtkMiter) );
+            continue;
+        }
+        if ( Value == 1 )
+        {
+            Abc_NtkCi(pNtk, i)->pCopy = Abc_NtkConst1(pNtkMiter);
+            continue;
+        }
+        assert( 0 );
+    }
+    // add the first cofactor
+    Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
+
+    // save the output
+    pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) );
+
+    // create the miter of the two outputs
+    Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pOutput1 );
 
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkMiter ) )
+    {
+        printf( "Abc_NtkMiterCofactor: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkMiter );
+        return NULL;
+    }
+    return pNtkMiter;
+}
 /**Function*************************************************************
 
   Synopsis    [Derives the miter of two cofactors of one output.]

src/base/abci/abcNewAig.c

@@ -65,7 +65,13 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk )
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return;
+        }
+    }
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );

src/base/abci/abcNtbdd.c

@@ -27,7 +27,7 @@
 static void        Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node );
-static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax );
+static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -243,15 +243,14 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly )
+DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly, int fReorder, int fVerbose )
 {
-    int fReorder = 1;
     ProgressBar * pProgress;
     Vec_Ptr_t * vFuncsGlob;
     Abc_Obj_t * pNode;
     DdNode * bFunc;
     DdManager * dd;
-    int i;
+    int i, Counter;
 
     // start the manager
     assert( pNtk->pManGlob == NULL );
@@ -269,18 +268,20 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
 
     // collect the global functions of the COs
     vFuncsGlob = Vec_PtrAlloc( 100 );
+    Counter = 0;
     if ( fLatchOnly )
     {
         // construct the BDDs
-        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkLatchNum(pNtk) );
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
         Abc_NtkForEachLatch( pNtk, pNode, i )
         {
-            Extra_ProgressBarUpdate( pProgress, i, NULL );
-            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax );
+//            Extra_ProgressBarUpdate( pProgress, i, NULL );
+            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
             if ( bFunc == NULL )
             {
+                if ( fVerbose )
                 printf( "Constructing global BDDs is aborted.\n" );
-                Extra_ProgressBarStop( pProgress );
+                Vec_PtrFree( vFuncsGlob );
                 Cudd_Quit( dd );
                 return NULL;
             }
@@ -292,15 +293,16 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
     else
     {
         // construct the BDDs
-        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
-            Extra_ProgressBarUpdate( pProgress, i, NULL );
-            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax );
+//            Extra_ProgressBarUpdate( pProgress, i, NULL );
+            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
             if ( bFunc == NULL )
             {
+                if ( fVerbose )
                 printf( "Constructing global BDDs is aborted.\n" );
-                Extra_ProgressBarStop( pProgress );
+                Vec_PtrFree( vFuncsGlob );
                 Cudd_Quit( dd );
                 return NULL;
             }
@@ -339,12 +341,14 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax )
+DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose )
 {
     DdNode * bFunc, * bFunc0, * bFunc1;
     assert( !Abc_ObjIsComplement(pNode) );
     if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
     {
+        Extra_ProgressBarStop( pProgress );
+        if ( fVerbose )
         printf( "The number of live nodes reached %d.\n", nBddSizeMax );
         fflush( stdout );
         return NULL;
@@ -353,11 +357,11 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
     if ( pNode->pCopy )
         return (DdNode *)pNode->pCopy;
     // compute the result for both branches
-    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax ); 
+    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose ); 
     if ( bFunc0 == NULL )
         return NULL;
     Cudd_Ref( bFunc0 );
-    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax ); 
+    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose ); 
     if ( bFunc1 == NULL )
         return NULL;
     Cudd_Ref( bFunc1 );
@@ -370,6 +374,9 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
     // set the result
     assert( pNode->pCopy == NULL );
     pNode->pCopy = (Abc_Obj_t *)bFunc;
+    // increment the progress bar
+    if ( pProgress )
+        Extra_ProgressBarUpdate( pProgress, (*pCounter)++, NULL );
     return bFunc;
 }
 
@@ -427,7 +434,7 @@ double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
     Vec_PtrForEachEntry( vNodes, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
     // build the BDD of the cone
-    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000 );  Cudd_Ref( bFunc );
+    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000, NULL, NULL, 1 );  Cudd_Ref( bFunc );
     bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
     // count minterms
     Result = Cudd_CountMinterm( dd, bFunc, dd->size );

src/base/abci/abcPrint.c

@@ -28,6 +28,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+//extern int s_TotalNodes = 0;
+//extern int s_TotalChanges = 0;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -147,6 +150,11 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         fclose( pTable );
     }
 */
+/*
+    s_TotalNodes += Abc_NtkNodeNum(pNtk);
+    printf( "Total nodes = %6d   %6.2f Mb   Changes = %6d.\n", 
+        s_TotalNodes, s_TotalNodes * 20.0 / (1<<20), s_TotalChanges );
+*/
 }
 
 /**Function*************************************************************
@@ -644,7 +652,13 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return;
+        }
+    }
 
     // get hold of the SOP of the node
     CountConst = CountBuf = CountInv = CountAnd = CountOr = CountOther = CounterTotal = 0;

src/base/abci/abcProve.c

@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "fraig.h"
+#include "math.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -32,10 +33,11 @@ extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
 static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails );
 static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
- 
+  
 /**Function*************************************************************
 
   Synopsis    [Attempts to solve the miter using a number of tricks.]
@@ -50,106 +52,126 @@ static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fV
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose )
+int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
 {
+    Prove_Params_t * pParams = pPars;
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2;  // was 5000
-    int nConfs, nImps, nBTLimit, RetValue, nSatFails;
-    int nIter = 0, clk, timeStart = clock();
+    int RetValue, nIter, Counter, clk, timeStart = clock();
 
     // get the starting network
     pNtk = *ppNtk;
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkPoNum(pNtk) == 1 );
 
-    // set the initial limits
-    nConfs   = !nConfLimit? nConfsStart : ABC_MIN( nConfsStart, nConfLimit );
-    nImps    = !nImpLimit ? nImpsStart  : ABC_MIN( nImpsStart , nImpLimit );
-    nBTLimit = nBTLimitStart;
-
-    if ( fVerbose )
-        printf( "Global resource limits: ConfsLim = %6d. ImpsLim = %d.\n", nConfLimit, nImpLimit );
+    if ( pParams->fVerbose )
+    {
+        printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
+            pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
+        printf( "Mitering = %d (%3.1f).  Rewriting = %d (%3.1f).  Fraiging = %d (%3.1f).\n", 
+            pParams->nMiteringLimitStart,  pParams->nMiteringLimitMulti, 
+            pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
+            pParams->nFraigingLimitStart,  pParams->nFraigingLimitMulti );
+        printf( "Mitering last = %d.\n", 
+            pParams->nMiteringLimitLast );
+    }
 
     // if SAT only, solve without iteration
-    if ( !fUseRewrite && !fUseFraig )
+    if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
     {
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 );
-        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+        RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 );
+        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         *ppNtk = pNtk;
         return RetValue;
     }
 
     // check the current resource limits
-    do {
-        nIter++;
-
-        if ( fVerbose )
+    for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
+    {
+        if ( pParams->fVerbose )
         {
-            printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter, nConfs, nBTLimit );
+            printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 
+                 (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 
+                 (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
             fflush( stdout );
         }
 
         // try brute-force SAT
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, nConfs, nImps, 0 );
-        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+        RetValue = Abc_NtkMiterSat( pNtk, (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 0, 0, 0 );
+        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         if ( RetValue >= 0 )
             break;
 
-        if ( fUseRewrite )
+        // try rewriting
+        if ( pParams->fUseRewriting )
         {
             clk = clock();
-
-            // try rewriting
-            Abc_NtkRewrite( pNtk, 0, 0, 0 );
-            if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
-                break;
-            Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
-            if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
-                break;
-            pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
-            if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
-                break;
-
-            Abc_NtkMiterPrint( pNtk, "Rewriting  ", clk, fVerbose );
+            Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
+            while ( 1 )
+            {
+                Abc_NtkRewrite( pNtk, 0, 0, 0 );
+                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+                    break;
+                if ( --Counter == 0 )
+                    break;
+                Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+                    break;
+                if ( --Counter == 0 )
+                    break;
+                pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
+                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+                    break;
+                if ( --Counter == 0 )
+                    break;
+            }
+            Abc_NtkMiterPrint( pNtk, "Rewriting  ", clk, pParams->fVerbose );
         }
-
-        if ( fUseFraig )
+ 
+        if ( pParams->fUseFraiging )
         {
+            int nSatFails;
             // try FRAIGing
             clk = clock();
-            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue, &nSatFails );  Abc_NtkDelete( pNtkTemp );
-            Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, fVerbose );
+            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), &RetValue, &nSatFails );  Abc_NtkDelete( pNtkTemp );
+            Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, pParams->fVerbose );
 //            printf( "NumFails = %d\n", nSatFails );
             if ( RetValue >= 0 )
                 break;
         }
-        else
-            nSatFails = 1000;
-
-        // increase resource limits
-//        nConfs   = ABC_MIN( nConfs * 3 / 2, 1000000000 );   // was 4/2
-        nConfs   = nSatFails * nBTLimit / 2;   
-        nImps    = ABC_MIN( nImps  * 3 / 2, 1000000000 );
-        nBTLimit = ABC_MIN( nBTLimit * 8,   1000000000 );
-
-        // timeout at 5 minutes
-//        if ( clock() - timeStart >= 1200 * CLOCKS_PER_SEC )
-//            break;
-        if ( nIter == 7 )
-            break;
     }    
-//    while ( (nConfLimit == 0 || nConfs <= nConfLimit) && 
-//            (nImpLimit  == 0 || nImps  <= nImpLimit ) );
-    while ( 1 );
 
     // try to prove it using brute force SAT
+    if ( RetValue < 0 && pParams->fUseBdds )
+    {
+        if ( pParams->fVerbose )
+        {
+            printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
+            fflush( stdout );
+        }
+        clk = clock();
+        pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
+        if ( pNtk )   
+        {
+            Abc_NtkDelete( pNtkTemp );
+            RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) );
+        }
+        else 
+            pNtk = pNtkTemp;
+        Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
+    }
+
     if ( RetValue < 0 )
     {
+        if ( pParams->fVerbose )
+        {
+            printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
+            fflush( stdout );
+        }
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 );
-        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+        RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 );
+        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
     }
 
     // assign the model if it was proved by rewriting (const 1 miter)
@@ -240,7 +262,8 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
 {
     if ( !fVerbose )
         return;
-    printf( "Nodes = %7d.  Levels = %4d.  ", Abc_NtkNodeNum(pNtk), Abc_AigGetLevelNum(pNtk) );
+    printf( "Nodes = %7d.  Levels = %4d.  ", Abc_NtkNodeNum(pNtk), 
+        Abc_NtkIsStrash(pNtk)? Abc_AigGetLevelNum(pNtk) : Abc_NtkGetLevelNum(pNtk) );
     PRT( pString, clock() - clk );
 }
 

src/base/abci/abcRefactor.c

@@ -132,6 +132,10 @@ clk = clock();
         Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
 pManRef->timeNtk += clock() - clk;
         Dec_GraphFree( pFForm );
+//    {
+//        extern int s_TotalChanges;
+//        s_TotalChanges++;
+//    }
     }
     Extra_ProgressBarStop( pProgress );
 pManRef->timeTotal = clock() - clkStart;

src/base/abci/abcRestruct.c

@@ -74,7 +74,7 @@ static Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, C
 static Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCut );
 static Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, Abc_Obj_t * pRoot, int Required, int nNodesSaved, int * pnNodesAdded );
 
-static Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fMulti );
+static Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fDag );
 static Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose );
 static void Abc_NtkManRstStop( Abc_ManRst_t * p );
 static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p );
@@ -145,7 +145,7 @@ pManRst->timeCut += clock() - clk;
             break;
         // get the cuts for the given node
 clk = clock();
-        pCutList = Abc_NodeGetCutsRecursive( pManCut, pNode, fMulti ); 
+        pCutList = Abc_NodeGetCutsRecursive( pManCut, pNode, fMulti, 0 ); 
 pManRst->timeCut += clock() - clk;
 
         // perform restructuring
@@ -203,7 +203,7 @@ pManRst->timeTotal = clock() - clkStart;
 ***********************************************************************/
 void Abc_RestructNodeDivisors( Abc_ManRst_t * p, Abc_Obj_t * pRoot, int nNodesSaved )
 {
-    Abc_Obj_t * pNode, * pFanin, * pFanout;
+    Abc_Obj_t * pNode, * pFanout;//, * pFanin;
     int i, k;
     // start with the leaves
     Vec_PtrClear( p->vDecs );
@@ -276,7 +276,7 @@ Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_
 {
     Dec_Graph_t * pGraph;
     Cut_Cut_t * pCut;
-    int nCuts;
+//    int nCuts;
     p->nNodesConsidered++;
 /*
     // count the number of cuts with four inputs or more
@@ -949,7 +949,7 @@ Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fMulti )
+Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fDag )
 {
     static Cut_Params_t Params, * pParams = &Params;
     Cut_Man_t * pManCut;
@@ -963,7 +963,8 @@ Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fM
     pParams->fFilter   = 1;       // filter dominated cuts
     pParams->fSeq      = 0;       // compute sequential cuts
     pParams->fDrop     = 0;       // drop cuts on the fly
-    pParams->fMulti    = fMulti;  // compute factor-cuts
+    pParams->fDag      = fDag;    // compute DAG cuts
+    pParams->fTree     = 0;       // compute tree cuts
     pParams->fVerbose  = 0;       // the verbosiness flag
     pParams->nIdsMax   = Abc_NtkObjNumMax( pNtk );
     pManCut = Cut_ManStart( pParams );
@@ -1351,9 +1352,9 @@ Dec_Graph_t * Abc_NodeMffcSingleNode( Abc_ManRst_t * p, Vec_Int_t * vSims, int n
 ***********************************************************************/
 Dec_Graph_t * Abc_NodeMffcDoubleNode( Abc_ManRst_t * p, Vec_Int_t * vSims, int nNodes, Vec_Int_t * vOnes )
 {
-    Dec_Graph_t * pGraph;
-    unsigned uRoot, uNode;
-    int i;
+//    Dec_Graph_t * pGraph;
+//    unsigned uRoot, uNode;
+//    int i;
 
 
     return NULL;

src/base/abci/abcResub.c

@@ -25,6 +25,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define ABC_RS_DIV1_MAX    150   // the max number of divisors to consider
+#define ABC_RS_DIV2_MAX    500   // the max number of pair-wise divisors to consider
+
 typedef struct Abc_ManRes_t_ Abc_ManRes_t;
 struct Abc_ManRes_t_
 {
@@ -79,6 +82,7 @@ struct Abc_ManRes_t_
     int                nUsedNodeTotal;
     int                nTotalDivs;
     int                nTotalLeaves;
+    int                nTotalGain;
 };
 
 // external procedures
@@ -90,8 +94,8 @@ static void          Abc_ManResubPrint( Abc_ManRes_t * p );
 
 // other procedures
 static int           Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required );
-static int           Abc_ManResubMffc( Abc_ManRes_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves );
 static void          Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords );
+static void          Abc_ManResubPrintDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
 
 static void          Abc_ManResubDivsS( Abc_ManRes_t * p, int Required );
 static void          Abc_ManResubDivsD( Abc_ManRes_t * p, int Required );
@@ -136,13 +140,17 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd
     // cleanup the AIG
     Abc_AigCleanup(pNtk->pManFunc);
     // start the managers
-    pManCut = Abc_NtkManCutStart( nCutMax, 10000, 100000, 100000 );
-    pManRes = Abc_ManResubStart( nCutMax, 200 );
+    pManCut = Abc_NtkManCutStart( nCutMax, 100000, 100000, 100000 );
+    pManRes = Abc_ManResubStart( nCutMax, ABC_RS_DIV1_MAX );
 
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
         Abc_NtkStartReverseLevels( pNtk );
 
+    if ( Abc_NtkLatchNum(pNtk) )
+        Abc_NtkForEachLatch(pNtk, pNode, i)
+            pNode->pNext = pNode->pData;
+
     // resynthesize each node once
     nNodes = Abc_NtkObjNumMax(pNtk);
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
@@ -179,13 +187,16 @@ clk = clock();
 pManRes->timeRes += clock() - clk;
         if ( pFForm == NULL )
             continue;
+        pManRes->nTotalGain += pManRes->nLastGain;
 /*
-        if ( pNode->Id % 25 == 0 )
+        if ( pManRes->nLeaves == 4 && pManRes->nMffc == 2 && pManRes->nLastGain == 1 )
+        {
             printf( "%6d :  L = %2d. V = %2d. Mffc = %2d. Divs = %3d.   Up = %3d. Un = %3d. B = %3d.\n", 
                    pNode->Id, pManRes->nLeaves, Abc_CutVolumeCheck(pNode, vLeaves), pManRes->nMffc, pManRes->nDivs, 
                    pManRes->vDivs1UP->nSize, pManRes->vDivs1UN->nSize, pManRes->vDivs1B->nSize );
+            Abc_ManResubPrintDivs( pManRes, pNode, vLeaves );
+        }
 */
-
         // acceptable replacement found, update the graph
 clk = clock();
         Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRes->nLastGain );
@@ -207,6 +218,10 @@ pManRes->timeTotal = clock() - clkStart;
     Abc_NtkForEachObj( pNtk, pNode, i )
         pNode->pData = NULL;
 
+    if ( Abc_NtkLatchNum(pNtk) )
+        Abc_NtkForEachLatch(pNtk, pNode, i)
+            pNode->pData = pNode->pNext, pNode->pNext = NULL;
+
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
 //    Abc_AigCheckFaninOrder( pNtk->pManFunc );
@@ -340,6 +355,7 @@ void Abc_ManResubPrint( Abc_ManRes_t * p )
                                                    );                          PRT( "TOTAL ", p->timeTotal );
     printf( "Total leaves   = %8d.\n", p->nTotalLeaves );
     printf( "Total divisors = %8d.\n", p->nTotalDivs );
+    printf( "Total gain     = %8d.\n", p->nTotalGain );
     
 }
 
@@ -382,7 +398,7 @@ void Abc_ManResubCollectDivs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vInternal )
 ***********************************************************************/
 int Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required )
 {
-    Abc_Obj_t * pNode, * pFanout;//, * pFanin;
+    Abc_Obj_t * pNode, * pFanout;
     int i, k, Limit, Counter;
 
     Vec_PtrClear( p->vDivs1UP );
@@ -451,10 +467,24 @@ Quits :
     assert( pRoot == Vec_PtrEntryLast(p->vDivs) );
 
     assert( Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) <= Vec_PtrSize(p->vSims) - p->nLeavesMax );
+    return 1;
+}
 
-/*
-if (pRoot->Id == 15281 )
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManResubPrintDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
 {
+    Abc_Obj_t * pFanin, * pNode;
+    int i, k;
     // print the nodes
     Vec_PtrForEachEntry( p->vDivs, pNode, i )
     {
@@ -488,59 +518,7 @@ if (pRoot->Id == 15281 )
     }
     printf( "\n" );
 }
-*/
 
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_ManResubMffc( Abc_ManRes_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves )
-{
-    Abc_Obj_t * pObj;
-    int Counter, i, k;
-    // increment the traversal ID for the leaves
-    // increment the fanout counters of the leaves
-    Abc_NtkIncrementTravId( pRoot->pNtk );
-    Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves )
-    {
-        pObj->vFanouts.nSize++;
-        Abc_NodeSetTravIdCurrent( pObj ); 
-    }
-    // make sure the node is in the cone and is no one of the leaves
-    assert( Abc_NodeIsTravIdPrevious(pRoot) );
-    Counter = Abc_NodeMffcLabel( pRoot );
-    // remove the extra counters
-    Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves )
-        pObj->vFanouts.nSize--;
-
-    // sort the nodes by level!!!
-    
-    // move the labeled nodes to the end 
-    Vec_PtrClear( p->vTemp );
-    k = nLeaves;
-    Vec_PtrForEachEntryStart( vDivs, pObj, i, nLeaves )
-        if ( Abc_NodeIsTravIdCurrent(pObj) )
-            Vec_PtrPush( p->vTemp, pObj );
-        else
-            Vec_PtrWriteEntry( vDivs, k++, pObj );
-    // add the labeled nodes
-    Vec_PtrForEachEntry( p->vTemp, pObj, i )
-        Vec_PtrWriteEntry( vDivs, k++, pObj );
-    assert( k == Vec_PtrSize(p->vDivs) );
-    assert( pRoot == Vec_PtrEntryLast(p->vDivs) );
-    return Counter;
-}
 
 /**Function*************************************************************
 
@@ -928,7 +906,7 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
 
             puData1 = pObj1->pData;
 
-            if ( Vec_PtrSize(p->vDivs2UP0) < 500 )
+            if ( Vec_PtrSize(p->vDivs2UP0) < ABC_RS_DIV2_MAX )
             {
                 // get positive unate divisors
                 for ( w = 0; w < p->nWords; w++ )
@@ -965,7 +943,7 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
                 }
             }
 
-            if ( Vec_PtrSize(p->vDivs2UN0) < 500 )
+            if ( Vec_PtrSize(p->vDivs2UN0) < ABC_RS_DIV2_MAX )
             {
                 // get negative unate divisors
                 for ( w = 0; w < p->nWords; w++ )

src/base/abci/abcRewrite.c

@@ -110,6 +110,10 @@ clk = clock();
             Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
 Rwr_ManAddTimeUpdate( pManRwr, clock() - clk );
             if ( fCompl ) Dec_GraphComplement( pGraph );
+//    {
+//        extern int s_TotalChanges;
+//        s_TotalChanges++;
+//    }
         }
     }
     Extra_ProgressBarStop( pProgress );

src/base/abci/abcSat.c

@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
+extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
 static nMuxes;
 
 ////////////////////////////////////////////////////////////////////////
@@ -42,7 +42,7 @@ static nMuxes;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFront, int fVerbose )
 {
     solver * pSat;
     lbool   status;
@@ -56,7 +56,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbo
 
     // load clauses into the solver
     clk = clock();
-    pSat = Abc_NtkMiterSatCreate( pNtk );
+    pSat = Abc_NtkMiterSatCreate( pNtk, fJFront );
     if ( pSat == NULL )
         return 1;
 //    printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
@@ -107,6 +107,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbo
         Vec_IntFree( vCiIds );
     }
     // free the solver
+    if ( fVerbose )
+        Asat_SatPrintStats( stdout, pSat );
     solver_delete( pSat );
     return RetValue;
 }
@@ -391,12 +393,14 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
+int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
 {
     Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
     Vec_Ptr_t * vNodes, * vSuper;
-    Vec_Int_t * vVars;
+    Vec_Int_t * vVars, * vFanio;
+    Vec_Vec_t * vCircuit;
     int i, k, fUseMuxes = 1;
+    int clk1 = clock(), clk;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
@@ -408,6 +412,9 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
     vNodes = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the solver
     vSuper = Vec_PtrAlloc( 100 );    // the nodes belonging to the given implication supergate
     vVars  = Vec_IntAlloc( 100 );    // the temporary array for variables in the clause
+    if ( fJFront )
+        vCircuit = Vec_VecAlloc( 1000 );
+//        vCircuit = Vec_VecStart( 184 );
 
     // add the clause for the constant node
     pNode = Abc_NtkConst1(pNtk);
@@ -485,6 +492,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
             if ( vSuper->nSize == 0 )
             {
                 if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
+//                if ( !Abc_NtkClauseTriv( pSat, pNode, vVars ) )
                     return 0;
             }
             else
@@ -493,6 +501,32 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
                     return 0;
             }
         }
+        // add the variables to the J-frontier
+        if ( !fJFront )
+            continue;
+        // make sure that the fanin entries go first
+        assert( pNode->pCopy );
+        Vec_VecExpand( vCircuit, (int)pNode->pCopy );
+        vFanio = Vec_VecEntry( vCircuit, (int)pNode->pCopy );
+        Vec_PtrForEachEntryReverse( vSuper, pFanin, k )
+//        Vec_PtrForEachEntry( vSuper, pFanin, k )
+        {
+            pFanin = Abc_ObjRegular( pFanin );
+            assert( pFanin->pCopy && pFanin->pCopy != pNode->pCopy );
+            Vec_IntPushFirst( vFanio, (int)pFanin->pCopy );
+            Vec_VecPush( vCircuit, (int)pFanin->pCopy, pNode->pCopy );
+        }
+    }
+
+    // create the variable order
+    if ( fJFront )
+    {
+    clk = clock();
+        Asat_JManStart( pSat, vCircuit );
+        Vec_VecFree( vCircuit );
+    PRT( "Setup", clock() - clk );
+//        Asat_JManStop( pSat );
+//    PRT( "Total", clock() - clk1 );
     }
 
     // delete
@@ -513,7 +547,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
+solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront )
 {
     solver * pSat;
     Abc_Obj_t * pNode;
@@ -522,7 +556,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
     nMuxes = 0;
 
     pSat = solver_new();
-    RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
+    RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk, fJFront );
     Abc_NtkForEachObj( pNtk, pNode, i )
         pNode->fMarkA = 0;
 //    Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );

src/base/abci/abcStrash.c

@@ -58,7 +58,13 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return NULL;
+        }
+    }
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
@@ -72,7 +78,9 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
 //    if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
 //        printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
     if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
-        printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
+    {
+//        printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
+    }
     // duplicate EXDC 
     if ( pNtk->pExdc )
         pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
@@ -108,7 +116,13 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     assert( Abc_NtkIsStrash(pNtk1) );
     assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); 
     if ( Abc_NtkIsBddLogic(pNtk2) )
-        Abc_NtkBddToSop(pNtk2, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk2, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return 0;
+        }
+    }
     // check that the networks have the same PIs
     // reorder PIs of pNtk2 according to pNtk1
     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1 ) )
@@ -163,6 +177,7 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fAllNodes
         assert( pObj->pCopy == NULL );
         // mark the old object with the new AIG node
         pObj->pCopy = pNodeNew;
+        Abc_HManAddProto( pObj->pCopy, pObj );
     }
     Vec_PtrFree( vNodes );
     Extra_ProgressBarStop( pProgress );

src/base/abci/abcSymm.c

@@ -88,7 +88,7 @@ void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
 
     // compute the global functions
 clk = clock();
-    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 0 );
+    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 0, 1, fVerbose );
     Cudd_AutodynDisable( dd );
     Cudd_zddVarsFromBddVars( dd, 2 );
 clkBdd = clock() - clk;

src/base/abci/abcUnate.c

@@ -73,7 +73,7 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
     int clkBdd, clkUnate;
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL )
         return;
 clkBdd = clock() - clk;
 

src/base/abci/abcUnreach.c

@@ -58,7 +58,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     }
 
     // compute the global BDDs of the latches
-    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1 );    
+    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );    
     if ( dd == NULL )
         return 0;
     if ( fVerbose )
@@ -331,7 +331,11 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
 
     // transform the network to the SOP representation
-    Abc_NtkBddToSop( pNtkNew, 0 );
+    if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
+    {
+        printf( "Converting to SOPs has failed.\n" );
+        return NULL;
+    }
     return pNtkNew;
 }
 

src/base/abci/abcVanEijk.c

@@ -713,7 +713,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit )
 Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pClass, * pNode, * pRepr, * pObj, *pObjNew;
+    Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;//, *pObjNew;
     Abc_Obj_t * pMiter, * pTotal;
     Vec_Ptr_t * vCone;
     int i, k;

src/base/abci/abcVanImp.c

@@ -870,7 +870,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
 {
     Abc_Ntk_t * pNtkNew; 
     Vec_Ptr_t * vCone;
-    Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2, * pObjNew;
+    Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2;//, * pObjNew;
     unsigned Imp;
     int i, k;
 

src/base/abci/abcVerify.c

@@ -85,7 +85,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 );
+    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
@@ -112,6 +112,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
 ***********************************************************************/
 void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
 {
+    Prove_Params_t Params, * pParams = &Params;
 //    Fraig_Params_t Params;
 //    Fraig_Man_t * pMan;
     Abc_Ntk_t * pMiter;
@@ -171,7 +172,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     Abc_NtkDelete( pMiter );
 */
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterProve( &pMiter, 0, 0, 1, 1, 0 );
+    Prove_ParamsSetDefault( pParams );
+    pParams->nItersMax = 5;
+    RetValue = Abc_NtkMiterProve( &pMiter, pParams );
     if ( RetValue == -1 )
         printf( "Networks are undecided (resource limits is reached).\n" );
     else if ( RetValue == 0 )
@@ -254,7 +257,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 );
+    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )

src/base/abci/abc_.c

@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
- 
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -40,6 +40,7 @@
 
 ***********************************************************************/
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/module.make

@@ -10,6 +10,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcFpga.c \
     src/base/abci/abcFraig.c \
         src/base/abci/abcFxu.c \
+        src/base/abci/abcGen.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcNtbdd.c \
@@ -22,11 +23,13 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcRestruct.c \
     src/base/abci/abcResub.c \
     src/base/abci/abcRewrite.c \
+    src/base/abci/abcRr.c \
     src/base/abci/abcSat.c \
     src/base/abci/abcStrash.c \
     src/base/abci/abcSweep.c \
     src/base/abci/abcSymm.c \
     src/base/abci/abcTiming.c \
+    src/base/abci/abcTrace.c \
     src/base/abci/abcUnate.c \
     src/base/abci/abcUnreach.c \
     src/base/abci/abcVanEijk.c \

src/base/cmd/cmd.c

@@ -18,6 +18,10 @@
 
 ***********************************************************************/
  
+#ifdef WIN32
+#include <process.h> 
+#endif
+
 #include "mainInt.h"
 #include "cmdInt.h"
 #include "abc.h"
@@ -45,6 +49,7 @@ static int CmdCommandLs            ( Abc_Frame_t * pAbc, int argc, char ** argv
 #endif
 static int CmdCommandSis           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandMvsis         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int CmdCommandCapo          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -85,6 +90,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "Various", "sis",     CmdCommandSis,            1); 
     Cmd_CommandAdd( pAbc, "Various", "mvsis",   CmdCommandMvsis,          1); 
+    Cmd_CommandAdd( pAbc, "Various", "capo",    CmdCommandCapo,           0); 
 }
 
 /**Function********************************************************************
@@ -1253,6 +1259,11 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
 
     // write out the current network
     pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
+    if ( pNetlist == NULL )
+    {
+        fprintf( pErr, "Cannot produce the intermediate network.\n" );
+        goto usage;
+    }
     Io_WriteBlif( pNetlist, "_sis_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 
@@ -1389,6 +1400,11 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
 
     // write out the current network
     pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
+    if ( pNetlist == NULL )
+    {
+        fprintf( pErr, "Cannot produce the intermediate network.\n" );
+        goto usage;
+    }
     Io_WriteBlif( pNetlist, "_mvsis_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 
@@ -1454,6 +1470,190 @@ usage:
 }
 
 
+/**Function********************************************************************
+
+  Synopsis    [Calls Capo internally.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    FILE * pFile;
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNetlist;
+    char Command[1000], Buffer[100];
+    char * pProgNameCapoWin     = "capo.exe";
+    char * pProgNameCapoUnix    = "capo";
+    char * pProgNameGnuplotWin  = "wgnuplot.exe";
+    char * pProgNameGnuplotUnix = "gnuplot";
+    char * pProgNameCapo;
+    char * pProgNameGnuplot;
+    char * pPlotFileName;
+    int i;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        goto usage;
+    }
+
+    if ( strcmp( argv[0], "capo" ) != 0 )
+    {
+        fprintf( pErr, "Wrong command: \"%s\".\n", argv[0] );
+        goto usage;
+    }
+
+    if ( argc > 1 )
+    {
+        if ( strcmp( argv[1], "-h" ) == 0 )
+            goto usage;
+        if ( strcmp( argv[1], "-?" ) == 0 )
+            goto usage;
+    }
+
+    // get the names from the resource file
+    if ( Cmd_FlagReadByName(pAbc, "capowin") )
+        pProgNameCapoWin = Cmd_FlagReadByName(pAbc, "capowin");
+    if ( Cmd_FlagReadByName(pAbc, "capounix") )
+        pProgNameCapoUnix = Cmd_FlagReadByName(pAbc, "capounix");
+
+    // check if capo is available
+    if ( (pFile = fopen( pProgNameCapoWin, "r" )) )
+        pProgNameCapo = pProgNameCapoWin;
+    else if ( (pFile = fopen( pProgNameCapoUnix, "r" )) )
+        pProgNameCapo = pProgNameCapoUnix;
+    else if ( pFile == NULL )
+    {
+        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pProgNameCapoWin, pProgNameCapoUnix );
+        goto usage;
+    }
+    fclose( pFile );
+
+    if ( Abc_NtkIsMappedLogic(pNtk) )
+    {
+        Abc_NtkUnmap(pNtk);
+        printf( "The current network is unmapped before calling Capo.\n" );
+    }
+
+    // write out the current network
+    pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
+    if ( pNetlist == NULL )
+    {
+        fprintf( pErr, "Cannot produce the intermediate network.\n" );
+        goto usage;
+    }
+    Io_WriteBlif( pNetlist, "_capo_in.blif", 1 );
+    Abc_NtkDelete( pNetlist );
+
+    // create the file for Capo
+    sprintf( Command, "%s -f _capo_in.blif -log out.txt ", pProgNameCapo );
+    pPlotFileName = NULL;
+    for ( i = 1; i < argc; i++ )
+    {
+        sprintf( Buffer, " %s", argv[i] );
+        strcat( Command, Buffer );
+        if ( !strcmp( argv[i], "-plot" ) )
+            pPlotFileName = argv[i+1];
+    }
+
+    // call Capo
+    if ( system( Command ) )
+    {
+        fprintf( pErr, "The following command has returned non-zero exit status:\n" );
+        fprintf( pErr, "\"%s\"\n", Command );
+        unlink( "_capo_in.blif" );
+        goto usage;
+    }
+    // remove temporary networks
+    unlink( "_capo_in.blif" );
+    if ( pPlotFileName == NULL )
+        return 0;
+
+    // get the file name
+    sprintf( Buffer, "%s.plt", pPlotFileName );
+    pPlotFileName = Buffer;
+
+    // read in the Capo plotting output
+    if ( (pFile = fopen( pPlotFileName, "r" )) == NULL )
+    {
+        fprintf( pErr, "Cannot open the plot file \"%s\".\n\n", pPlotFileName );
+        goto usage;
+    }
+    fclose( pFile );
+
+    // get the names from the plotting software
+    if ( Cmd_FlagReadByName(pAbc, "gnuplotwin") )
+        pProgNameGnuplotWin = Cmd_FlagReadByName(pAbc, "gnuplotwin");
+    if ( Cmd_FlagReadByName(pAbc, "gnuplotunix") )
+        pProgNameGnuplotUnix = Cmd_FlagReadByName(pAbc, "gnuplotunix");
+
+    // check if Gnuplot is available
+    if ( (pFile = fopen( pProgNameGnuplotWin, "r" )) )
+        pProgNameGnuplot = pProgNameGnuplotWin;
+    else if ( (pFile = fopen( pProgNameGnuplotUnix, "r" )) )
+        pProgNameGnuplot = pProgNameGnuplotUnix;
+    else if ( pFile == NULL )
+    {
+        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pProgNameGnuplotWin, pProgNameGnuplotUnix );
+        goto usage;
+    }
+    fclose( pFile );
+
+    // spawn the viewer
+#ifdef WIN32
+    if ( _spawnl( _P_NOWAIT, pProgNameGnuplot, pProgNameGnuplot, pPlotFileName, NULL ) == -1 )
+    {
+        fprintf( stdout, "Cannot find \"%s\".\n", pProgNameGnuplot );
+        goto usage;
+    }
+#else
+    {
+        sprintf( Command, "%s %s ", pProgNameGnuplot, pPlotFileName );
+        if ( system( Command ) == -1 )
+        {
+            fprintf( stdout, "Cannot execute \"%s\".\n", Command );
+            goto usage;
+        }
+    }
+#endif
+
+    // remove temporary networks
+//    unlink( pPlotFileName );
+    return 0;
+
+usage:
+    fprintf( pErr, "\n" );
+    fprintf( pErr, "Usage: capo [-h] <com>\n");
+    fprintf( pErr, "         peforms placement of the current network using Capo\n" );
+    fprintf( pErr, "         a Capo binary should be present in the same directory\n" );
+    fprintf( pErr, "         (if plotting, the Gnuplot binary should also be present)\n" );
+    fprintf( pErr, "   -h  : print the command usage\n" );
+    fprintf( pErr, " <com> : a Capo command\n" );
+    fprintf( pErr, "         Example 1: capo\n" );
+    fprintf( pErr, "                    (performs placement with default options)\n" );
+    fprintf( pErr, "         Example 2: capo -AR <aspec_ratio> -WS <whitespace_percentage> -save\n" );
+    fprintf( pErr, "                    (specifies the aspect ratio [default = 1.0] and\n" );
+    fprintf( pErr, "                    the whitespace percentage [0%%; 100%%) [default = 15%%])\n" );
+    fprintf( pErr, "         Example 3: capo -plot <base_fileName>\n" );
+    fprintf( pErr, "                    (produces <base_fileName.plt> and visualize it using Gnuplot)\n" );
+    fprintf( pErr, "         Example 4: capo -help\n" );
+    fprintf( pErr, "                    (prints the default usage message of the Capo binary)\n" );
+    fprintf( pErr, "         Please refer to the Capo webpage for additional information:\n" );
+    fprintf( pErr, "         http://vlsicad.eecs.umich.edu/BK/PDtools/\n" );
+    return 1;                    // error exit 
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/io/ioRead.c

@@ -42,6 +42,9 @@
 Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
 {
     Abc_Ntk_t * pNtk, * pTemp;
+//    extern int s_TotalNodes;
+//    extern int s_TotalChanges;
+//    s_TotalNodes = s_TotalChanges = 0;
     // set the new network
     if ( Extra_FileNameCheckExtension( pFileName, "blif" ) )
         pNtk = Io_ReadBlif( pFileName, fCheck );

src/base/io/ioReadBench.c

@@ -136,7 +136,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                     Abc_ObjSetData( pNode, Abc_SopCreateNor(pNtk->pManFunc, nNames) );
                 else if ( strcmp(pType, "XOR") == 0 )
                     Abc_ObjSetData( pNode, Abc_SopCreateXor(pNtk->pManFunc, nNames) );
-                else if ( strcmp(pType, "NXOR") == 0 )
+                else if ( strcmp(pType, "NXOR") == 0 || strcmp(pType, "XNOR") == 0 )
                     Abc_ObjSetData( pNode, Abc_SopCreateNxor(pNtk->pManFunc, nNames) );
                 else if ( strncmp(pType, "BUF", 3) == 0 )
                     Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) );

src/base/io/ioWriteCnf.c

@@ -23,6 +23,8 @@
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
+ 
+static Abc_Ntk_t * s_pNtk = NULL;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -57,15 +59,51 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
         fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter for combinational circuits.\n" );
         return 0;
     }
+    if ( Abc_NtkNodeNum(pNtk) == 0 )
+    {
+        fprintf( stdout, "The network has no logic nodes. No CNF file is generaled.\n" );
+        return 0;
+    }
     // create solver with clauses
-    pSat = Abc_NtkMiterSatCreate( pNtk );
+    pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
+    if ( pSat == NULL )
+    {
+        fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" );
+        return 1;
+    }        
     // write the clauses
+    s_pNtk = pNtk;
     Asat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 );
+    s_pNtk = NULL;
     // free the solver
     solver_delete( pSat );
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Output the mapping of PIs into variable numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars )
+{
+    extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
+    Abc_Ntk_t * pNtk = s_pNtk;
+    Vec_Int_t * vCiIds;
+    Abc_Obj_t * pObj;
+    int i;
+    vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
+    fprintf( pFile, "c PI variable numbers: <PI_name> <SAT_var_number>\n" );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        fprintf( pFile, "c %s %d\n", Abc_ObjName(pObj), Vec_IntEntry(vCiIds, i) + (int)(incrementVars > 0) );
+    Vec_IntFree( vCiIds );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/io/ioWriteDot.c

@@ -412,7 +412,13 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return;
+        }
+    }
 
     // mark the nodes from the set
     Vec_PtrForEachEntry( vNodes, pNode, i )

src/base/io/ioWriteList.c

@@ -120,8 +120,8 @@ void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost )
     if ( Abc_ObjFanoutNum( Abc_NtkConst1(pNtk) ) > 0 )
         Io_WriteListEdge( pFile, Abc_NtkConst1(pNtk) );
 
-    // write the PO edges
-    Abc_NtkForEachCi( pNtk, pObj, i )
+    // write the PI edges
+    Abc_NtkForEachPi( pNtk, pObj, i )
         Io_WriteListEdge( pFile, pObj );
 
     // write the internal nodes
@@ -132,7 +132,7 @@ void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost )
     if ( fUseHost )
         Io_WriteListHost( pFile, pNtk );
     else
-        Abc_NtkForEachCo( pNtk, pObj, i )
+        Abc_NtkForEachPo( pNtk, pObj, i )
             Io_WriteListEdge( pFile, pObj );
 
     fprintf( pFile, "\n" );
@@ -157,12 +157,13 @@ void Io_WriteListEdge( FILE * pFile, Abc_Obj_t * pObj )
     fprintf( pFile, "%-10s >    ", Abc_ObjName(pObj) );
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        fprintf( pFile, " %s ([%s_to_%s] = %d)", Abc_ObjName(pFanout), Abc_ObjName(pObj), Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) );
-        if ( i == Abc_ObjFanoutNum(pObj) - 1 )
-            fprintf( pFile, "." );
-        else
+        fprintf( pFile, " %s", Abc_ObjName(pFanout) );
+        fprintf( pFile, " ([%s_to_", Abc_ObjName(pObj) );
+        fprintf( pFile, "%s] = %d)", Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) );
+        if ( i != Abc_ObjFanoutNum(pObj) - 1 )
             fprintf( pFile, "," );
     }
+    fprintf( pFile, "." );
     fprintf( pFile, "\n" );
 }
 
@@ -186,22 +187,19 @@ void Io_WriteListHost( FILE * pFile, Abc_Ntk_t * pNtk )
     {
         fprintf( pFile, "%-10s >    ", Abc_ObjName(pObj) );
         fprintf( pFile, " %s ([%s_to_%s] = %d)", "HOST", Abc_ObjName(pObj), "HOST", 0 );
-        if ( i == Abc_NtkPoNum(pNtk) - 1 )
-            fprintf( pFile, "." );
-        else
-            fprintf( pFile, "," );
+        fprintf( pFile, "." );
+        fprintf( pFile, "\n" );
     }
-    fprintf( pFile, "\n" );
 
     fprintf( pFile, "%-10s >    ", "HOST" );
     Abc_NtkForEachPi( pNtk, pObj, i )
     {
-        fprintf( pFile, " %s ([%s_to_%s] = %d)", Abc_ObjName(pObj), "HOST", Abc_ObjName(pObj), 0 );
-        if ( i == Abc_NtkPiNum(pNtk) - 1 )
-            fprintf( pFile, "." );
-        else
+        fprintf( pFile, " %s", Abc_ObjName(pObj) );
+        fprintf( pFile, " ([%s_to_%s] = %d)", "HOST", Abc_ObjName(pObj), 0 );
+        if ( i != Abc_NtkPiNum(pNtk) - 1 )
             fprintf( pFile, "," );
     }
+    fprintf( pFile, "." );
     fprintf( pFile, "\n" );
 }
 

src/base/main/main.h

@@ -81,6 +81,7 @@ extern FILE *          Abc_FrameReadErr( Abc_Frame_t * p );
 extern bool            Abc_FrameReadMode( Abc_Frame_t * p );
 extern bool            Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode );
 extern void            Abc_FrameRestart( Abc_Frame_t * p );
+extern bool            Abc_FrameShowProgress( Abc_Frame_t * p );
 
 extern void            Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
 extern void            Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );

src/base/main/mainFrame.c

@@ -111,9 +111,12 @@ Abc_Frame_t * Abc_FrameAllocate()
     // set the starting step
     p->nSteps = 1;
     p->fBatchMode = 0;
+    p->fProgress = 1;
     // initialize decomposition manager
     define_cube_size(20);
     set_espresso_flags();
+    // initialize the trace manager
+//    Abc_HManStart();
     return p;
 }
 
@@ -132,6 +135,7 @@ Abc_Frame_t * Abc_FrameAllocate()
 void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
     extern void undefine_cube_size();
+//    Abc_HManStop();
     undefine_cube_size();
     if ( p->pManDec ) Dec_ManStop( p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
@@ -155,6 +159,22 @@ void Abc_FrameRestart( Abc_Frame_t * p )
 {
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_FrameShowProgress( Abc_Frame_t * p )
+{
+    return p->fProgress;
+}
+
 
 /**Function*************************************************************
 

src/base/main/mainInt.h

@@ -55,6 +55,7 @@ struct Abc_Frame_t_
     int             nSteps;      // the counter of different network processed
     int             fAutoexac;   // marks the autoexec mode
     int                fBatchMode;     // are we invoked in batch mode?
+    int             fProgress;   // shows progress bars
     // output streams
     FILE *          Out;
     FILE *          Err;

src/base/seq/seqAigCore.c

@@ -358,7 +358,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
     // solve the miter
 clk = clock();
 //    RetValue = Abc_NtkMiterSat_OldAndRusty( pNtkCnf, 30, 0 );
-    RetValue = Abc_NtkMiterSat( pNtkCnf, 500000, 50000000, 0 );
+    RetValue = Abc_NtkMiterSat( pNtkCnf, 500000, 50000000, 0, 0 );
 if ( fVerbose )
 if ( clock() - clk > 100 )
 {

src/base/seq/seqMapIter.c

@@ -613,7 +613,7 @@ void Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk )
         if ( pList == NULL )
             continue;
         for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
-            Cut_TruthCanonicize( pCut );
+            Cut_TruthNCanonicize( pCut );
     }
 }
 

src/base/seq/seqRetCore.c

@@ -107,7 +107,13 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return NULL;
+        }
+    }
 
     // start the network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );

src/map/pga/pgaMatch.c

@@ -73,7 +73,7 @@ void Pga_MappingMatches( Pga_Man_t * p, int Mode )
             continue;
         // get the cuts
 clk = clock();
-        pList = Abc_NodeGetCutsRecursive( p->pManCut, pObj, 0 );
+        pList = Abc_NodeGetCutsRecursive( p->pManCut, pObj, 0, 0 );
 p->timeCuts += clock() - clk;
         // match the node
         Pga_MappingMatchNode( p, pObj->Id, pList, Mode );

src/misc/extra/extra.h

@@ -293,6 +293,8 @@ extern char *       Extra_TimeStamp();
 extern char *       Extra_StringAppend( char * pStrGiven, char * pStrAdd );
 extern unsigned     Extra_ReadBinary( char * Buffer );
 extern void         Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
+extern int          Extra_ReadHexadecimal( unsigned Sign[], char * pString, int nVars );
+extern void         Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars );
 extern void         Extra_PrintHex( FILE * pFile, unsigned uTruth, int nVars );
 extern void         Extra_PrintSymbols( FILE * pFile, char Char, int nTimes, int fPrintNewLine );
 
@@ -390,30 +392,68 @@ extern void        Extra_ProgressBarStop( ProgressBar * p );
 extern void        Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString );
 
 static inline void Extra_ProgressBarUpdate( ProgressBar * p, int nItemsCur, char * pString ) 
-{  if ( nItemsCur < *((int*)p) ) return; Extra_ProgressBarUpdate_int(p, nItemsCur, pString); }
-
-/*=== extraUtilIntVec.c ================================================================*/
-
-typedef struct Extra_IntVec_t_    Extra_IntVec_t;
-extern Extra_IntVec_t * Extra_IntVecAlloc( int nCap );
-extern Extra_IntVec_t * Extra_IntVecAllocArray( int * pArray, int nSize );
-extern Extra_IntVec_t * Extra_IntVecAllocArrayCopy( int * pArray, int nSize );
-extern Extra_IntVec_t * Extra_IntVecDup( Extra_IntVec_t * pVec );
-extern Extra_IntVec_t * Extra_IntVecDupArray( Extra_IntVec_t * pVec );
-extern void        Extra_IntVecFree( Extra_IntVec_t * p );
-extern void        Extra_IntVecFill( Extra_IntVec_t * p, int nSize, int Entry );
-extern int *       Extra_IntVecReleaseArray( Extra_IntVec_t * p );
-extern int *       Extra_IntVecReadArray( Extra_IntVec_t * p );
-extern int         Extra_IntVecReadSize( Extra_IntVec_t * p );
-extern int         Extra_IntVecReadEntry( Extra_IntVec_t * p, int i );
-extern int         Extra_IntVecReadEntryLast( Extra_IntVec_t * p );
-extern void        Extra_IntVecWriteEntry( Extra_IntVec_t * p, int i, int Entry );
-extern void        Extra_IntVecGrow( Extra_IntVec_t * p, int nCapMin );
-extern void        Extra_IntVecShrink( Extra_IntVec_t * p, int nSizeNew );
-extern void        Extra_IntVecClear( Extra_IntVec_t * p );
-extern void        Extra_IntVecPush( Extra_IntVec_t * p, int Entry );
-extern int         Extra_IntVecPop( Extra_IntVec_t * p );
-extern void        Extra_IntVecSort( Extra_IntVec_t * p );
+{  if ( p && nItemsCur < *((int*)p) ) return; Extra_ProgressBarUpdate_int(p, nItemsCur, pString); }
+
+/*=== extraUtilTruth.c ================================================================*/
+
+static inline int Extra_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+static inline int Extra_WordCountOnes( unsigned uWord )
+{
+    uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
+    uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
+    uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
+    uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
+    return  (uWord & 0x0000FFFF) + (uWord>>16);
+}
+static inline int Extra_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        if ( pIn0[w] != pIn1[w] )
+            return 0;
+    return 1;
+}
+static inline void Extra_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = pIn[w];
+}
+static inline void Extra_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = ~pIn[w];
+}
+static inline void Extra_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = pIn0[w] & pIn1[w];
+}
+static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = ~(pIn0[w] & pIn1[w]);
+}
+
+extern void     Extra_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
+extern void     Extra_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
+extern void     Extra_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
+extern DdNode * Extra_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
+extern int      Extra_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
+extern int      Extra_TruthSupportSize( unsigned * pTruth, int nVars );
+extern int      Extra_TruthSupport( unsigned * pTruth, int nVars );
+extern void     Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
+extern void     Extra_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
+extern void     Extra_TruthCombine( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
+extern void     Extra_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
+extern int      Extra_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
+extern int      Extra_TruthCountOnes( unsigned * pTruth, int nVars );
+extern void     Extra_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
+extern unsigned Extra_TruthHash( unsigned * pIn, int nWords );
+extern unsigned Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
 
 /*=== extraUtilUtil.c ================================================================*/
 

src/misc/extra/extraUtilFile.c

@@ -320,6 +320,65 @@ void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits )
 
 /**Function*************************************************************
 
+  Synopsis    [Reads the hex unsigned into the bit-string.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_ReadHexadecimal( unsigned Sign[], char * pString, int nVars )
+{
+    int nDigits, Digit, k, c;
+    Sign[0] = 0;
+    // write the number into the file
+    nDigits = (1 << nVars) / 4;
+    for ( k = 0; k < nDigits; k++ )
+    {
+        c = nDigits-1-k;
+        if ( pString[c] >= '0' && pString[c] <= '9' )
+            Digit = pString[c] - '0';
+        else if ( pString[c] >= 'A' && pString[c] <= 'F' )
+            Digit = pString[c] - 'A' + 10;
+        else if ( pString[c] >= 'a' && pString[c] <= 'f' )
+            Digit = pString[c] - 'a' + 10;
+        else { assert( 0 ); return 0; }
+        Sign[k/8] |= ( (Digit & 15) << ((k%8) * 4) );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the hex unsigned into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars )
+{
+    int nDigits, Digit, k;
+    // write the number into the file
+    nDigits = (1 << nVars) / 4;
+    for ( k = nDigits - 1; k >= 0; k-- )
+    {
+        Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15);
+        if ( Digit < 10 )
+            fprintf( pFile, "%d", Digit );
+        else
+            fprintf( pFile, "%c", 'a' + Digit-10 );
+    }
+//    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints the hex unsigned into a file.]
 
   Description []

src/misc/extra/extraUtilProgress.c

@@ -58,6 +58,10 @@ static void Extra_ProgressBarClean( ProgressBar * p );
 ProgressBar * Extra_ProgressBarStart( FILE * pFile, int nItemsTotal )
 {
     ProgressBar * p;
+    extern int Abc_FrameShowProgress( void * p );
+    extern void * Abc_FrameGetGlobalFrame();
+
+    if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL;
     p = ALLOC( ProgressBar, 1 );
     memset( p, 0, sizeof(ProgressBar) );
     p->pFile       = pFile;
@@ -82,6 +86,7 @@ ProgressBar * Extra_ProgressBarStart( FILE * pFile, int nItemsTotal )
 ***********************************************************************/
 void Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString )
 {
+    if ( p == NULL ) return;
     if ( nItemsCur < p->nItemsNext )
         return;
     if ( nItemsCur > p->nItemsTotal )
@@ -107,6 +112,7 @@ void Extra_ProgressBarUpdate_int( ProgressBar * p, int nItemsCur, char * pString
 ***********************************************************************/
 void Extra_ProgressBarStop( ProgressBar * p )
 {
+    if ( p == NULL ) return;
     Extra_ProgressBarClean( p );
     FREE( p );
 }
@@ -125,6 +131,7 @@ void Extra_ProgressBarStop( ProgressBar * p )
 void Extra_ProgressBarShow( ProgressBar * p, char * pString )
 {
     int i;
+    if ( p == NULL ) return;
     if ( pString )
         fprintf( p->pFile, "%s ", pString );
     for ( i = (pString? strlen(pString) + 1 : 0); i < p->posCur; i++ )
@@ -151,6 +158,7 @@ void Extra_ProgressBarShow( ProgressBar * p, char * pString )
 void Extra_ProgressBarClean( ProgressBar * p )
 {
     int i;
+    if ( p == NULL ) return;
     for ( i = 0; i <= p->posTotal; i++ )
         fprintf( p->pFile, " " );
     fprintf( p->pFile, "\r" );

src/misc/extra/module.make

@@ -10,4 +10,5 @@ SRC +=    src/misc/extra/extraBddAuto.c \
     src/misc/extra/extraUtilMisc.c \
     src/misc/extra/extraUtilProgress.c \
     src/misc/extra/extraUtilReader.c \
+    src/misc/extra/extraUtilTruth.c \
     src/misc/extra/extraUtilUtil.c

src/misc/vec/vecInt.h

@@ -457,6 +457,33 @@ static inline void Vec_IntPush( Vec_Int_t * p, int Entry )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Vec_IntPushFirst( Vec_Int_t * p, int Entry )
+{
+    int i;
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_IntGrow( p, 16 );
+        else
+            Vec_IntGrow( p, 2 * p->nCap );
+    }
+    p->nSize++;
+    for ( i = p->nSize - 1; i >= 1; i-- )
+        p->pArray[i] = p->pArray[i-1];
+    p->pArray[0] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry )
 {
     if ( p->nSize == p->nCap )

src/misc/vec/vecVec.h

@@ -123,6 +123,28 @@ static inline Vec_Vec_t * Vec_VecStart( int nSize )
 
 /**Function*************************************************************
 
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecExpand( Vec_Vec_t * p, int Level )
+{
+    int i;
+    if ( p->nSize >= Level + 1 )
+        return;
+    Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
+    for ( i = p->nSize; i <= Level; i++ )
+        p->pArray[i] = Vec_PtrAlloc( 0 );
+    p->nSize = Level + 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []

src/opt/cut/cut.h

@@ -59,8 +59,10 @@ struct Cut_ParamsStruct_t_
     int                fFilter;           // filter dominated cuts
     int                fSeq;              // compute sequential cuts
     int                fDrop;             // drop cuts on the fly
-    int                fMulti;            // compute factor-cuts
+    int                fDag;              // compute only DAG cuts
+    int                fTree;             // compute only tree cuts
     int                fRecord;           // record the cut computation flow
+    int                fFancy;            // perform fancy computations
     int                fVerbose;          // the verbosiness flag
 };
 
@@ -117,8 +119,9 @@ extern void             Cut_ManPrintStats( Cut_Man_t * p );
 extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, int TimeTotal );
 extern void             Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
 extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
+extern void             Cut_ManIncrementDagNodes( Cut_Man_t * p );
 /*=== cutNode.c ==========================================================*/
-extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv ); 
+extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv, int TreeCode ); 
 extern Cut_Cut_t *      Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
 extern Cut_Cut_t *      Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst );
 /*=== cutSeq.c ==========================================================*/
@@ -135,7 +138,13 @@ extern void             Cut_OracleNodeSetTriv( Cut_Oracle_t * p, int Node );
 extern Cut_Cut_t *      Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 );
 extern void             Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node );
 /*=== cutTruth.c ==========================================================*/
-extern void             Cut_TruthCanonicize( Cut_Cut_t * pCut );
+extern void             Cut_TruthNCanonicize( Cut_Cut_t * pCut );
+/*=== cutPre22.c ==========================================================*/
+extern void             Cut_CellPrecompute();
+extern void             Cut_CellLoad();
+extern int              Cut_CellIsRunning();
+extern void             Cut_CellDumpToFile();
+extern int              Cut_CellTruthLookup( unsigned * pTruth, int nVars );
 
 #ifdef __cplusplus
 }

src/opt/cut/cutInt.h

@@ -65,13 +65,13 @@ struct Cut_ManStruct_t_
     Cut_Cut_t *        pStore1[2];
     Cut_Cut_t *        pCompareOld;
     Cut_Cut_t *        pCompareNew;
+    unsigned *         puTemp[4];
     // record of the cut computation
     Vec_Int_t *        vNodeCuts;        // the number of cuts for each node
     Vec_Int_t *        vNodeStarts;      // the number of the starting cut of each node
     Vec_Int_t *        vCutPairs;        // the pairs of parent cuts for each cut
     // statistics
     int                nCutsCur;
-    int                nCutsMulti;
     int                nCutsAlloc;
     int                nCutsDealloc;
     int                nCutsPeak;
@@ -79,8 +79,8 @@ struct Cut_ManStruct_t_
     int                nCutsFilter;
     int                nCutsLimit;
     int                nNodes;
-    int                nNodesMulti;
-    int                nNodesMulti0;
+    int                nNodesDag;
+    int                nNodesNoCuts;
     // runtime
     int                timeMerge;
     int                timeUnion;
@@ -130,7 +130,7 @@ extern void                Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut
 /*=== cutMerge.c ==========================================================*/
 extern Cut_Cut_t *         Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
 /*=== cutNode.c ==========================================================*/
-extern void                Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv ); 
+extern void                Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv, int TreeCode ); 
 extern int                 Cut_CutListVerify( Cut_Cut_t * pList );
 /*=== cutTable.c ==========================================================*/
 extern Cut_HashTable_t *   Cut_TableStart( int Size );
@@ -139,7 +139,8 @@ extern int                 Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t
 extern void                Cut_TableClear( Cut_HashTable_t * pTable );
 extern int                 Cut_TableReadTime( Cut_HashTable_t * pTable );
 /*=== cutTruth.c ==========================================================*/
-extern void                Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 );
+extern void                Cut_TruthComputeOld( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 );
+extern void                Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 );
 
 #endif
 

src/opt/cut/cutMan.c

@@ -61,22 +61,30 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
         Vec_PtrFill( p->vCutsOld, pParams->nIdsMax, NULL );
         p->vCutsTemp = Vec_PtrAlloc( pParams->nCutSet );
         Vec_PtrFill( p->vCutsTemp, pParams->nCutSet, NULL );
+        if ( pParams->fTruth && pParams->nVarsMax > 5 )
+        {
+            pParams->fTruth = 0;
+            printf( "Skipping computation of truth tables for sequential cuts with more than 5 inputs.\n" );
+        }
     }
-    assert( !pParams->fTruth || pParams->nVarsMax <= 5 );
     // entry size
     p->EntrySize = sizeof(Cut_Cut_t) + pParams->nVarsMax * sizeof(int);
     if ( pParams->fTruth )
     {
-        if ( pParams->nVarsMax > 8 )
+        if ( pParams->nVarsMax > 14 )
         {
             pParams->fTruth = 0;
-            printf( "Skipping computation of truth table for more than 8 inputs.\n" );
+            printf( "Skipping computation of truth table for more than %d inputs.\n", 14 );
         }
         else
         {
             p->nTruthWords = Cut_TruthWords( pParams->nVarsMax );
             p->EntrySize += p->nTruthWords * sizeof(unsigned);
         }
+        p->puTemp[0] = ALLOC( unsigned, 4 * p->nTruthWords );
+        p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
+        p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
+        p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
     }
     // enable cut computation recording
     if ( pParams->fRecord )
@@ -120,6 +128,7 @@ void Cut_ManStop( Cut_Man_t * p )
     if ( p->vNodeCuts )   Vec_IntFree( p->vNodeCuts );
     if ( p->vNodeStarts ) Vec_IntFree( p->vNodeStarts );
     if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
+    if ( p->puTemp[0] )   free( p->puTemp[0] );
 
     Extra_MmFixedStop( p->pMmCuts, 0 );
     free( p );
@@ -153,15 +162,10 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     printf( "Cuts per node     = %8.1f\n", ((float)(p->nCutsCur-p->nCutsTriv))/p->nNodes );
     printf( "The cut size      = %8d bytes.\n", p->EntrySize );
     printf( "Peak memory       = %8.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
-    if ( p->pParams->fMulti )
-    {
-    printf( "Factor-cut computation statistics:\n" );
     printf( "Total nodes       = %8d.\n", p->nNodes );
-    printf( "Factor nodes      = %8d.\n", p->nNodesMulti );
-    printf( "Factor nodes 0    = %8d.\n", p->nNodesMulti0 );
-    printf( "Factor cuts       = %8d.\n", p->nCutsMulti );
-    printf( "Cuts per node     = %8.1f\n", ((float)(p->nCutsMulti))/(p->nNodesMulti-p->nNodesMulti0) );
-    }
+    printf( "DAG nodes         = %8d.\n", p->nNodesDag );
+    printf( "Tree nodes        = %8d.\n", p->nNodes - p->nNodesDag );
+    printf( "Nodes w/o cuts    = %8d.\n", p->nNodesNoCuts );
     PRT( "Merge ", p->timeMerge );
     PRT( "Union ", p->timeUnion );
     PRT( "Filter", p->timeFilter );
@@ -229,6 +233,22 @@ int Cut_ManReadVarsMax( Cut_Man_t * p )
     return p->pParams->nVarsMax;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_ManIncrementDagNodes( Cut_Man_t * p )
+{
+    p->nNodesDag++;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/opt/cut/cutNode.c

@@ -277,7 +277,7 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t
     }
     // compute the truth table
     if ( p->pParams->fTruth )
-        Cut_TruthCompute( pCut, pCut0, pCut1, p->fCompl0, p->fCompl1 );
+        Cut_TruthCompute( p, pCut, pCut0, pCut1, p->fCompl0, p->fCompl1 );
     // add to the list
     Cut_ListAdd( pSuperList, pCut );
     // return status (0 if okay; 1 if exceeded the limit)
@@ -295,7 +295,7 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv )
+Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv, int TreeCode )
 {
     Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pList, * pCut;
@@ -312,7 +312,7 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
     // compute the cuts
 clk = clock();
     Cut_ListStart( pSuper );
-    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, Cut_NodeReadCutsNew(p, Node0), Cut_NodeReadCutsNew(p, Node1), fTriv );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, Cut_NodeReadCutsNew(p, Node0), Cut_NodeReadCutsNew(p, Node1), fTriv, TreeCode );
     pList = Cut_ListFinish( pSuper );
 p->timeMerge += clock() - clk;
     // verify the result of cut computation
@@ -351,9 +351,9 @@ p->timeMerge += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv )
+void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv, int TreeCode )
 {
-    Cut_Cut_t * pStop0, * pStop1, * pTemp0, * pTemp1;
+    Cut_Cut_t * pStop0, * pStop1, * pTemp0, * pTemp1, * pStore0, * pStore1;
     int i, nCutsOld, Limit;
     // start with the elementary cut
     if ( fTriv ) 
@@ -375,6 +375,19 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
     // set temporary variables
     p->fCompl0 = fCompl0;
     p->fCompl1 = fCompl1;
+    // if tree cuts are computed, make sure only the unit cuts propagate over the DAG nodes
+    if ( TreeCode & 1 )
+    {
+        assert( pList0->nLeaves == 1 );
+        pStore0 = pList0->pNext;
+        pList0->pNext = NULL;
+    }
+    if ( TreeCode & 2 )
+    {
+        assert( pList1->nLeaves == 1 );
+        pStore1 = pList1->pNext;
+        pList1->pNext = NULL;
+    }
     // find the point in the list where the max-var cuts begin
     Cut_ListForEachCut( pList0, pStop0 )
         if ( pStop0->nLeaves == (unsigned)Limit )
@@ -386,8 +399,10 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
     // small by small
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
+    {
         if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
-            return;
+            goto Quits;
+    }
     // small by large
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCut( pStop1, pTemp1 )
@@ -395,7 +410,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
         if ( (pTemp0->uSign & pTemp1->uSign) != pTemp0->uSign )
             continue;
         if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
-            return;
+            goto Quits;
     }
     // small by large
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
@@ -404,7 +419,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
         if ( (pTemp0->uSign & pTemp1->uSign) != pTemp1->uSign )
             continue;
         if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
-            return;
+            goto Quits;
     }
     // large by large
     Cut_ListForEachCut( pStop0, pTemp0 )
@@ -419,15 +434,15 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
         if ( i < Limit )
             continue;
         if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
-            return;
+            goto Quits;
     } 
-    if ( fTriv ) 
-    {
-        p->nCutsMulti += p->nCutsCur - nCutsOld;         
-        p->nNodesMulti++;
-        if ( p->nCutsCur == nCutsOld )
-            p->nNodesMulti0++;
-    }
+    if ( p->nNodeCuts == 0 )
+        p->nNodesNoCuts++;
+Quits:
+    if ( TreeCode & 1 )
+        pList0->pNext = pStore0;
+    if ( TreeCode & 2 )
+        pList1->pNext = pStore1;
 }
 
 /**Function*************************************************************

src/opt/cut/cutOracle.c

@@ -366,7 +366,7 @@ Cut_Cut_t * Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int No
         ppTail = &pCut->pNext;
         // compute the truth table
         if ( p->pParams->fTruth )
-            Cut_TruthCompute( pCut, pCut0, pCut1, fCompl0, fCompl1 );
+            Cut_TruthComputeOld( pCut, pCut0, pCut1, fCompl0, fCompl1 );
     }
     *ppTail = NULL;
 

src/opt/cut/cutSeq.c

@@ -109,9 +109,9 @@ void Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int
     // merge the old and the new
 clk = clock();
     Cut_ListStart( pSuper );
-    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[0], p->pStore1[1], 0 );
-    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[0], 0 );
-    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[1], fTriv );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[0], p->pStore1[1], 0, 0 );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[0], 0, 0 );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[1], fTriv, 0 );
     pListNew = Cut_ListFinish( pSuper );
 p->timeMerge += clock() - clk;
 

src/opt/cut/cutTruth.c

@@ -20,17 +20,27 @@
 
 #include "cutInt.h"
 
+/* 
+    Truth tables computed in this package are represented as bit-strings
+    stored in the cut data structure. Cuts of any number of inputs have 
+    the truth table with 2^k bits, where k is the max number of cut inputs.
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern int nTotal = 0;
+extern int nGood  = 0;
+extern int nEqual = 0;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Performs truth table computation.]
+  Synopsis    [Computes the stretching phase of the cut w.r.t. the merged cut.]
 
   Description []
                
@@ -60,6 +70,48 @@ static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
 
   Synopsis    [Performs truth table computation.]
 
+  Description [This procedure cannot be used while recording oracle
+  because it will overwrite Num0 and Num1.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_TruthNCanonicize( Cut_Cut_t * pCut )
+{
+    unsigned uTruth;
+    unsigned * uCanon2;
+    char * pPhases2;
+    assert( pCut->nVarsMax < 6 );
+
+    // get the direct truth table
+    uTruth = *Cut_CutReadTruth(pCut);
+
+    // compute the direct truth table
+    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
+//    uCanon[0] = uCanon2[0];
+//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
+//    uPhases[0] = pPhases2[0];
+    pCut->uCanon0 = uCanon2[0];
+    pCut->Num0    = pPhases2[0];
+
+    // get the complemented truth table
+    uTruth = ~*Cut_CutReadTruth(pCut);
+
+    // compute the direct truth table
+    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
+//    uCanon[0] = uCanon2[0];
+//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
+//    uPhases[0] = pPhases2[0];
+    pCut->uCanon1 = uCanon2[0];
+    pCut->Num1    = pPhases2[0];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
   Description []
                
   SideEffects []
@@ -67,7 +119,7 @@ static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 )
+void Cut_TruthComputeOld( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 )
 {
     static unsigned uTruth0[8], uTruth1[8];
     int nTruthWords = Cut_TruthWords( pCut->nVarsMax );
@@ -111,43 +163,55 @@ void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, i
 
   Synopsis    [Performs truth table computation.]
 
-  Description [This procedure cannot be used while recording oracle
-  because it will overwrite Num0 and Num1.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_TruthCanonicize( Cut_Cut_t * pCut )
+void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 )
 {
-    unsigned uTruth;
-    unsigned * uCanon2;
-    char * pPhases2;
-    assert( pCut->nVarsMax < 6 );
-
-    // get the direct truth table
-    uTruth = *Cut_CutReadTruth(pCut);
-
-    // compute the direct truth table
-    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
-//    uCanon[0] = uCanon2[0];
-//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
-//    uPhases[0] = pPhases2[0];
-    pCut->uCanon0 = uCanon2[0];
-    pCut->Num0    = pPhases2[0];
+    // permute the first table
+    if ( fCompl0 ) 
+        Extra_TruthNot( p->puTemp[0], Cut_CutReadTruth(pCut0), pCut->nVarsMax );
+    else
+        Extra_TruthCopy( p->puTemp[0], Cut_CutReadTruth(pCut0), pCut->nVarsMax );
+    Extra_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nVarsMax, Cut_TruthPhase(pCut, pCut0) );
+    // permute the second table
+    if ( fCompl1 ) 
+        Extra_TruthNot( p->puTemp[1], Cut_CutReadTruth(pCut1), pCut->nVarsMax );
+    else
+        Extra_TruthCopy( p->puTemp[1], Cut_CutReadTruth(pCut1), pCut->nVarsMax );
+    Extra_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nVarsMax, Cut_TruthPhase(pCut, pCut1) );
+    // produce the resulting table
+    if ( pCut->fCompl )
+        Extra_TruthNand( Cut_CutReadTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nVarsMax );
+    else
+        Extra_TruthAnd( Cut_CutReadTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nVarsMax );
+    // quit if no fancy computation is needed
+    if ( !p->pParams->fFancy )
+        return;
+
+    // count the total number of truth tables computed
+    nTotal++;
+
+    // MAPPING INTO ALTERA 6-2 LOGIC BLOCKS
+    // call this procedure to find the minimum number of common variables in the cofactors
+    // if this number is less or equal than 3, the cut can be implemented using the 6-2 logic block
+//    if ( Extra_TruthMinCofSuppOverlap( Cut_CutReadTruth(pCut), pCut->nVarsMax, NULL ) <= 3 )
+//        nGood++;
+
+    // MAPPING INTO ACTEL 2x2 CELLS
+    // call this procedure to see if a semi-canonical form can be found in the lookup table 
+    // (if it exists, then a two-level 3-input LUT implementation of the cut exists)
+    // Before this procedure is called, cell manager should be defined by calling
+    // Cut_CellLoad (make sure file "cells22_daomap_iwls.txt" is available in the working dir)
+    if ( Cut_CellIsRunning() && pCut->nVarsMax <= 9 )
+        nGood += Cut_CellTruthLookup( Cut_CutReadTruth(pCut), pCut->nVarsMax );
+}
 
-    // get the complemented truth table
-    uTruth = ~*Cut_CutReadTruth(pCut);
 
-    // compute the direct truth table
-    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
-//    uCanon[0] = uCanon2[0];
-//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
-//    uPhases[0] = pPhases2[0];
-    pCut->uCanon1 = uCanon2[0];
-    pCut->Num1    = pPhases2[0];
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/opt/cut/module.make

@@ -4,5 +4,6 @@ SRC +=  src/opt/cut/cutApi.c \
         src/opt/cut/cutMerge.c \
         src/opt/cut/cutNode.c \
         src/opt/cut/cutOracle.c \
+        src/opt/cut/cutPre22.c \
         src/opt/cut/cutSeq.c \
         src/opt/cut/cutTruth.c 

src/opt/rwr/rwrEva.c

@@ -66,7 +66,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
     Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
     // get the node's cuts
 clk = clock();
-    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0 );
+    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0, 0 );
     assert( pCut != NULL );
 p->timeCut += clock() - clk;
 

src/sat/aig/rwrTruth.c

@@ -95,7 +95,7 @@ static inline int Aig_WordCountOnes( unsigned val )
     val = (val & 0x33333333) + ((val>>2) & 0x33333333);
     val = (val & 0x0F0F0F0F) + ((val>>4) & 0x0F0F0F0F);
     val = (val & 0x00FF00FF) + ((val>>8) & 0x00FF00FF);
-    return (val & 0x0000FFFF) + (val>>8);
+    return (val & 0x0000FFFF) + (val>>16);
 }
 
 /**Function*************************************************************

src/sat/asat/added.c

@@ -41,6 +41,7 @@ static inline int  lit_sign(lit l) { return (l & 1); }
 
 static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement );
 
+extern void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -77,6 +78,7 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin
         return;
     }
     fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
+//    Io_WriteCnfOutputPiMapping( pFile, incrementVars );
     fprintf( pFile, "p cnf %d %d\n", p->size, nClauses );
 
     // write the original clauses
@@ -161,6 +163,31 @@ int * solver_get_model( solver * p, int * pVars, int nVars )
     return pModel;    
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_SatPrintStats( FILE * pFile, solver * p )
+{
+    printf( "Start = %4d. Conf = %6d. Dec = %6d. Prop = %7d. Insp = %8d.\n",
+        (int)p->solver_stats.starts, 
+        (int)p->solver_stats.conflicts,
+        (int)p->solver_stats.decisions,
+        (int)p->solver_stats.propagations,
+        (int)p->solver_stats.inspects );
+    printf( "Total runtime = %7.2f sec.  Var select = %7.2f sec.  Var update = %7.2f sec.\n",
+        (float)(p->timeTotal)/(float)(CLOCKS_PER_SEC),
+        (float)(p->timeSelect)/(float)(CLOCKS_PER_SEC),
+        (float)(p->timeUpdate)/(float)(CLOCKS_PER_SEC) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/sat/asat/module.make

 SRC +=  src/sat/asat/added.c \
     src/sat/asat/asatmem.c \
+    src/sat/asat/jfront.c \
     src/sat/asat/solver.c

src/sat/asat/solver.c

@@ -121,6 +121,7 @@ static inline void    vec_remove(vec* v, void* e)
 
 static inline void order_update(solver* s, int v) // updateorder
 {
+//    int clk = clock();
     int*    orderpos = s->orderpos;
     double* activity = s->activity;
     int*    heap     = (int*)vec_begin(&s->order);
@@ -138,6 +139,7 @@ static inline void order_update(solver* s, int v) // updateorder
     }
     heap[i]     = x;
     orderpos[x] = i;
+//    s->timeUpdate += clock() - clk;
 }
 
 static inline void order_assigned(solver* s, int v) 
@@ -146,16 +148,19 @@ static inline void order_assigned(solver* s, int v)
 
 static inline void order_unassigned(solver* s, int v) // undoorder
 {
+//    int clk = clock();
     int* orderpos = s->orderpos;
     if (orderpos[v] == -1){
         orderpos[v] = vec_size(&s->order);
         vec_push(&s->order,(void*)v);
         order_update(s,v);
     }
+//    s->timeUpdate += clock() - clk;
 }
 
 static int  order_select(solver* s, float random_var_freq) // selectvar
 {
+//    int clk = clock();
     int*    heap;
     double* activity;
     int*    orderpos;
@@ -215,9 +220,15 @@ static int  order_select(solver* s, float random_var_freq) // selectvar
             return next;
     }
 
+//    s->timeSelect += clock() - clk;
     return var_Undef;
 }
 
+// J-frontier
+extern void Asat_JManAssign( Asat_JMan_t * p, int Var );
+extern void Asat_JManUnassign( Asat_JMan_t * p, int Var );
+extern int Asat_JManSelect( Asat_JMan_t * p );
+
 //=================================================================================================
 // Activity functions:
 
@@ -236,7 +247,7 @@ static inline void act_var_bump(solver* s, int v) {
 
     //printf("bump %d %f\n", v-1, activity[v]);
 
-    if (s->orderpos[v] != -1)
+    if ( s->pJMan == NULL && s->orderpos[v] != -1 )
         order_update(s,v);
 
 }
@@ -422,7 +433,10 @@ static inline bool enqueue(solver* s, lit l, clause* from)
         reasons[v] = from;
         s->trail[s->qtail++] = l;
 
-        order_assigned(s, v);
+        if ( s->pJMan )
+            Asat_JManAssign( s->pJMan, v );
+        else
+            order_assigned(s, v);
         return 1;
     }
 }
@@ -460,8 +474,12 @@ static inline void solver_canceluntil(solver* s, int level) {
         reasons[x] = (clause*)0;
     }
 
-    for (c = s->qhead-1; c >= bound; c--)
-        order_unassigned(s,lit_var(trail[c]));
+    if ( s->pJMan )
+        for (c = s->qtail-1; c >= bound; c--)
+            Asat_JManUnassign( s->pJMan, lit_var(trail[c]) );
+    else
+        for (c = s->qhead-1; c >= bound; c--)
+            order_unassigned( s, lit_var(trail[c]) );
 
     s->qhead = s->qtail = bound;
     vec_resize(&s->trail_lim,level);
@@ -803,7 +821,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
     int*    levels          = s->levels;
     double  var_decay       = 0.95;
     double  clause_decay    = 0.999;
-    double  random_var_freq = 0.02;
+    double  random_var_freq = 0.0;//0.02;
 
     int     conflictC       = 0;
     vec     learnt_clause;
@@ -872,7 +890,10 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
 
             // New variable decision:
             s->solver_stats.decisions++;
-            next = order_select(s,(float)random_var_freq);
+            if ( s->pJMan )
+                next = Asat_JManSelect( s->pJMan );
+            else
+                next = order_select(s,(float)random_var_freq);
 
             if (next == var_Undef){
                 // Model found:
@@ -953,7 +974,10 @@ solver* solver_new(void)
 #else
     s->pMem = Asat_MmStepStart( 10 );
 #endif
-
+    s->pJMan = NULL;
+    s->timeTotal = clock();
+    s->timeSelect = 0;
+    s->timeUpdate = 0;
     return s;
 }
 
@@ -998,6 +1022,7 @@ void solver_delete(solver* s)
         free(s->tags     );
     }
 
+    if ( s->pJMan ) Asat_JManStop( s );
     free(s);
 }
 
@@ -1155,6 +1180,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit
         printf("==============================================================================\n");
 
     solver_canceluntil(s,0);
+    s->timeTotal = clock() - s->timeTotal;
     return status;
 }
 

src/sat/asat/solver.h

@@ -64,6 +64,8 @@ static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); }
 //=================================================================================================
 // Public interface:
 
+typedef struct Asat_JMan_t_  Asat_JMan_t;
+
 struct solver_t;
 typedef struct solver_t solver;
 
@@ -82,6 +84,12 @@ extern int     solver_nclauses(solver* s);
 extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName,
                                        lit* assumptionsBegin, lit* assumptionsEnd,
                                        int incrementVars);
+extern void    Asat_SatPrintStats( FILE * pFile, solver * p );
+
+// J-frontier support
+extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit );
+extern void          Asat_JManStop(  solver * pSat );
+
 
 struct stats_t
 {
@@ -143,7 +151,13 @@ struct solver_t
     // the memory manager
     Asat_MmStep_t *     pMem;
 
+    // J-frontier
+    Asat_JMan_t *       pJMan;
+
     stats    solver_stats;
+    int      timeTotal;
+    int      timeSelect;
+    int      timeUpdate;
 };
  
 #ifdef __cplusplus

src/sat/csat/csat_apis.c

@@ -17,6 +17,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "fraig.h"
 #include "csat_apis.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -105,6 +106,8 @@ ABC_Manager ABC_InitManager()
 ***********************************************************************/
 void ABC_ReleaseManager( ABC_Manager mng )
 {
+    CSAT_Target_ResultT * p_res = ABC_Get_Target_Result( mng,0 );
+    ABC_TargetResFree(p_res);
     if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
     if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
     if ( mng->pMmNames )   Extra_MmFlexStop( mng->pMmNames, 0 );
@@ -536,6 +539,7 @@ void ABC_AnalyzeTargets( ABC_Manager mng )
 ***********************************************************************/
 enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
 {
+    Prove_Params_t Params, * pParams = &Params;
     int RetValue, i;
 
     // check if the target network is available
@@ -544,9 +548,16 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
 
     // try to prove the miter using a number of techniques
     if ( mng->mode )
-        RetValue = Abc_NtkMiterSat( mng->pTarget, mng->nConfLimit, mng->nImpLimit, 0 );
+        RetValue = Abc_NtkMiterSat( mng->pTarget, mng->nConfLimit, mng->nImpLimit, 0, 0 );
     else
-        RetValue = Abc_NtkMiterProve( &mng->pTarget, mng->nConfLimit, mng->nImpLimit, 1, 1, 0 );
+    {
+        // set default parameters for CEC
+        Prove_ParamsSetDefault( pParams );
+        // set infinite resource limit for the final mitering
+        pParams->nMiteringLimitLast = ABC_INFINITY;
+        // call the checker
+        RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams );
+    }
 
     // analyze the result
     mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
@@ -658,6 +669,14 @@ void ABC_TargetResFree( CSAT_Target_ResultT * p )
 {
     if ( p == NULL )
         return;
+    if( p->names )
+    {
+        int i = 0;
+        for ( i = 0; i < p->no_sig; i++ )
+        {
+            FREE(p->names[i]);
+        }
+    }
     FREE( p->names );
     FREE( p->values );
     free( p );

src/sat/fraig/fraig.h

@@ -41,6 +41,7 @@ typedef struct Fraig_NodeVecStruct_t_     Fraig_NodeVec_t;
 typedef struct Fraig_HashTableStruct_t_   Fraig_HashTable_t;
 typedef struct Fraig_ParamsStruct_t_      Fraig_Params_t;
 typedef struct Fraig_PatternsStruct_t_    Fraig_Patterns_t;
+typedef struct Prove_ParamsStruct_t_      Prove_Params_t;
 
 struct Fraig_ParamsStruct_t_
 {
@@ -61,6 +62,31 @@ struct Fraig_ParamsStruct_t_
     int  fInternal;     // is set to 1 for internal fraig calls
 };
 
+struct Prove_ParamsStruct_t_
+{
+    // general parameters
+    int   fUseFraiging;          // enables fraiging
+    int   fUseRewriting;         // enables rewriting
+    int   fUseBdds;              // enables BDD construction when other methods fail
+    int   fVerbose;              // prints verbose stats
+    // iterations
+    int   nItersMax;             // the number of iterations
+    // mitering 
+    int   nMiteringLimitStart;   // starting mitering limit
+    float nMiteringLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
+    // rewriting 
+    int   nRewritingLimitStart;  // the number of rewriting iterations
+    float nRewritingLimitMulti;  // multiplicative coefficient to increase the limit in each iteration
+    // fraiging 
+    int   nFraigingLimitStart;   // starting backtrack(conflict) limit
+    float nFraigingLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
+    // last-gasp BDD construction
+    int   nBddSizeLimit;         // the number of BDD nodes when construction is aborted
+    int   fBddReorder;           // enables dynamic BDD variable reordering
+    // last-gasp mitering
+    int   nMiteringLimitLast;    // final mitering limit
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                       GLOBAL VARIABLES                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -155,6 +181,7 @@ extern Fraig_Node_t *      Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pNode,
 extern void                Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t * pNodeOld, Fraig_Node_t * pNodeNew );
 
 /*=== fraigMan.c =============================================================*/
+extern void                Prove_ParamsSetDefault( Prove_Params_t * pParams );
 extern void                Fraig_ParamsSetDefault( Fraig_Params_t * pParams );
 extern void                Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams );
 extern Fraig_Man_t *       Fraig_ManCreate( Fraig_Params_t * pParams );

src/sat/fraig/fraigApi.c

@@ -65,7 +65,7 @@ int               Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p )           {
 // returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns)
 int               Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p )   { return p->iPatsPerm;        }
 // returns the number of times FRAIG package timed out
-int               Fraig_ManReadSatFails( Fraig_Man_t * p )                    { return p->nSatFails;        }      
+int               Fraig_ManReadSatFails( Fraig_Man_t * p )                    { return p->nSatFailsReal;    }      
 
 /**Function*************************************************************
 

src/sat/fraig/fraigInt.h

@@ -189,7 +189,8 @@ struct Fraig_ManStruct_t_
     int                   nSatCalls;     // the number of times equivalence checking was called
     int                   nSatProof;     // the number of times a proof was found
     int                   nSatCounter;   // the number of times a counter example was found
-    int                   nSatFails;     // the number of times the SAT solver failed to complete
+    int                   nSatFails;     // the number of times the SAT solver failed to complete due to resource limit or prediction
+    int                   nSatFailsReal; // the number of times the SAT solver failed to complete due to resource limit
 
     int                   nSatCallsImp;  // the number of times equivalence checking was called
     int                   nSatProofImp;  // the number of times a proof was found
@@ -243,8 +244,9 @@ struct Fraig_NodeStruct_t_
     unsigned              fMark3   :  1; // the mark used for traversals
     unsigned              fFeedUse :  1; // the presence of the variable in the feedback
     unsigned              fFeedVal :  1; // the value of the variable in the feedback
+    unsigned              fFailTfo :  1; // the node is in the TFO of the failed SAT run
     unsigned              nFanouts :  2; // the indicator of fanouts (none, one, or many)
-    unsigned              nOnes    : 21; // the number of 1's in the random sim info
+    unsigned              nOnes    : 20; // the number of 1's in the random sim info
  
     // the children of the node
     Fraig_Node_t *        p1;            // the first child

src/sat/fraig/fraigMan.c

@@ -40,6 +40,42 @@ int timeAssign;
   SeeAlso     []
 
 ***********************************************************************/
+void Prove_ParamsSetDefault( Prove_Params_t * pParams )
+{
+    // general parameters
+    pParams->fUseFraiging         = 1;       // enables fraiging
+    pParams->fUseRewriting        = 1;       // enables rewriting
+    pParams->fUseBdds             = 1;       // enables BDD construction when other methods fail
+    pParams->fVerbose             = 0;       // prints verbose stats
+    // iterations
+    pParams->nItersMax            = 6;       // the number of iterations
+    // mitering 
+    pParams->nMiteringLimitStart  = 1000;    // starting mitering limit
+    pParams->nMiteringLimitMulti  = 2.0;     // multiplicative coefficient to increase the limit in each iteration
+    // rewriting 
+    pParams->nRewritingLimitStart = 3;       // the number of rewriting iterations
+    pParams->nRewritingLimitMulti = 1.0;     // multiplicative coefficient to increase the limit in each iteration
+    // fraiging 
+    pParams->nFraigingLimitStart  = 2;       // starting backtrack(conflict) limit
+    pParams->nFraigingLimitMulti  = 8.0;     // multiplicative coefficient to increase the limit in each iteration
+    // last-gasp BDD construction
+    pParams->nBddSizeLimit        = 1000000; // the number of BDD nodes when construction is aborted
+    pParams->fBddReorder          = 1;       // enables dynamic BDD variable reordering
+    // last-gasp mitering
+    pParams->nMiteringLimitLast   = 1000000; // final mitering limit
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the default parameters of the package.]
+
+  Description [This set of parameters is tuned for equivalence checking.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
 {
     memset( pParams, 0, sizeof(Fraig_Params_t) );
@@ -271,8 +307,8 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
         (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20);
     printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n", 
         p->nWordsRand, p->nWordsDyna, p->iWordPerm, nMemory );
-    printf( "Proof = %d. Counter-example = %d. Fail = %d. Zero = %d.\n", 
-        p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatZeros );
+    printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
+        p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, p->nSatZeros );
     printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) ClaVars = %d.\n", 
         Fraig_CountNodes(p,0), p->vNodes->nSize, Fraig_ManCountMuxes(p), Fraig_ManCountExors(p), p->nVarsClauses );
     if ( p->pSat ) Msat_SolverPrintStats( p->pSat );

src/sat/fraig/fraigNode.c

@@ -176,6 +176,7 @@ Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_
     // compute the level of this node
     pNode->Level = 1 + FRAIG_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
     pNode->fInv  = Fraig_NodeIsSimComplement(p1) & Fraig_NodeIsSimComplement(p2);
+    pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo;
 
     // derive the simulation info 
 clk = clock();

src/sat/fraig/fraigPrime.c

@@ -22,7 +22,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// The 1,000 smallest prime numbers used to compute the hash value
+// The 1,024 smallest prime numbers used to compute the hash value
 // http://www.math.utah.edu/~alfeld/math/primelist.html
 int s_FraigPrimes[FRAIG_MAX_PRIMES] = { 2, 3, 5, 
 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, 
@@ -93,7 +93,9 @@ int s_FraigPrimes[FRAIG_MAX_PRIMES] = { 2, 3, 5,
 7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603, 
 7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723, 
 7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873, 
-7877, 7879, 7883, 7901, 7907, 7919 };
+7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009, 
+8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123, 
+8147, 8161 };
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///

src/sat/fraig/fraigSat.c

@@ -17,6 +17,7 @@
 ***********************************************************************/
 
 #include "fraigInt.h"
+#include "math.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -304,6 +305,20 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
     assert( !Fraig_IsComplement(pOld) );
     assert( pNew != pOld );
 
+    // if at least one of the nodes is a failed node, perform adjustments:
+    // if the backtrack limit is small, simply skip this node
+    // if the backtrack limit is > 10, take the quare root of the limit
+    if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
+    {
+        p->nSatFails++;
+//            return 0;
+//        if ( nBTLimit > 10 )
+//            nBTLimit /= 10;
+        if ( nBTLimit <= 10 )
+            return 0;
+        nBTLimit = (int)sqrt(nBTLimit);
+    }
+
     p->nSatCalls++;
 
     // make sure the solver is allocated and has enough variables
@@ -394,13 +409,27 @@ PRT( "time", clock() - clk );
 
         // record the counter example
         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
+
+//        if ( pOld->fFailTfo || pNew->fFailTfo )
+//            printf( "*" );
+//        printf( "s(%d)", pNew->Level );
         p->nSatCounter++;
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
     {
 p->time3 += clock() - clk;
-        p->nSatFails++;
+
+//        if ( pOld->fFailTfo || pNew->fFailTfo )
+//            printf( "*" );
+//        printf( "T(%d)", pNew->Level );
+
+        // mark the node as the failed node
+        if ( pOld != p->pConst1 ) 
+            pOld->fFailTfo = 1;
+        pNew->fFailTfo = 1;
+//        p->nSatFails++;
+        p->nSatFailsReal++;
         return 0;
     }
 
@@ -454,17 +483,34 @@ PRT( "time", clock() - clk );
         // record the counter example
         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
         p->nSatCounter++;
+
+//        if ( pOld->fFailTfo || pNew->fFailTfo )
+//            printf( "*" );
+//        printf( "s(%d)", pNew->Level );
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
     {
 p->time3 += clock() - clk;
-        p->nSatFails++;
+
+//        if ( pOld->fFailTfo || pNew->fFailTfo )
+//            printf( "*" );
+//        printf( "T(%d)", pNew->Level );
+
+        // mark the node as the failed node
+        pOld->fFailTfo = 1;
+        pNew->fFailTfo = 1;
+//        p->nSatFails++;
+        p->nSatFailsReal++;
         return 0;
     }
 
     // return SAT proof
     p->nSatProof++;
+
+//    if ( pOld->fFailTfo || pNew->fFailTfo )
+//        printf( "*" );
+//    printf( "u(%d)", pNew->Level );
     return 1;
 }
 

src/sat/msat/msatOrderJ.c

@@ -38,7 +38,7 @@ struct Msat_OrderVar_t_
 {
     Msat_OrderVar_t    * pNext;
     Msat_OrderVar_t    * pPrev;
-    int                 Num;
+    int                  Num;
 };
 
 // the ring of variables data structure (J-boundary)
@@ -170,7 +170,8 @@ int Msat_OrderCheck( Msat_Order_t * p )
     Msat_OrderVar_t * pVar, * pNext;
     Msat_IntVec_t * vRound;
     int * pRound, nRound;
-    int * pVars, nVars, i;
+    int * pVars, nVars, i, k;
+    int Counter = 0;
 
     // go through all the variables in the boundary
     Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
@@ -188,10 +189,14 @@ int Msat_OrderCheck( Msat_Order_t * p )
             if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
                 break;
         }
-        assert( i != nRound );
-        if ( i != nRound )
-            return 0;
+//        assert( i != nRound );
+//        if ( i == nRound )
+//            return 0;
+        if ( i == nRound )
+            Counter++;
     }
+    if ( Counter > 0 )
+        printf( "%d(%d) ", Counter, p->rVars.nItems );
 
     // we may also check other unassigned variables in the cone
     // to make sure that if they are not in J-boundary, 
@@ -209,16 +214,16 @@ int Msat_OrderCheck( Msat_Order_t * p )
         vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] );
         nRound = Msat_IntVecReadSize( vRound );
         pRound = Msat_IntVecReadArray( vRound );
-        for ( i = 0; i < nRound; i++ )
+        for ( k = 0; k < nRound; k++ )
         {
-            if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) )
+            if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) )
                 continue;
-            if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
+            if ( Msat_OrderVarIsAssigned(p, pRound[k]) )
                 break;
         }
-        assert( i == nRound );
-        if ( i == nRound )
-            return 0;
+//        assert( k == nRound );
+//        if ( k != nRound )
+//            return 0;
     }
     return 1;
 }
@@ -256,7 +261,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
     Msat_OrderVar_t * pVar, * pNext, * pVarBest;
     double * pdActs = p->pSat->pdActivity;
     double dfActBest;
-    int clk = clock();
+//    int clk = clock();
 
     pVarBest = NULL;
     dfActBest = -1.0;
@@ -268,12 +273,13 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
             pVarBest  = pVar;
         }
     }
-timeSelect += clock() - clk;
-timeAssign += clock() - clk;
+//timeSelect += clock() - clk;
+//timeAssign += clock() - clk;
 
 //if ( pVarBest && pVarBest->Num % 1000 == 0 )
 //printf( "%d ", p->rVars.nItems );
 
+//    Msat_OrderCheck( p );
     if ( pVarBest )
     {
         assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) );
@@ -296,7 +302,7 @@ timeAssign += clock() - clk;
 void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
 {
     Msat_IntVec_t * vRound;
-    int i, clk = clock();
+    int i;//, clk = clock();
 
     // make sure the variable is in the boundary
     assert( Var < p->nVarsAlloc );
@@ -316,7 +322,7 @@ void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
             continue;
         Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] );
     }
-timeSelect += clock() - clk;
+//timeSelect += clock() - clk;
 //    Msat_OrderCheck( p );
 }
 
@@ -334,7 +340,7 @@ timeSelect += clock() - clk;
 void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
 {
     Msat_IntVec_t * vRound, * vRound2;
-    int i, k, clk = clock();
+    int i, k;//, clk = clock();
 
     // make sure the variable is not in the boundary
     assert( Var < p->nVarsAlloc );
@@ -363,7 +369,7 @@ void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
             if ( k == vRound2->nSize ) // there is no assigned vars, delete this one
                 Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] );
         }
-timeSelect += clock() - clk;
+//timeSelect += clock() - clk;
 //    Msat_OrderCheck( p );
 }
 
@@ -450,7 +456,7 @@ void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar )
         pRing->pRoot = pVar->pNext;
     // move the root to the next entry after pVar
     // this way all the additions to the list will be traversed first
-//    pRing->pRoot = pVar->pNext;
+//    pRing->pRoot = pVar->pPrev;
     // delete the node
     pVar->pPrev->pNext = pVar->pNext;
     pVar->pNext->pPrev = pVar->pPrev;

todo.txt

 Minor things:
 
 - add required time support
-
 - clean end-of-line markers (CR is more preferable than CR-LF)
-
-- mysterious Mac problem (fixed?)
-- mysterious Solaris problem (fixed)
-
-- QR's compilation problems
-
+- mysterious Mac problem                                      
 - prevent node name clash between PO and internal names (i.e. [484])
-- add the output of ABC version/platform in the output files
-
-- fix gcc compiler warnings
-
-- update CVS regularly
-
+- add the output of ABC version/platform in the output files  
+- fix gcc compiler warnings                                   
 
 Major things:
 
 - substantially improving performance of FRAIGing 
 (used in equivalence checking and lossless synthesis)
 
-- developing a new (much more efficient and faster) AIG rewriting package
+- developing a new (more efficient and faster) AIG rewriting package
 
 - implementing additional rewriting options for delay optimization
 
@@ -31,7 +21,7 @@ on-demand cut computation currenlty available as a stand-alone command "cut"
 
 - experimenting with yield-aware standard-cell mapping
 
-- developing a hybrid mapper for arbitrary programmable macrocell 
+- developing a mapper for arbitrary programmable macrocell 
 architecture specified using a configuration file (this mapper should work 
 for both cell-evalution and mainstream FPGA mapping)