Version abc70328

abc.dsp

@@ -322,6 +322,10 @@ SOURCE=.\src\base\abci\abcQuant.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcRec.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcReconv.c
 # End Source File
 # Begin Source File

abc.rc

@@ -151,3 +151,17 @@ alias t4       "read_dsd 56BA(a,b*c,e+d,f); clp -r; print_dsd"
 alias t5       "read_dsd 56BA(a,CA(b,c,d),e,f); clp -r; print_dsd"
 alias t6       "read_dsd f*CA(b,c,d)*CA(e,a,g); clp -r; print_dsd"
 
+alias stdsd    "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps"
+alias trec     "rec_start; r c.blif; st; rec_add; rec_use"
+alias trec4    "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
+alias trec5    "rec_start -K 5; r i10.blif; st; rec_add; rec_use"
+alias trec6    "rec_start -K 6; r i10.blif; st; rec_add; rec_use"
+alias trec7    "rec_start -K 7; r i10.blif; st; rec_add; rec_use"
+alias trec8    "rec_start -K 8; r i10.blif; st; rec_add; rec_use"
+alias trec10   "rec_start -K 10; r i10.blif; st; rec_add; rec_use"
+alias trec12   "rec_start -K 12; r i10.blif; st; rec_add; rec_use"
+
+#alias tsh      "r i10_if.blif; st; ps; u; sw; st; ps; cec"
+alias tst4     "r i10_if4.blif; st; ps; r x/rec4_.blif; st; rec_start; r i10_if4.blif; st -r; ps; cec"
+alias tst4n    "r i10_if4.blif; st; ps; r 5npn/all_functions.aig; st; rec_start; r i10_if4.blif; st -r; ps; cec"
+alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_if6.blif; st -r; ps; cec"

readme

@@ -17,6 +17,9 @@ Several things to try if it does not compile on your platform:
   (c) Comment calls to Libs_Init() and Libs_End() in "src\base\main\mainInit.c"
 - Try linking with gcc (rather than g++)
   For this replace "LD   := g++" with "LD   := gcc -lm" in Makefile
+- If your Linux distributin does not have "readline", you may have problems 
+  compiling ABC with gcc. Please try installing this library from
+  http://tiswww.case.edu/php/chet/readline/rltop.html
 
 
 Finally, run regression test:

src/base/abc/abc.h

@@ -747,6 +747,17 @@ extern void               Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj );
 /*=== abcProve.c ==========================================================*/
 extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
 extern int                Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
+/*=== abcRec.c ==========================================================*/
+extern void               Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts );
+extern void               Abc_NtkRecStop();
+extern void               Abc_NtkRecAdd( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkRecPs();
+extern void               Abc_NtkRecFilter( int iVar, int iPlus );
+extern Abc_Ntk_t *        Abc_NtkRecUse();
+extern int                Abc_NtkRecIsRunning();
+extern int                Abc_NtkRecVarNum();
+extern Vec_Int_t *        Abc_NtkRecMemory();
+extern int                Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
 /*=== abcReconv.c ==========================================================*/
 extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
 extern void               Abc_NtkManCutStop( Abc_ManCut_t * p );
@@ -814,8 +825,8 @@ extern char *             Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, in
 extern char *             Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues );
 extern char *             Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues );
 /*=== abcStrash.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup );
-extern Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
+extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord );
+extern Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int fRecord );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos );
 extern Abc_Ntk_t *        Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
 /*=== abcSweep.c ==========================================================*/
@@ -861,6 +872,7 @@ extern int                Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanData( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkCleanEquiv( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkCountCopy( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkLoadCopy( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCopies );

src/base/abc/abcAig.c

@@ -262,6 +262,16 @@ bool Abc_AigCheck( Abc_Aig_t * pMan )
         printf( "Abc_AigCheck: The number of nodes in the structural hashing table is wrong.\n" );
         return 0;
     }
+    // if the node is a choice node, nodes in its class should not have fanouts
+    Abc_NtkForEachNode( pMan->pNtkAig, pObj, i )
+        if ( Abc_AigNodeIsChoice(pObj) )
+            for ( pAnd = pObj->pData; pAnd; pAnd = pAnd->pData )
+                if ( Abc_ObjFanoutNum(pAnd) > 0 )
+                {
+                    printf( "Abc_AigCheck: Representative %s", Abc_ObjName(pAnd) );
+                    printf( " of choice node %s has %d fanouts.\n", Abc_ObjName(pObj), Abc_ObjFanoutNum(pAnd) );
+                    return 0;
+                }
     return 1;
 }
 

src/base/abc/abcDfs.c

@@ -976,8 +976,7 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
     if ( Abc_NodeIsTravIdCurrent(pNode) )
     {
         fprintf( stdout, "Network \"%s\" contains combinational loop!\n", Abc_NtkName(pNtk) );
-        fprintf( stdout, "Node \"%s\" is encountered twice on the following path:\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
-        fprintf( stdout, " %s", Abc_ObjIsNode(pNode)? Abc_ObjName(Abc_ObjFanout0(pNode)) : Abc_NtkName(pNode->pData) );
+        fprintf( stdout, "Node \"%s\" is encountered twice on the following path to the COs:\n", Abc_ObjName(pNode) );
         return 0;
     }
     // mark this node as a node on the current path
@@ -995,9 +994,26 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
         if ( fAcyclic = Abc_NtkIsAcyclic_rec(pFanin) )
             continue;
         // return as soon as the loop is detected
-        fprintf( stdout, " <-- %s", Abc_ObjName(Abc_ObjFanout0(pFanin)) );
+        fprintf( stdout, " %s ->", Abc_ObjName(pFanin) );
         return 0;
     }
+    // visit choices
+    if ( Abc_NtkIsStrash(pNode->pNtk) && Abc_AigNodeIsChoice(pNode) )
+    {
+        for ( pFanin = pNode->pData; pFanin; pFanin = pFanin->pData )
+        {
+            // check if the fanin is visited
+            if ( Abc_NodeIsTravIdPrevious(pFanin) ) 
+                continue;
+            // traverse the fanin's cone searching for the loop
+            if ( fAcyclic = Abc_NtkIsAcyclic_rec(pFanin) )
+                continue;
+            // return as soon as the loop is detected
+            fprintf( stdout, " %s", Abc_ObjName(pFanin) );
+            fprintf( stdout, " (choice of %s) -> ", Abc_ObjName(pNode) );
+            return 0;
+        }
+    }
     // mark this node as a visited node
     Abc_NodeSetTravIdPrevious( pNode );
     return 1;
@@ -1042,7 +1058,7 @@ bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk )
         if ( fAcyclic = Abc_NtkIsAcyclic_rec(pNode) )
             continue;
         // stop as soon as the first loop is detected
-        fprintf( stdout, " (cone of CO \"%s\")\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        fprintf( stdout, " CO \"%s\"\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
         break;
     }
     return fAcyclic;

src/base/abc/abcLib.c

@@ -340,7 +340,7 @@ void Abc_NodeStrashUsingNetwork_rec( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObj )
     Abc_ObjForEachFanin( pObj, pFanin, i )
         Abc_NodeStrashUsingNetwork_rec( pNtkAig, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)) );
     // compute for the node
-    pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj );
+    pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj, 0 );
     // set for the fanout net
     Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
 }
@@ -420,7 +420,7 @@ Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         if ( Abc_ObjIsNode(pObj) )
         {
-            pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj );
+            pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj, 0 );
             Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
             continue;
         }

src/base/abc/abcNtk.c

@@ -669,7 +669,7 @@ Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t
     }
     // copy the nodes
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pCopy = Abc_NodeStrash( pNtkNew, pObj );
+        pObj->pCopy = Abc_NodeStrash( pNtkNew, pObj, 0 );
     Vec_PtrFree( vNodes );
 
     // add the PO

src/base/abc/abcUtil.c

@@ -246,6 +246,7 @@ int Abc_NtkGetAigNodeNum( Abc_Ntk_t * pNtk )
         assert( pNode->pData );
         if ( Abc_ObjFaninNum(pNode) < 2 )
             continue;
+//printf( "%d ", Hop_DagSize( pNode->pData ) );
         nNodes += pNode->pData? Hop_DagSize( pNode->pData ) : 0;
     }
     return nNodes;
@@ -468,6 +469,25 @@ void Abc_NtkCleanData( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Cleans the copy field of all objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCleanEquiv( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pEquiv = NULL;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of nodes having non-trivial copies.]
 
   Description []

src/base/abci/abcDress.c

@@ -73,7 +73,7 @@ void Abc_NtkDress( Abc_Ntk_t * pNtkLogic, char * pFileName, int fVerbose )
     }
 
     // convert the current logic network into an AIG
-    pMiter = Abc_NtkStrash( pNtkLogic, 1, 0 );
+    pMiter = Abc_NtkStrash( pNtkLogic, 1, 0, 0 );
 
     // convert it into the AIG and make the netlist point to the AIG
     Abc_NtkAppend( pMiter, pNtkLogicOrig, 1 );

src/base/abci/abcDsd.c

@@ -27,10 +27,10 @@
  
 static Abc_Ntk_t *     Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
 static void            Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-static Abc_Obj_t *     Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t *     Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew, int * pCounters );
 
 static Vec_Ptr_t *     Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk );
-static void            Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive );
+static void            Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive, int * pCounters );
 static bool            Abc_NodeIsForDsd( Abc_Obj_t * pNode );
 static int             Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars );
 
@@ -171,7 +171,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
     // collect DSD nodes in DFS order (leaves and const1 are not collected)
     ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
     for ( i = 0; i < nNodesDsd; i++ )
-        Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNtkNew );
+        Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNtkNew, NULL );
     free( ppNodesDsd );
 
     // set the pointers to the CO drivers
@@ -200,7 +200,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew )
+Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew, int * pCounters )
 {
     DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
     DdManager * ddNew = pNtkNew->pManFunc;
@@ -257,8 +257,22 @@ Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNode
         }
         case DSD_NODE_PRIME:
         {
+            if ( pCounters )
+            {
+                if ( nDecs < 10 )
+                    pCounters[nDecs]++;
+                else
+                    pCounters[10]++;
+            }
             bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd );                Cudd_Ref( bLocal );
             bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
+/*
+if ( nDecs == 3 )
+{
+Extra_bddPrint( ddDsd, bTemp );
+printf( "\n" );
+}
+*/
             Cudd_RecursiveDeref( ddDsd, bTemp );
             // bLocal is now in the new BDD manager
             break;
@@ -296,6 +310,7 @@ int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive )
     DdManager * dd = pNtk->pManFunc;
     Vec_Ptr_t * vNodes;
     int i;
+    int pCounters[11] = {0};
 
     assert( Abc_NtkIsBddLogic(pNtk) );
 
@@ -308,9 +323,14 @@ int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive )
     // collect nodes for decomposition
     vNodes = Abc_NtkCollectNodesForDsd( pNtk );
     for ( i = 0; i < vNodes->nSize; i++ )
-        Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd, fRecursive );
+        Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd, fRecursive, pCounters );
     Vec_PtrFree( vNodes );
 
+    printf( "Number of non-decomposable functions:\n" );
+    for ( i = 3; i < 10; i++ )
+        printf( "Inputs = %d.  Functions = %6d.\n", i, pCounters[i] );
+    printf( "Inputs > %d.  Functions = %6d.\n", 9, pCounters[10] );
+
     // stop the DSD manager
     Dsd_ManagerStop( pManDsd );
 
@@ -360,7 +380,7 @@ Vec_Ptr_t * Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive )
+void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive, int * pCounters )
 {
     DdManager * dd = pNode->pNtk->pManFunc;
     Abc_Obj_t * pRoot, * pFanin, * pNode1, * pNode2, * pNodeC;
@@ -387,7 +407,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
         ppNodesDsd = Dsd_TreeCollectNodesDfsOne( pManDsd, pNodeDsd, &nNodesDsd );
         for ( i = 0; i < nNodesDsd; i++ )
         {
-            pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk );
+            pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk, pCounters );
             if ( Abc_NodeIsForDsd(pRoot) && fRecursive )
                 Vec_PtrPush( vNodes, pRoot );
         }
@@ -447,12 +467,14 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
 bool Abc_NodeIsForDsd( Abc_Obj_t * pNode )
 {
     DdManager * dd = pNode->pNtk->pManFunc;
-    DdNode * bFunc, * bFunc0, * bFunc1;
+//    DdNode * bFunc, * bFunc0, * bFunc1;
     assert( Abc_ObjIsNode(pNode) );
 //    if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) )
 //        return 1;
 //    return 0;
 
+/*
+    // this does not catch things like a(b+c), which should be decomposed
     for ( bFunc = Cudd_Regular(pNode->pData); !cuddIsConstant(bFunc); )
     {
         bFunc0 = Cudd_Regular( cuddE(bFunc) );
@@ -464,6 +486,9 @@ bool Abc_NodeIsForDsd( Abc_Obj_t * pNode )
         else
             return 1;
     }
+*/
+    if ( Abc_ObjFaninNum(pNode) > 2 )
+        return 1;
     return 0;
 }
 

src/base/abci/abcFraig.c

@@ -166,7 +166,7 @@ Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc
     char ** ppNames;
     int i, k;
     // strash the EXDC network
-    pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0 );
+    pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0, 0 );
     Abc_NtkCleanCopy( pNtkStrash );
     Abc_AigConst1(pNtkStrash)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
     // set the mapping of the PI nodes
@@ -664,7 +664,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
     if ( pStore == NULL )
     {
         // start the stored network
-        pStore = Abc_NtkStrash( pNtk, 0, 0 );
+        pStore = Abc_NtkStrash( pNtk, 0, 0, 0 );
         if ( pStore == NULL )
         {
             printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );

src/base/abci/abcIvy.c

@@ -502,7 +502,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     // strash the network if it is not strashed already
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1 );
+        pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1, 0 );
         Abc_NtkDelete( pNtkTemp );
     }
 

src/base/abci/abcMiter.c

@@ -60,8 +60,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int n
     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 0, fComb ) )
         return NULL;
     // make sure the circuits are strashed 
-    fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0));
-    fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0));
+    fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
+    fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
     if ( pNtk1 && pNtk2 )
         pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize );
     if ( fRemove1 )  Abc_NtkDelete( pNtk1 );

src/base/abci/abcRenode.c

@@ -140,7 +140,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
         s_vMemory2 = NULL;
     }
 
-    printf( "Decomposed %d functions.\n", nDsdCounter );
+//    printf( "Decomposed %d functions.\n", nDsdCounter );
 
     return pNtkNew;
 }
@@ -160,14 +160,14 @@ int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
 {
     Kit_Graph_t * pGraph;
     int i, nNodes;
-
+/*
 extern void Kit_DsdTest( unsigned * pTruth, int nVars );
 if ( If_CutLeaveNum(pCut) == 8 )
 {
     nDsdCounter++;
     Kit_DsdTest( If_CutTruth(pCut), If_CutLeaveNum(pCut) );
 }
-
+*/
     pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
     if ( pGraph == NULL )
     {

src/base/abci/abcStrash.c

@@ -26,7 +26,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fAllNodes );
+static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int fAllNodes, int fRecord );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -96,7 +96,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
+Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord )
 {
     Abc_Ntk_t * pNtkAig;
     int nNodes;
@@ -113,7 +113,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
     // perform strashing
 //    Abc_NtkCleanCopy( pNtk );
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
-    Abc_NtkStrashPerform( pNtk, pNtkAig, fAllNodes );
+    Abc_NtkStrashPerform( pNtk, pNtkAig, fAllNodes, fRecord );
     Abc_NtkFinalize( pNtk, pNtkAig );
     // print warning about self-feed latches
 //    if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
@@ -182,7 +182,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
         printf( "Warning: Procedure Abc_NtkAppend() added %d new CIs.\n", nNewCis );
     // add pNtk2 to pNtk1 while strashing
     if ( Abc_NtkIsLogic(pNtk2) )
-        Abc_NtkStrashPerform( pNtk2, pNtk1, 1 );
+        Abc_NtkStrashPerform( pNtk2, pNtk1, 1, 0 );
     else
         Abc_NtkForEachNode( pNtk2, pObj, i )
             pObj->pCopy = Abc_AigAnd( pNtk1->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
@@ -216,7 +216,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, bool fAllNodes )
+void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, int fAllNodes, int fRecord )
 {
     ProgressBar * pProgress;
     Vec_Ptr_t * vNodes;
@@ -232,7 +232,7 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, bool fAllNo
     Vec_PtrForEachEntry( vNodes, pNodeOld, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        pNodeOld->pCopy = Abc_NodeStrash( pNtkNew, pNodeOld );
+        pNodeOld->pCopy = Abc_NodeStrash( pNtkNew, pNodeOld, fRecord );
     }
     Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
@@ -272,7 +272,7 @@ void Abc_NodeStrash_rec( Abc_Aig_t * pMan, Hop_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
+Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int fRecord )
 {
     Hop_Man_t * pMan;
     Hop_Obj_t * pRoot;
@@ -286,6 +286,20 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
     // check the constant case
     if ( Abc_NodeIsConst(pNodeOld) || Hop_Regular(pRoot) == Hop_ManConst1(pMan) )
         return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Hop_IsComplement(pRoot) );
+    // perform special case-strashing using the record of AIG subgraphs
+    if ( fRecord && Abc_NtkRecIsRunning() && Abc_ObjFaninNum(pNodeOld) > 2 && Abc_ObjFaninNum(pNodeOld) <= Abc_NtkRecVarNum() )
+    {
+        extern Vec_Int_t * Abc_NtkRecMemory();
+        extern int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
+        int nVars = Abc_NtkRecVarNum();
+        Vec_Int_t * vMemory = Abc_NtkRecMemory();
+        unsigned * pTruth = Abc_ConvertAigToTruth( pMan, Hop_Regular(pRoot), nVars, vMemory, 0 );
+        assert( Extra_TruthSupportSize(pTruth, nVars) == Abc_ObjFaninNum(pNodeOld) ); // should be swept
+        if ( Hop_IsComplement(pRoot) )
+            Extra_TruthNot( pTruth, pTruth, nVars );
+        if ( Abc_NtkRecStrashNode( pNtkNew, pNodeOld, pTruth, nVars ) )
+            return pNodeOld->pCopy;
+    }
     // set elementary variables
     Abc_ObjForEachFanin( pNodeOld, pFanin, i )
         Hop_IthVar(pMan, i)->pData = pFanin->pCopy;

src/base/abci/abcSweep.c

@@ -74,7 +74,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
             pObj->pNext = pObj->pData;
     }
     // derive the AIG
-    pNtkAig = Abc_NtkStrash( pNtk, 0, 1 );
+    pNtkAig = Abc_NtkStrash( pNtk, 0, 1, 0 );
     // reconstruct gate assignments
     if ( fUseTrick )
     {

src/base/abci/abcVerify.c

@@ -529,7 +529,7 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
     int fStrashed = 0;
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        pNtk = Abc_NtkStrash(pNtk, 0, 0);
+        pNtk = Abc_NtkStrash(pNtk, 0, 0, 0);
         fStrashed = 1;
     }
 /*
@@ -699,9 +699,9 @@ void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pM
     int fRemove1 = 0, fRemove2 = 0;
 
     if ( !Abc_NtkIsStrash(pNtk1) )
-        fRemove1 = 1, pNtk1 = Abc_NtkStrash( pNtk1, 0, 0 );
+        fRemove1 = 1, pNtk1 = Abc_NtkStrash( pNtk1, 0, 0, 0 );
     if ( !Abc_NtkIsStrash(pNtk2) )
-        fRemove2 = 1, pNtk2 = Abc_NtkStrash( pNtk2, 0, 0 );
+        fRemove2 = 1, pNtk2 = Abc_NtkStrash( pNtk2, 0, 0, 0 );
 
     // simulate sequential circuits
     vInfo1 = Sim_SimulateSeqModel( pNtk1, nFrames, pModel );

src/base/abci/module.make

@@ -33,6 +33,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcProve.c \
     src/base/abci/abcQbf.c \
     src/base/abci/abcQuant.c \
+    src/base/abci/abcRec.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcRefactor.c \
     src/base/abci/abcRenode.c \

src/base/io/io.c

@@ -785,9 +785,6 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCheck;
     int c;
 
-    printf( "Stand-alone structural Verilog reader is now available as command \"read_ver\".\n" );
-    return 0;
-
     fCheck = 1;
     glo_fMapped = 0;
     Extra_UtilGetoptReset();
@@ -851,6 +848,9 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib );
     extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
 
+    printf( "Stand-alone structural Verilog reader is available as command \"read_verilog\".\n" );
+    return 0;
+
     fCheck = 1;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )

src/base/io/ioWriteBench.c

@@ -223,7 +223,7 @@ int Io_WriteBenchLutOne( FILE * pFile, Abc_Ntk_t * pNtk )
     Abc_NtkForEachLatch( pNtk, pNode, i )
         fprintf( pFile, "%-11s = DFFRSE( %s, gnd, gnd, gnd, gnd )\n", 
             Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode))), Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) );
-
+//Abc_NtkLevel(pNtk);
     // write internal nodes
     vMemory = Vec_IntAlloc( 10000 );
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
@@ -283,6 +283,19 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth
     // write it in the hexadecimal form
     fprintf( pFile, "%-11s = LUT 0x",  Abc_ObjName(Abc_ObjFanout0(pNode)) );
     Extra_PrintHexadecimal( pFile, pTruth, nFanins );
+/*
+    {
+extern void Kit_DsdTest( unsigned * pTruth, int nVars );
+Abc_ObjForEachFanin( pNode, pFanin, i )
+printf( "%c%d ", 'a'+i, Abc_ObjFanin0(pFanin)->Level );
+printf( "\n" );
+Kit_DsdTest( pTruth, nFanins );
+    }
+    if ( pNode->Id % 1000 == 0 )
+    {
+        int x = 0;
+    }
+*/
     // write the fanins
     fprintf( pFile, " (" );
     Abc_ObjForEachFanin( pNode, pFanin, i )

src/base/ver/verCore.c

@@ -1184,9 +1184,9 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
             }
 
             // consider the case of mapped network
+            Vec_PtrClear( pMan->vNames );
             if ( pMan->fMapped )
             {
-                Vec_PtrClear( pMan->vNames );
                 if ( !strcmp( pEquation, "1\'b0" ) )
                     pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen());
                 else if ( !strcmp( pEquation, "1\'b1" ) )
@@ -1207,7 +1207,6 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
             }
             else
             {
-                // parse the formula
                 if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") || !strcmp(pEquation, "1\'bx") )
                     pFunc = Hop_ManConst0(pNtk->pManFunc);
                 else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") )

src/map/if/if.h

@@ -101,6 +101,7 @@ struct If_Par_t_
     float *            pTimesArr;     // arrival times
     float *            pTimesReq;     // required times
     int (* pFuncCost)  (If_Cut_t *);  // procedure to compute the user's cost of a cut
+    int (* pFuncUser)  (If_Man_t *, If_Obj_t *, If_Cut_t *); //  procedure called for each cut when cut computation is finished
     void *             pReoMan;       // reordering manager
 };
 

src/map/if/ifMap.c

@@ -149,6 +149,11 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     if ( Mode && pObj->nRefs > 0 )
         If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY );
 
+    // call the user specified function for each cut
+    if ( p->pPars->pFuncUser )
+        If_ObjForEachCut( pObj, pCut, i )
+            p->pPars->pFuncUser( p, pObj, pCut );
+
     // free the cuts
     If_ManDerefNodeCutSet( p, pObj );
 }

src/misc/extra/extra.h

@@ -114,7 +114,7 @@ typedef unsigned long long uint64;
 #endif
 
 #ifndef PRTP
-#define PRTP(a,t,T)  printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), 100.0*(t)/(T))
+#define PRTP(a,t,T)  printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
 #endif
 
 /*===========================================================================*/
@@ -322,6 +322,7 @@ 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_PrintHexadecimalString( char * pString, 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 );
 
@@ -530,22 +531,23 @@ static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned *
         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 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_TruthExist( unsigned * pTruth, int nVars, int iVar );
-extern void     Extra_TruthForall( unsigned * pTruth, int nVars, int iVar );
-extern void     Extra_TruthMux( 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 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 );
+extern unsigned ** Extra_TruthElementary( int nVars );
+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 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_TruthExist( unsigned * pTruth, int nVars, int iVar );
+extern void        Extra_TruthForall( unsigned * pTruth, int nVars, int iVar );
+extern void        Extra_TruthMux( 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 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

@@ -385,6 +385,34 @@ void Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars )
   SeeAlso     []
 
 ***********************************************************************/
+void Extra_PrintHexadecimalString( char * pString, 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 )
+            *pString++ = '0' + Digit;
+        else
+            *pString++ = 'a' + Digit-10;
+    }
+//    fprintf( pFile, "\n" );
+    *pString = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the hex unsigned into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Extra_PrintHex( FILE * pFile, unsigned uTruth, int nVars )
 {
     int nMints, nDigits, Digit, k;

src/misc/extra/extraUtilTruth.c

@@ -62,6 +62,42 @@ static unsigned s_VarMasks[5][2] = {
 
 /**Function*************************************************************
 
+  Synopsis    [Derive elementary truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned ** Extra_TruthElementary( int nVars )
+{
+    unsigned ** pRes;
+    int i, k, nWords;
+    nWords = Extra_TruthWordNum(nVars);
+    pRes = (unsigned **)Extra_ArrayAlloc( nVars, nWords, 4 );
+    for ( i = 0; i < nVars; i++ )
+    {
+        if ( i < 5 )
+        {
+            for ( k = 0; k < nWords; k++ )
+                pRes[i][k] = s_VarMasks[i][1];
+        }
+        else
+        {
+            for ( k = 0; k < nWords; k++ )
+                if ( k & (1 << (i-5)) )
+                    pRes[i][k] = ~(unsigned)0;
+                else
+                    pRes[i][k] = 0;
+        }
+    }
+    return pRes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Swaps two adjacent variables in the truth table.]
 
   Description [Swaps var number Start and var number Start+1 (0-based numbers).

src/misc/vec/vecPtr.h

@@ -309,6 +309,37 @@ static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
 
 /**Function*************************************************************
 
+  Synopsis    [Resizes the array of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrDoubleSimInfo( Vec_Ptr_t * vInfo )
+{
+    Vec_Ptr_t * vInfoNew;
+    int nWords;
+    assert( Vec_PtrSize(vInfo) > 2 );
+    // get the new array
+    nWords = (unsigned *)Vec_PtrEntry(vInfo,1) - (unsigned *)Vec_PtrEntry(vInfo,0);
+    vInfoNew = Vec_PtrAllocSimInfo( 2*Vec_PtrSize(vInfo), nWords );
+    // copy the simulation info
+    memcpy( Vec_PtrEntry(vInfoNew,0), Vec_PtrEntry(vInfo,0), Vec_PtrSize(vInfo) * nWords * 4 );
+    // replace the array
+    free( vInfo->pArray );
+    vInfo->pArray = vInfoNew->pArray;
+    vInfo->nSize *= 2;
+    vInfo->nCap *= 2;
+    // free the old array
+    vInfoNew->pArray = NULL;
+    free( vInfoNew );
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []

src/opt/kit/kit.h

@@ -200,6 +200,23 @@ static inline int Kit_TruthIsOpposite( unsigned * pIn0, unsigned * pIn1, int nVa
             return 0;
     return 1;
 }
+static inline int Kit_TruthIsEqualWithPhase( unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+    int w;
+    if ( (pIn0[0] & 1) == (pIn1[0] & 1) )
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            if ( pIn0[w] != pIn1[w] )
+                return 0;
+    }
+    else
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            if ( pIn0[w] != ~pIn1[w] )
+                return 0;
+    }
+    return 1;
+}
 static inline int Kit_TruthIsConst0( unsigned * pIn, int nVars )
 {
     int w;
@@ -288,6 +305,30 @@ static inline void Kit_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * p
     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = ~(pIn0[w] & pIn1[w]);
 }
+static inline void Kit_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars, int fCompl0, int fCompl1 )
+{
+    int w;
+    if ( fCompl0 && fCompl1 )
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = ~(pIn0[w] | pIn1[w]);
+    }
+    else if ( fCompl0 && !fCompl1 )
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = ~pIn0[w] & pIn1[w];
+    }
+    else if ( !fCompl0 && fCompl1 )
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = pIn0[w] & ~pIn1[w];
+    }
+    else // if ( !fCompl0 && !fCompl1 )
+    {
+        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+            pOut[w] = pIn0[w] & pIn1[w];
+    }
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                           ITERATORS                              ///
@@ -345,8 +386,8 @@ extern int             Kit_SopDivisor( Kit_Sop_t * cResult, Kit_Sop_t * cSop, in
 extern void            Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vMemory );
 /*=== kitTruth.c ==========================================================*/
 extern void            Kit_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
-extern void            Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
-extern void            Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
+extern void            Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn );
+extern void            Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn );
 extern int             Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
 extern int             Kit_TruthSupportSize( unsigned * pTruth, int nVars );
 extern unsigned        Kit_TruthSupport( unsigned * pTruth, int nVars );
@@ -364,6 +405,7 @@ extern void            Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned
 extern void            Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
 extern int             Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
 extern void            Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
+extern void            Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux );
 extern unsigned        Kit_TruthHash( unsigned * pIn, int nWords );
 extern unsigned        Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
 

src/sat/csat/csat_apis.c

@@ -572,7 +572,7 @@ void ABC_SolveInit( ABC_Manager mng )
 
     // set the new target network
 //    mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues );
-    mng->pTarget = Abc_NtkStrash( mng->pNtk, 0, 1 );
+    mng->pTarget = Abc_NtkStrash( mng->pNtk, 0, 1, 0 );
 }
 
 /**Function*************************************************************
@@ -676,7 +676,7 @@ void ABC_Dump_Bench_File( ABC_Manager mng )
     char * pFileName;
  
     // derive the netlist
-    pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0 );
+    pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0, 0 );
     pNtkTemp = Abc_NtkToNetlistBench( pNtkAig );
     Abc_NtkDelete( pNtkAig );
     if ( pNtkTemp == NULL )