Version abc70328

31 files changed, 2078 insertions, 159 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index ececd26f..79134898 100644
--- a/src/base/abc/abc.h
+++ b/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 );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 1d09548b..4c2bb218 100644
--- a/src/base/abc/abcAig.c
+++ b/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;
 }
 
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 3dd9a132..4fabd1ff 100644
--- a/src/base/abc/abcDfs.c
+++ b/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;
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index d9d8bce9..f5b90e90 100644
--- a/src/base/abc/abcLib.c
+++ b/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;
         }
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index bed5d399..df193212 100644
--- a/src/base/abc/abcNtk.c
+++ b/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
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 965e611e..23b89a5b 100644
--- a/src/base/abc/abcUtil.c
+++ b/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 []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9138d897..e76c0261 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -128,6 +128,12 @@ static int Abc_CommandHaigStart      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandHaigStop       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandHaigUse        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandRecStart       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecStop        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecAdd         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecPs          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecUse         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static int Abc_CommandMap            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnmap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAttach         ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -276,6 +282,12 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Choicing",     "haig_stop",     Abc_CommandHaigStop,         0 );
     Cmd_CommandAdd( pAbc, "Choicing",     "haig_use",      Abc_CommandHaigUse,          1 );
 
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_start",     Abc_CommandRecStart,         0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop",      Abc_CommandRecStop,          0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_add",       Abc_CommandRecAdd,           0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_ps",        Abc_CommandRecPs,            0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_use",       Abc_CommandRecUse,           1 );
+
     Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Abc_CommandMap,              1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "unmap",         Abc_CommandUnmap,            1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "attach",        Abc_CommandAttach,           1 );
@@ -313,6 +325,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Map_Var4Test();
 
 //    Abc_NtkPrint256();
+//    Kit_TruthCountMintermsPrecomp();
 } 
 
 /**Function*************************************************************
@@ -454,7 +467,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( !Abc_NtkIsStrash(pNtk->pExdc) )
         {
-            pNtkTemp = Abc_NtkStrash(pNtk->pExdc, 0, 0);
+            pNtkTemp = Abc_NtkStrash(pNtk->pExdc, 0, 0, 0);
             Percentage = Abc_NtkSpacePercentage( Abc_ObjChild0( Abc_NtkPo(pNtkTemp, 0) ) );
             Abc_NtkDelete( pNtkTemp );
         }
@@ -1029,7 +1042,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fReorder, fVerbose );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
         Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fReorder, fVerbose );
         Abc_NtkDelete( pNtk );
     }
@@ -1891,7 +1904,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
         pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
         Abc_NtkDelete( pNtk );
     }
@@ -1933,6 +1946,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
     int fAllNodes;
+    int fRecord;
     int fCleanup;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -1942,8 +1956,9 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     fAllNodes = 0;
     fCleanup  = 1;
+    fRecord   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ach" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "acrh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -1953,6 +1968,9 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fCleanup ^= 1;
             break;
+        case 'r':
+            fRecord ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -1967,7 +1985,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkStrash( pNtk, fAllNodes, fCleanup );
+    pNtkRes = Abc_NtkStrash( pNtk, fAllNodes, fCleanup, fRecord );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Strashing has failed.\n" );
@@ -1978,10 +1996,11 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: strash [-ach]\n" );
+    fprintf( pErr, "usage: strash [-acrh]\n" );
     fprintf( pErr, "\t        transforms combinational logic into an AIG\n" );
     fprintf( pErr, "\t-a    : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" );
     fprintf( pErr, "\t-c    : toggles cleanup to remove the dagling AIG nodes [default = %s]\n", fCleanup? "all": "DFS" );
+    fprintf( pErr, "\t-r    : enables using the record of AIG subgraphs [default = %s]\n", fRecord? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -2047,7 +2066,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
     {
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
         if ( pNtkTemp == NULL )
         {
             fprintf( pErr, "Strashing before balancing has failed.\n" );
@@ -2674,7 +2693,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
         // get the new network
         if ( !Abc_NtkIsStrash(pNtk) )
         {
-            pNtkNew = Abc_NtkStrash( pNtk, 0, 0 );
+            pNtkNew = Abc_NtkStrash( pNtk, 0, 0, 0 );
             pNtkRes = Abc_NtkDsdGlobal( pNtkNew, fVerbose, fPrint, fShort );
             Abc_NtkDelete( pNtkNew );
         }
@@ -3507,7 +3526,7 @@ int Abc_CommandCascade( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtkRes = Abc_NtkCascade( pNtk, nLutSize, fCheck, fVerbose );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
         pNtkRes = Abc_NtkCascade( pNtk, nLutSize, fCheck, fVerbose );
         Abc_NtkDelete( pNtk );
     }
@@ -3708,7 +3727,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
 
     // compute the miter
-    pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, 10 );
+    pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, 0 );
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
 
@@ -4100,7 +4119,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the new network
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
         pNtkRes  = Abc_NtkFrames( pNtkTemp, nFrames, fInitial );
         Abc_NtkDelete( pNtkTemp );
     }
@@ -5619,7 +5638,7 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
 /*
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 1 );
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 1, 0 );
         pNtkRes = Abc_NtkPlayer( pNtkTemp, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
         Abc_NtkDelete( pNtkTemp );
     }
@@ -5924,7 +5943,7 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the strashed network
-    pNtkRes = Abc_NtkStrash( pNtk, 0, 1 );
+    pNtkRes = Abc_NtkStrash( pNtk, 0, 1, 0 );
     RetValue = Abc_NtkQuantify( pNtkRes, fUniv, iVar, fVerbose );
     // clean temporary storage for the cofactors
     Abc_NtkCleanData( pNtkRes );
@@ -6022,7 +6041,7 @@ int Abc_CommandQuaRel( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the strashed network
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        pNtk = Abc_NtkStrash( pNtk, 0, 1 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 1, 0 );
         pNtkRes = Abc_NtkTransRel( pNtk, fInputs, fVerbose );
         Abc_NtkDelete( pNtk );
     }
@@ -6192,7 +6211,7 @@ int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 1 );
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 1, 0 );
         pNtkRes = Abc_NtkIvyStrash( pNtkTemp );
         Abc_NtkDelete( pNtkTemp );
     }
@@ -6713,7 +6732,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( Abc_NtkIsStrash(pNtk) )
         pNtkTemp = Abc_NtkDup( pNtk );
     else
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
 
     RetValue = Abc_NtkIvyProve( &pNtkTemp, pParams );
 
@@ -6957,7 +6976,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk, 0, 1 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 1, 0 );
         Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
         Abc_NtkDelete( pNtk );
     }
@@ -7050,7 +7069,7 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkQbf( pNtk, nPars, fVerbose );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk, 0, 1 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 1, 0 );
         Abc_NtkQbf( pNtk, nPars, fVerbose );
         Abc_NtkDelete( pNtk );
     }
@@ -7192,7 +7211,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes );
+        pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
         pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
         Abc_NtkDelete( pNtk );
     }
@@ -7772,6 +7791,302 @@ usage:
     return 1;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecStart( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nVars;
+    int nCuts;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nVars = 4;
+    nCuts = 8;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nVars = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nVars < 1 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCuts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCuts < 1 ) 
+                goto usage;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !(nVars >= 3 && nVars <= 16) )
+    {
+        fprintf( pErr, "The range of allowed values is 3 <= K <= 16.\n" );
+        return 0;
+    }
+    if ( Abc_NtkRecIsRunning() )
+    {
+        fprintf( pErr, "The AIG subgraph recording is already started.\n" );
+        return 0;
+    }
+    if ( pNtk && !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for AIGs; run strashing (\"st\").\n" );
+        return 0;
+    }
+    Abc_NtkRecStart( pNtk, nVars, nCuts );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: rec_start [-K num] [-C num] [-h]\n" );
+    fprintf( pErr, "\t         starts recording AIG subgraphs (should be called for\n" );
+    fprintf( pErr, "\t         an empty network or after reading in a previous record)\n" );
+    fprintf( pErr, "\t-K num : the largest number of inputs [default = %d]\n", nVars );
+    fprintf( pErr, "\t-C num : the max number of cuts used at a node (0 < num < 2^12) [default = %d]\n", nCuts );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecStop( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !Abc_NtkRecIsRunning() )
+    {
+        fprintf( pErr, "This command works only after calling \"rec_start\".\n" );
+        return 0;
+    }
+    Abc_NtkRecStop();
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: rec_stop [-h]\n" );
+    fprintf( pErr, "\t        cleans the internal storage for AIG subgraphs\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecAdd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works for AIGs.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkRecIsRunning() )
+    {
+        fprintf( pErr, "This command works for AIGs after calling \"rec_start\".\n" );
+        return 0;
+    }
+    Abc_NtkRecAdd( pNtk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: rec_add [-h]\n" );
+    fprintf( pErr, "\t        adds subgraphs from the current network to the set\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecPs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !Abc_NtkRecIsRunning() )
+    {
+        fprintf( pErr, "This command works for AIGs only after calling \"rec_start\".\n" );
+        return 0;
+    }
+    Abc_NtkRecPs();
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: rec_ps [-h]\n" );
+    fprintf( pErr, "\t        prints statistics about the recorded AIG subgraphs\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecUse( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !Abc_NtkRecIsRunning() )
+    {
+        fprintf( pErr, "This command works for AIGs only after calling \"rec_start\".\n" );
+        return 0;
+    }
+    // get the new network
+    pNtkRes = Abc_NtkRecUse();
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Transforming internal AIG subgraphs into an AIG with choices has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: rec_use [-h]\n" );
+    fprintf( pErr, "\t        transforms internal storage into an AIG with choices\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -7850,7 +8165,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
         if ( pNtk == NULL )
         {
             fprintf( pErr, "Strashing before mapping has failed.\n" );
@@ -8305,7 +8620,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
-        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
         if ( pNtk == NULL )
         {
             fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
@@ -8446,7 +8761,7 @@ int Abc_CommandFpgaFast( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
-        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
         if ( pNtk == NULL )
         {
             fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
@@ -8692,7 +9007,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
-        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
         if ( pNtk == NULL )
         {
             fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
@@ -9301,7 +9616,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
     {
         // strash and balance the network
-        pNtkNew = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtkNew = Abc_NtkStrash( pNtk, 0, 0, 0 );
         if ( pNtkNew == NULL )
         {
             fprintf( pErr, "Strashing before FPGA mapping/retiming has failed.\n" );
@@ -9428,7 +9743,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
     {
         // strash and balance the network
-        pNtkNew = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtkNew = Abc_NtkStrash( pNtk, 0, 0, 0 );
         if ( pNtkNew == NULL )
         {
             fprintf( pErr, "Strashing before SC mapping/retiming has failed.\n" );
@@ -10366,7 +10681,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( Abc_NtkIsStrash(pNtk) )
         pNtkTemp = Abc_NtkDup( pNtk );
     else
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
 
     RetValue = Abc_NtkMiterProve( &pNtkTemp, pParams );
 
diff --git a/src/base/abci/abcDress.c b/src/base/abci/abcDress.c
index cc9ce0b9..f8182532 100644
--- a/src/base/abci/abcDress.c
+++ b/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 );
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 235c3672..c00a7d7c 100644
--- a/src/base/abci/abcDsd.c
+++ b/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;
 }
 
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index daf30331..96c468fe 100644
--- a/src/base/abci/abcFraig.c
+++ b/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" );
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index abcde7ce..d3779277 100644
--- a/src/base/abci/abcIvy.c
+++ b/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 );
     }
 
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 0088d72b..823d81cc 100644
--- a/src/base/abci/abcMiter.c
+++ b/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 );
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
new file mode 100644
index 00000000..a6ec6981
--- /dev/null
+++ b/src/base/abci/abcRec.c
@@ -0,0 +1,1173 @@
+/**CFile****************************************************************
+
+  FileName    [abcRec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Record of semi-canonical AIG subgraphs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcRec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "if.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_ManRec_t_ Abc_ManRec_t;
+struct Abc_ManRec_t_
+{
+    Abc_Ntk_t *       pNtk;          // the record
+    Vec_Ptr_t *       vTtElems;      // the elementary truth tables
+    Vec_Ptr_t *       vTtNodes;      // the node truth tables
+    Abc_Obj_t **      pBins;         // hash table mapping truth tables into nodes
+    int               nBins;         // the number of allocated bins
+    int               nVars;         // the number of variables
+    int               nVarsInit;     // the number of variables requested initially
+    int               nWords;        // the number of TT words
+    int               nCuts;         // the max number of cuts to use
+    // temporaries
+    int *             pBytes;        // temporary storage for minterms
+    int *             pMints;        // temporary storage for minterm counters
+    unsigned *        pTemp1;        // temporary truth table
+    unsigned *        pTemp2;        // temporary truth table
+    Vec_Ptr_t *       vNodes;        // the temporary nodes
+    Vec_Ptr_t *       vTtTemps;      // the truth tables for the internal nodes of the cut
+    Vec_Ptr_t *       vLabels;       // temporary storage for AIG node labels
+    Vec_Str_t *       vCosts;        // temporary storage for costs
+    Vec_Int_t *       vMemory;       // temporary memory for truth tables
+    // statistics
+    int               nTried;        // the number of cuts tried
+    int               nFilterSize;   // the number of same structures
+    int               nFilterRedund; // the number of same structures
+    int               nFilterVolume; // the number of same structures
+    int               nFilterTruth;  // the number of same structures
+    int               nFilterError;  // the number of same structures
+    int               nFilterSame;   // the number of same structures
+    int               nAdded;        // the number of subgraphs added
+    int               nAddedFuncs;   // the number of functions added
+    // rewriting
+    int               nFunsFound;    // the found functions
+    int               nFunsNotFound; // the missing functions 
+    // runtime
+    int               timeCollect;   // the runtime to canonicize
+    int               timeTruth;     // the runtime to canonicize
+    int               timeCanon;     // the runtime to canonicize
+    int               timeOther;     // the runtime to canonicize
+    int               timeTotal;     // the runtime to canonicize
+};
+
+// the truth table is canonicized in such a way that for (00000) its value is 0
+
+static Abc_Obj_t ** Abc_NtkRecTableLookup( Abc_ManRec_t * p, unsigned * pTruth, int nVars );
+static int          Abc_NtkRecComputeTruth( Abc_Obj_t * pObj, Vec_Ptr_t * vTtNodes, int nVars );
+static int          Abc_NtkRecAddCutCheckCycle_rec( Abc_Obj_t * pRoot, Abc_Obj_t * pObj );
+
+static Abc_ManRec_t * s_pMan = NULL;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the record for the given network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecIsRunning()
+{
+    return s_pMan != NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the record for the given network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecVarNum()
+{
+    return (s_pMan != NULL)? s_pMan->nVars : -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the record for the given network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkRecMemory()
+{
+    return s_pMan->vMemory;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the record for the given network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts )
+{
+    Abc_ManRec_t * p;
+    Abc_Obj_t * pObj, ** ppSpot;
+    char Buffer[10];
+    unsigned * pTruth;
+    int i, RetValue;
+    int clkTotal = clock(), clk;
+
+    assert( s_pMan == NULL );
+    if ( pNtk == NULL )
+    {
+        assert( nVars > 2 && nVars <= 16 );
+        pNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+        pNtk->pName = Extra_UtilStrsav( "record" );
+    }
+    else
+    {
+        if ( Abc_NtkGetChoiceNum(pNtk) > 0 )
+        {
+            printf( "The starting record should be a network without choice nodes.\n" );
+            return;
+        }
+        if ( Abc_NtkPiNum(pNtk) > 16 )
+        {
+            printf( "The starting record should be a network with no more than %d primary inputs.\n", 16 );
+            return;
+        }
+        if ( Abc_NtkPiNum(pNtk) > nVars )
+            printf( "The starting record has %d inputs (warning only).\n", Abc_NtkPiNum(pNtk) );
+        pNtk = Abc_NtkDup( pNtk );
+    }
+    // create the primary inputs
+    for ( i = Abc_NtkPiNum(pNtk); i < nVars; i++ )
+    {
+        pObj = Abc_NtkCreatePi( pNtk );
+        Buffer[0] = 'a' + i;
+        Buffer[1] = 0;
+        Abc_ObjAssignName( pObj, Buffer, NULL );
+    }
+    Abc_NtkCleanCopy( pNtk );
+    Abc_NtkCleanEquiv( pNtk );
+
+    // start the manager
+    p = ALLOC( Abc_ManRec_t, 1 );
+    memset( p, 0, sizeof(Abc_ManRec_t) );
+    p->pNtk = pNtk;
+    p->nVars = Abc_NtkPiNum(pNtk);
+    p->nWords = Kit_TruthWordNum( p->nVars );
+    p->nCuts = nCuts;
+    p->nVarsInit = nVars;
+
+    // create elementary truth tables
+    p->vTtElems = Vec_PtrAlloc( 0 ); assert( p->vTtElems->pArray == NULL );
+    p->vTtElems->nSize = p->nVars;
+    p->vTtElems->nCap = p->nVars;
+    p->vTtElems->pArray = (void *)Extra_TruthElementary( p->nVars );        
+
+    // allocate room for node truth tables
+    if ( Abc_NtkObjNum(pNtk) > (1<<14) )
+        p->vTtNodes = Vec_PtrAllocSimInfo( 2 * Abc_NtkObjNum(pNtk), p->nWords );
+    else
+        p->vTtNodes = Vec_PtrAllocSimInfo( 1<<14, p->nWords );
+
+    // create hash table
+    p->nBins = 50011;
+    p->pBins = ALLOC( Abc_Obj_t *, p->nBins );
+    memset( p->pBins, 0, sizeof(Abc_Obj_t *) * p->nBins );
+
+    // set elementary tables
+    Kit_TruthFill( Vec_PtrEntry(p->vTtNodes, 0), p->nVars );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, pObj->Id), Vec_PtrEntry(p->vTtElems, i), p->nVars );
+
+    // compute the tables
+clk = clock();
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        RetValue = Abc_NtkRecComputeTruth( pObj, p->vTtNodes, p->nVars );
+        assert( RetValue );
+    }
+p->timeTruth += clock() - clk;
+
+    // insert the PO nodes into the table
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        p->nTried++;
+        p->nAdded++;
+
+        pObj = Abc_ObjFanin0(pObj);
+        pTruth = Vec_PtrEntry( p->vTtNodes, pObj->Id );
+
+        if ( pTruth[0] == 1128481603 )
+        {
+            int x = 0;
+        }
+
+        // add the resulting truth table to the hash table 
+        ppSpot = Abc_NtkRecTableLookup( p, pTruth, p->nVars );
+        assert( pObj->pEquiv == NULL );
+        assert( pObj->pCopy == NULL );
+        if ( *ppSpot == NULL )
+        {
+            p->nAddedFuncs++;
+            *ppSpot = pObj;
+        }
+        else
+        {
+            pObj->pEquiv = (*ppSpot)->pEquiv;
+            (*ppSpot)->pEquiv = (Hop_Obj_t *)pObj;
+            if ( !Abc_NtkRecAddCutCheckCycle_rec(*ppSpot, pObj) )
+                printf( "Loop!\n" );
+        }
+    }
+
+    // temporaries
+    p->pBytes = ALLOC( int, 4*p->nWords );
+    p->pMints = ALLOC( int, 2*p->nVars );
+    p->pTemp1 = ALLOC( unsigned, p->nWords );
+    p->pTemp2 = ALLOC( unsigned, p->nWords );
+    p->vNodes = Vec_PtrAlloc( 100 );
+    p->vTtTemps = Vec_PtrAllocSimInfo( 64, p->nWords );
+    p->vMemory = Vec_IntAlloc( Abc_TruthWordNum(p->nVars) * 1000 );
+
+    // set the manager
+    s_pMan = p;
+p->timeTotal += clock() - clkTotal;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the given record.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecStop()
+{
+    assert( s_pMan != NULL );
+    if ( s_pMan->pNtk )
+        Abc_NtkDelete( s_pMan->pNtk );
+    Vec_PtrFree( s_pMan->vTtNodes );
+    Vec_PtrFree( s_pMan->vTtElems );
+    free( s_pMan->pBins );
+
+    // temporaries
+    free( s_pMan->pBytes );
+    free( s_pMan->pMints );
+    free( s_pMan->pTemp1 );
+    free( s_pMan->pTemp2 );
+    Vec_PtrFree( s_pMan->vNodes );
+    Vec_PtrFree( s_pMan->vTtTemps );
+    if ( s_pMan->vLabels )
+        Vec_PtrFree( s_pMan->vLabels );
+    if ( s_pMan->vCosts )
+        Vec_StrFree( s_pMan->vCosts );
+    Vec_IntFree( s_pMan->vMemory );
+
+    free( s_pMan );
+    s_pMan = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the given record.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkRecUse()
+{
+    Abc_ManRec_t * p = s_pMan;
+    Abc_Ntk_t * pNtk = p->pNtk;
+    assert( p != NULL );
+    Abc_NtkRecPs();
+    p->pNtk = NULL;
+    Abc_NtkRecStop();
+    return pNtk;
+}
+
+static inline void Abc_ObjSetMax( Abc_Obj_t * pObj, int Value ) { assert( pObj->Level < 0xff ); pObj->Level = (Value << 8) | (pObj->Level & 0xff); }
+static inline void Abc_ObjClearMax( Abc_Obj_t * pObj )          { pObj->Level = (pObj->Level & 0xff); }
+static inline int  Abc_ObjGetMax( Abc_Obj_t * pObj )            { return (pObj->Level >> 8) & 0xff; }
+
+/**Function*************************************************************
+
+  Synopsis    [Print statistics about the current record.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecPs()
+{
+    int Counter, Counters[17] = {0};
+    int CounterS, CountersS[17] = {0};
+    Abc_ManRec_t * p = s_pMan;
+    Abc_Ntk_t * pNtk = p->pNtk;
+    Abc_Obj_t * pObj, * pEntry, * pTemp;
+    int i;
+
+    // set the max PI number
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_ObjSetMax( pObj, i+1 );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        Abc_ObjSetMax( pObj, ABC_MAX( Abc_ObjGetMax(Abc_ObjFanin0(pObj)), Abc_ObjGetMax(Abc_ObjFanin1(pObj)) ) );
+    // go through the table
+    Counter = CounterS = 0;
+    for ( i = 0; i < p->nBins; i++ )
+    for ( pEntry = p->pBins[i]; pEntry; pEntry = pEntry->pCopy )
+    {
+        Counters[ Abc_ObjGetMax(pEntry) ]++;
+        Counter++;
+        for ( pTemp = pEntry; pTemp; pTemp = (Abc_Obj_t *)pTemp->pEquiv )
+        {
+            assert( Abc_ObjGetMax(pTemp) == Abc_ObjGetMax(pEntry) );
+            CountersS[ Abc_ObjGetMax(pTemp) ]++;
+            CounterS++;
+        }
+    }
+//    printf( "Functions = %d. Expected = %d.\n", Counter, p->nAddedFuncs );
+//    printf( "Subgraphs = %d. Expected = %d.\n", CounterS, p->nAdded );
+    assert( Counter == p->nAddedFuncs );
+    assert( CounterS == p->nAdded );
+
+    // clean
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        Abc_ObjClearMax( pObj );
+    }
+
+    printf( "The record with %d AND nodes in %d subgraphs for %d functions with %d inputs:\n", 
+        Abc_NtkNodeNum(pNtk), Abc_NtkPoNum(pNtk), p->nAddedFuncs, Abc_NtkPiNum(pNtk) );
+    for ( i = 0; i <= 16; i++ )
+    {
+        if ( Counters[i] )
+            printf( "Inputs = %2d.  Funcs = %8d.  Subgrs = %8d.  Ratio = %6.2f.\n", i, Counters[i], CountersS[i], 1.0*CountersS[i]/Counters[i] );
+    }
+
+    printf( "Subgraphs tried                             = %8d. (%6.2f %%)\n", p->nTried,        !p->nTried? 0 : 100.0*p->nTried/p->nTried );
+    printf( "Subgraphs filtered by support size          = %8d. (%6.2f %%)\n", p->nFilterSize,   !p->nTried? 0 : 100.0*p->nFilterSize/p->nTried );
+    printf( "Subgraphs filtered by structural redundancy = %8d. (%6.2f %%)\n", p->nFilterRedund, !p->nTried? 0 : 100.0*p->nFilterRedund/p->nTried );
+    printf( "Subgraphs filtered by volume                = %8d. (%6.2f %%)\n", p->nFilterVolume, !p->nTried? 0 : 100.0*p->nFilterVolume/p->nTried );
+    printf( "Subgraphs filtered by TT redundancy         = %8d. (%6.2f %%)\n", p->nFilterTruth,  !p->nTried? 0 : 100.0*p->nFilterTruth/p->nTried );
+    printf( "Subgraphs filtered by error                 = %8d. (%6.2f %%)\n", p->nFilterError,  !p->nTried? 0 : 100.0*p->nFilterError/p->nTried );
+    printf( "Subgraphs filtered by isomorphism           = %8d. (%6.2f %%)\n", p->nFilterSame,   !p->nTried? 0 : 100.0*p->nFilterSame/p->nTried );
+    printf( "Subgraphs added                             = %8d. (%6.2f %%)\n", p->nAdded,        !p->nTried? 0 : 100.0*p->nAdded/p->nTried );
+    printf( "Functions added                             = %8d. (%6.2f %%)\n", p->nAddedFuncs,   !p->nTried? 0 : 100.0*p->nAddedFuncs/p->nTried );
+
+    p->timeOther = p->timeTotal - p->timeCollect - p->timeTruth - p->timeCanon;
+    PRTP( "Collecting nodes ", p->timeCollect, p->timeTotal );
+    PRTP( "Computing truth  ", p->timeTruth, p->timeTotal );
+    PRTP( "Canonicizing     ", p->timeCanon, p->timeTotal );
+    PRTP( "Other            ", p->timeOther, p->timeTotal );
+    PRTP( "TOTAL            ", p->timeTotal, p->timeTotal );
+    if ( p->nFunsFound )
+    printf( "During rewriting found = %d and not found = %d functions.\n", p->nFunsFound, p->nFunsNotFound );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Filters the current record.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecFilter( int iVar, int iPlus )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the hash key.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Abc_NtkRecTableHash( unsigned * pTruth, int nVars, int nBins, int * pPrimes )
+{
+    int i, nWords = Kit_TruthWordNum( nVars );
+    unsigned uHash = 0;
+    for ( i = 0; i < nWords; i++ )
+        uHash ^= pTruth[i] * pPrimes[i & 0x7];
+    return uHash % nBins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the given record.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t ** Abc_NtkRecTableLookup( Abc_ManRec_t * p, unsigned * pTruth, int nVars )
+{
+    static int s_Primes[10] = { 1291, 1699, 2357, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
+    Abc_Obj_t ** ppSpot, * pEntry;
+    ppSpot = p->pBins + Abc_NtkRecTableHash( pTruth, nVars, p->nBins, s_Primes );
+    for ( pEntry = *ppSpot; pEntry; ppSpot = &pEntry->pCopy, pEntry = pEntry->pCopy )
+        if ( Kit_TruthIsEqualWithPhase(Vec_PtrEntry(p->vTtNodes, pEntry->Id), pTruth, nVars) )
+            return ppSpot;
+    return ppSpot;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecComputeTruth( Abc_Obj_t * pObj, Vec_Ptr_t * vTtNodes, int nVars )
+{
+    unsigned * pTruth, * pTruth0, * pTruth1;
+    int RetValue;
+    assert( Abc_ObjIsNode(pObj) );
+    pTruth  = Vec_PtrEntry( vTtNodes, pObj->Id );
+    pTruth0 = Vec_PtrEntry( vTtNodes, Abc_ObjFaninId0(pObj) );
+    pTruth1 = Vec_PtrEntry( vTtNodes, Abc_ObjFaninId1(pObj) );
+    Kit_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+    assert( (pTruth[0] & 1) == pObj->fPhase );
+    RetValue = ((pTruth[0] & 1) == pObj->fPhase);
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs renoding as technology mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecAdd( Abc_Ntk_t * pNtk )
+{
+    extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
+    extern int Abc_NtkRecAddCut( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut );
+
+    If_Par_t Pars, * pPars = &Pars;
+    Abc_Ntk_t * pNtkNew;
+    int clk = clock();
+
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Performing renoding with choices.\n" );
+
+    // set defaults
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+    pPars->nLutSize    =  s_pMan->nVarsInit;
+    pPars->nCutsMax    =  s_pMan->nCuts;
+    pPars->nFlowIters  =  0;
+    pPars->nAreaIters  =  0;
+    pPars->DelayTarget = -1;
+    pPars->fPreprocess =  0;
+    pPars->fArea       =  1;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  0; 
+    pPars->fLatchPaths =  0;
+    pPars->fSeqMap     =  0;
+    pPars->fVerbose    =  0;
+    // internal parameters
+    pPars->fTruth      =  0;
+    pPars->fUsePerm    =  0; 
+    pPars->nLatches    =  0;
+    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->fUseBdds    =  0;
+    pPars->fUseSops    =  0;
+    pPars->fUseCnfs    =  0;
+    pPars->fUseMv      =  0;
+    pPars->pFuncCost   =  NULL;
+    pPars->pFuncUser   =  Abc_NtkRecAddCut;
+
+    // perform recording
+    pNtkNew = Abc_NtkIf( pNtk, pPars );
+    Abc_NtkDelete( pNtkNew );
+s_pMan->timeTotal += clock() - clk;
+
+//    if ( !Abc_NtkCheck( s_pMan->pNtk ) )
+//        printf( "Abc_NtkRecAdd: The network check has failed.\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cut function to the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecCollectNodes_rec( If_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    if ( pNode->fMark )
+        return;
+    pNode->fMark = 1;
+    assert( If_ObjIsAnd(pNode) );
+    Abc_NtkRecCollectNodes_rec( If_ObjFanin0(pNode), vNodes );
+    Abc_NtkRecCollectNodes_rec( If_ObjFanin1(pNode), vNodes );
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cut function to the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecCollectNodes( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut, Vec_Ptr_t * vNodes )
+{
+    If_Obj_t * pLeaf;
+    int i, RetValue = 1;
+
+    // collect the internal nodes of the cut
+    Vec_PtrClear( vNodes );
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+    {
+        Vec_PtrPush( vNodes, pLeaf );
+        assert( pLeaf->fMark == 0 );
+        pLeaf->fMark = 1;
+    }
+
+    // collect other nodes
+    Abc_NtkRecCollectNodes_rec( pRoot, vNodes );
+
+    // check if there are leaves, such that both of their fanins are marked
+    // this indicates a redundant cut
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+    {
+        if ( !If_ObjIsAnd(pLeaf) )
+            continue;
+        if ( If_ObjFanin0(pLeaf)->fMark && If_ObjFanin1(pLeaf)->fMark )
+        {
+            RetValue = 0;
+            break;
+        }
+    }
+
+    // clean the mark
+    Vec_PtrForEachEntry( vNodes, pLeaf, i )
+        pLeaf->fMark = 0;
+/*
+    if ( pRoot->Id == 2639 )
+    {
+        // print the cut
+        Vec_PtrForEachEntry( vNodes, pLeaf, i )
+        {
+            if ( If_ObjIsAnd(pLeaf) )
+                printf( "%4d = %c%4d & %c%4d\n", pLeaf->Id, 
+                    (If_ObjFaninC0(pLeaf)? '-':'+'), If_ObjFanin0(pLeaf)->Id, 
+                    (If_ObjFaninC1(pLeaf)? '-':'+'), If_ObjFanin1(pLeaf)->Id ); 
+            else
+                printf( "%4d = pi\n", pLeaf->Id ); 
+        }
+        printf( "\n" );
+    }
+*/
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth tables of nodes in the cut.]
+
+  Description [Returns 0 if the TT does not depend on some cut variables.
+  Or if the TT can be expressed simpler using other nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecCutTruth( Vec_Ptr_t * vNodes, int nLeaves, Vec_Ptr_t * vTtTemps, Vec_Ptr_t * vTtElems )
+{
+    unsigned * pSims, * pSims0, * pSims1;
+    unsigned * pTemp = s_pMan->pTemp2;
+    unsigned uWord;
+    If_Obj_t * pObj, * pObj2, * pRoot;
+    int i, k, nLimit, nInputs = s_pMan->nVars;
+
+    assert( Vec_PtrSize(vNodes) > nLeaves );
+
+    // set the elementary truth tables and compute the truth tables of the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        pObj->pCopy = Vec_PtrEntry(vTtTemps, i);
+        pSims = (unsigned *)pObj->pCopy;
+        if ( i < nLeaves )
+        {
+            Kit_TruthCopy( pSims, Vec_PtrEntry(vTtElems, i), nInputs );
+            continue;
+        }
+        assert( If_ObjIsAnd(pObj) );
+        // get hold of the simulation information
+        pSims0 = (unsigned *)If_ObjFanin0(pObj)->pCopy;
+        pSims1 = (unsigned *)If_ObjFanin1(pObj)->pCopy;
+        // simulate the node
+        Kit_TruthAndPhase( pSims, pSims0, pSims1, nInputs, If_ObjFaninC0(pObj), If_ObjFaninC1(pObj) );
+    }
+
+    // check the support size
+    pRoot = Vec_PtrEntryLast( vNodes );
+    pSims = (unsigned *)pRoot->pCopy;
+    if ( Kit_TruthSupport(pSims, nInputs) != Kit_BitMask(nLeaves) )
+        return 0;
+
+    // make sure none of the nodes has the same simulation info as the output
+    // check pairwise comparisons
+    nLimit = Vec_PtrSize(vNodes) - 1;
+    Vec_PtrForEachEntryStop( vNodes, pObj, i, nLimit )
+    {
+        pSims0 = (unsigned *)pObj->pCopy;
+        if ( Kit_TruthIsEqualWithPhase(pSims, pSims0, nInputs) )
+            return 0;
+        Vec_PtrForEachEntryStop( vNodes, pObj2, k, i )
+        {
+            if ( (If_ObjFanin0(pRoot) == pObj && If_ObjFanin1(pRoot) == pObj2) ||
+                 (If_ObjFanin1(pRoot) == pObj && If_ObjFanin0(pRoot) == pObj2) )
+                 continue;
+            pSims1 = (unsigned *)pObj2->pCopy;
+
+            uWord = pSims0[0] & pSims1[0];
+            if ( pSims[0] == uWord || pSims[0] == ~uWord )
+            {
+                Kit_TruthAndPhase( pTemp, pSims0, pSims1, nInputs, 0, 0 );
+                if ( Kit_TruthIsEqualWithPhase(pSims, pTemp, nInputs) )
+                    return 0;
+            }
+
+            uWord = pSims0[0] & ~pSims1[0];
+            if ( pSims[0] == uWord || pSims[0] == ~uWord )
+            {
+                Kit_TruthAndPhase( pTemp, pSims0, pSims1, nInputs, 0, 1 );
+                if ( Kit_TruthIsEqualWithPhase(pSims, pTemp, nInputs) )
+                    return 0;
+            }
+
+            uWord = ~pSims0[0] & pSims1[0];
+            if ( pSims[0] == uWord || pSims[0] == ~uWord )
+            {
+                Kit_TruthAndPhase( pTemp, pSims0, pSims1, nInputs, 1, 0 );
+                if ( Kit_TruthIsEqualWithPhase(pSims, pTemp, nInputs) )
+                    return 0;
+            }
+
+            uWord = ~pSims0[0] & ~pSims1[0];
+            if ( pSims[0] == uWord || pSims[0] == ~uWord )
+            {
+                Kit_TruthAndPhase( pTemp, pSims0, pSims1, nInputs, 1, 1 );
+                if ( Kit_TruthIsEqualWithPhase(pSims, pTemp, nInputs) )
+                    return 0;
+            }
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cut function to the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecAddCutCheckCycle_rec( Abc_Obj_t * pRoot, Abc_Obj_t * pObj )
+{
+    assert( pRoot->Level > 0 );
+    if ( pObj->Level < pRoot->Level )
+        return 1;
+    if ( pObj == pRoot )
+        return 0;
+    if ( !Abc_NtkRecAddCutCheckCycle_rec(pRoot, Abc_ObjFanin0(pObj)) )
+        return 0;
+    if ( !Abc_NtkRecAddCutCheckCycle_rec(pRoot, Abc_ObjFanin1(pObj)) )
+        return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cut function to the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecAddCut( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
+{
+    static int s_MaxSize[16] = { 0 };
+    char Buffer[40], Name[20], Truth[20];
+    char pCanonPerm[16];
+    Abc_Obj_t * pObj, * pFanin0, * pFanin1, ** ppSpot, * pObjPo;
+    Abc_Ntk_t * pAig = s_pMan->pNtk;
+    If_Obj_t * pIfObj;
+    Vec_Ptr_t * vNodes = s_pMan->vNodes;
+    unsigned * pInOut = s_pMan->pTemp1;
+    unsigned * pTemp = s_pMan->pTemp2;
+    unsigned * pTruth;
+    int i, RetValue, nNodes, nNodesBeg, nInputs = s_pMan->nVars, nLeaves = If_CutLeaveNum(pCut);
+    unsigned uCanonPhase;
+    int clk;
+
+    if ( pRoot->Id == 2639 )
+    {
+        int y = 0;
+    }
+
+    assert( nInputs <= 16 );
+    assert( nInputs == (int)pCut->nLimit );
+    s_pMan->nTried++;
+
+    // skip small cuts
+    if ( nLeaves < 3 )
+    {
+        s_pMan->nFilterSize++;
+        return 1;
+    }
+
+    // collect internal nodes and skip redundant cuts
+clk = clock();
+    RetValue = Abc_NtkRecCollectNodes( pIfMan, pRoot, pCut, vNodes );
+s_pMan->timeCollect += clock() - clk;
+    if ( !RetValue )
+    {
+        s_pMan->nFilterRedund++;
+        return 1;
+    }
+
+    // skip cuts with very large volume
+    if ( Vec_PtrSize(vNodes) > nLeaves + 3*(nLeaves-1) + s_MaxSize[nLeaves] )
+    {
+        s_pMan->nFilterVolume++;
+        return 1;
+    }
+
+    // compute truth table and skip the redundant structures
+clk = clock();
+    RetValue = Abc_NtkRecCutTruth( vNodes, nLeaves, s_pMan->vTtTemps, s_pMan->vTtElems );
+s_pMan->timeTruth += clock() - clk;
+    if ( !RetValue )
+    {
+        s_pMan->nFilterTruth++;
+        return 1;
+    }
+
+    // copy the truth table
+    Kit_TruthCopy( pInOut, (unsigned *)pRoot->pCopy, nInputs );
+
+    // set permutation
+    for ( i = 0; i < nInputs; i++ )
+        pCanonPerm[i] = i;
+
+    // semi-canonicize the truth table
+clk = clock();
+    uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nInputs, pCanonPerm, (short *)s_pMan->pMints );
+s_pMan->timeCanon += clock() - clk;
+    // pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
+
+    // go through the variables in the new truth table
+    for ( i = 0; i < nLeaves; i++ )
+    {
+        // get hold of the corresponding leaf
+        pIfObj = If_ManObj( pIfMan, pCut->pLeaves[pCanonPerm[i]] );
+        // get hold of the corresponding new node
+        pObj = Abc_NtkPi( pAig, i );
+        pObj = Abc_ObjNotCond( pObj, (uCanonPhase & (1 << i)) );
+        // map them
+        pIfObj->pCopy = pObj;
+/*
+        if ( pRoot->Id == 2639 )
+        {
+            unsigned uSupp;
+            printf( "Node %6d : ", pIfObj->Id );
+            printf( "Support " );
+            uSupp = Kit_TruthSupport(Vec_PtrEntry( s_pMan->vTtNodes, Abc_ObjRegular(pObj)->Id ), nInputs);
+            Extra_PrintBinary( stdout, &uSupp, nInputs ); 
+            printf( "   " );
+            Extra_PrintBinary( stdout, Vec_PtrEntry( s_pMan->vTtNodes, Abc_ObjRegular(pObj)->Id ), 1<<6 ); 
+            printf( "\n" );
+        }
+*/
+    }
+
+    // build the node and compute its truth table
+    nNodesBeg = Abc_NtkObjNumMax( pAig );
+    Vec_PtrForEachEntryStart( vNodes, pIfObj, i, nLeaves )
+    {
+        pFanin0 = Abc_ObjNotCond( If_ObjFanin0(pIfObj)->pCopy, If_ObjFaninC0(pIfObj) );
+        pFanin1 = Abc_ObjNotCond( If_ObjFanin1(pIfObj)->pCopy, If_ObjFaninC1(pIfObj) );
+
+        nNodes = Abc_NtkObjNumMax( pAig );
+        pObj = Abc_AigAnd( pAig->pManFunc, pFanin0, pFanin1 );
+        assert( !Abc_ObjIsComplement(pObj) );
+        pIfObj->pCopy = pObj;
+
+        if ( pObj->Id == nNodes )
+        {
+            // increase storage for truth tables
+            if ( Vec_PtrSize(s_pMan->vTtNodes) <= pObj->Id )
+                Vec_PtrDoubleSimInfo(s_pMan->vTtNodes);
+            // compute the truth table
+            RetValue = Abc_NtkRecComputeTruth( pObj, s_pMan->vTtNodes, nInputs );
+            if ( RetValue == 0 )
+            {
+                s_pMan->nFilterError++;
+                printf( "T" );
+                return 1;
+            }
+        }
+    }
+
+    pTruth = Vec_PtrEntry( s_pMan->vTtNodes, pObj->Id );
+    if ( Kit_TruthSupport(pTruth, nInputs) != Kit_BitMask(nLeaves) )
+    {
+        s_pMan->nFilterError++;
+        printf( "S" );
+        return 1;
+    }
+
+    // compare the truth tables
+    if ( !Kit_TruthIsEqualWithPhase( pTruth, pInOut, nInputs ) )
+    {
+        s_pMan->nFilterError++;
+        printf( "F" );
+        return 1;
+    }
+//    Extra_PrintBinary( stdout, pInOut, 8 ); printf( "\n" );
+
+    // if not new nodes were added and the node has a CO fanout
+    if ( nNodesBeg == Abc_NtkObjNumMax(pAig) && Abc_NodeFindCoFanout(pObj) != NULL )
+    {
+        s_pMan->nFilterSame++;
+        return 1;
+    }
+    s_pMan->nAdded++;
+
+    // create PO for this node
+    pObjPo = Abc_NtkCreatePo(pAig);
+    Abc_ObjAddFanin( pObjPo, pObj );
+
+    // assign the name to this PO
+    sprintf( Name, "%d_%06d", nLeaves, Abc_NtkPoNum(pAig) );
+    if ( (nInputs <= 6) && 0 )
+    {
+        Extra_PrintHexadecimalString( Truth, pInOut, nInputs );
+        sprintf( Buffer, "%s_%s", Name, Truth );
+    }
+    else
+    {
+        sprintf( Buffer, "%s", Name );
+    }
+    Abc_ObjAssignName( pObjPo, Buffer, NULL );
+
+    // add the resulting truth table to the hash table 
+    ppSpot = Abc_NtkRecTableLookup( s_pMan, pTruth, nInputs );
+    assert( pObj->pEquiv == NULL );
+    assert( pObj->pCopy == NULL );
+    if ( *ppSpot == NULL )
+    {
+        s_pMan->nAddedFuncs++;
+        *ppSpot = pObj;
+    }
+    else
+    {
+        pObj->pEquiv = (*ppSpot)->pEquiv;
+        (*ppSpot)->pEquiv = (Hop_Obj_t *)pObj;
+        if ( !Abc_NtkRecAddCutCheckCycle_rec(*ppSpot, pObj) )
+            printf( "Loop!\n" );
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Labels the record AIG with the corresponding new AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkRecStrashNodeLabel_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fBuild, Vec_Ptr_t * vLabels )
+{
+    Abc_Obj_t * pFanin0New, * pFanin1New, * pLabel;
+    assert( !Abc_ObjIsComplement(pObj) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pObj ) )
+        return Vec_PtrEntry( vLabels, pObj->Id );
+    assert( Abc_ObjIsNode(pObj) );
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pObj );
+    // label the fanins
+    pFanin0New = Abc_NtkRecStrashNodeLabel_rec( pNtkNew, Abc_ObjFanin0(pObj), fBuild, vLabels );
+    pFanin1New = Abc_NtkRecStrashNodeLabel_rec( pNtkNew, Abc_ObjFanin1(pObj), fBuild, vLabels );
+    // label the node if possible
+    pLabel = NULL;
+    if ( pFanin0New && pFanin1New )
+    {
+        pFanin0New = Abc_ObjNotCond( pFanin0New, Abc_ObjFaninC0(pObj) );
+        pFanin1New = Abc_ObjNotCond( pFanin1New, Abc_ObjFaninC1(pObj) );
+        if ( fBuild )
+            pLabel = Abc_AigAnd( pNtkNew->pManFunc, pFanin0New, pFanin1New );
+        else
+            pLabel = Abc_AigAndLookup( pNtkNew->pManFunc, pFanin0New, pFanin1New );
+    }
+    Vec_PtrWriteEntry( vLabels, pObj->Id, pLabel );
+    return pLabel;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the area of the given node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecStrashNodeCount_rec( Abc_Obj_t * pObj, Vec_Str_t * vCosts, Vec_Ptr_t * vLabels )
+{
+    int Cost0, Cost1;
+    if ( Vec_PtrEntry( vLabels, pObj->Id ) )
+        return 0;
+    assert( Abc_ObjIsNode(pObj) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pObj ) )
+        return Vec_StrEntry( vCosts, pObj->Id );
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pObj );
+    // count for the fanins
+    Cost0 = Abc_NtkRecStrashNodeCount_rec( Abc_ObjFanin0(pObj), vCosts, vLabels );
+    Cost1 = Abc_NtkRecStrashNodeCount_rec( Abc_ObjFanin1(pObj), vCosts, vLabels );
+    Vec_StrWriteEntry( vCosts, pObj->Id, (char)(Cost0 + Cost1 + 1) );
+    return Cost0 + Cost1 + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes the given node using its local function.]
+
+  Description [Assumes that the fanins are already strashed.
+  Returns 0 if the function is not found in the table.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars )
+{
+    char pCanonPerm[16];
+    Abc_Ntk_t * pAig = s_pMan->pNtk;
+    unsigned * pInOut = s_pMan->pTemp1;
+    unsigned * pTemp = s_pMan->pTemp2;
+    unsigned * pTruthRec;
+    Abc_Obj_t * pCand, * pCandMin, * pLeaf, * pFanin, ** ppSpot;
+    unsigned uCanonPhase;
+    int i, nLeaves, CostMin, Cost, nOnes, fCompl;
+
+    // check if the record works
+    nLeaves = Abc_ObjFaninNum(pObj);
+    assert( nLeaves >= 3 && nLeaves <= s_pMan->nVars );
+    pFanin = Abc_ObjFanin0(pObj);
+    assert( Abc_ObjRegular(pFanin->pCopy)->pNtk == pNtkNew );
+    assert( s_pMan != NULL );
+    assert( nVars == s_pMan->nVars );
+
+    // copy the truth table
+    Kit_TruthCopy( pInOut, pTruth, nVars );
+
+    // set permutation
+    for ( i = 0; i < nVars; i++ )
+        pCanonPerm[i] = i;
+
+    // canonicize the truth table
+    uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nVars, pCanonPerm, (short *)s_pMan->pMints );
+
+    // get hold of the curresponding class
+    ppSpot = Abc_NtkRecTableLookup( s_pMan, pInOut, nVars );
+    if ( *ppSpot == NULL )
+    {
+        s_pMan->nFunsNotFound++;        
+//        printf( "The class of a function with %d inputs is not found.\n", nLeaves );
+        return 0;
+    }
+    s_pMan->nFunsFound++;        
+
+    // make sure the truth table is the same
+    pTruthRec = Vec_PtrEntry( s_pMan->vTtNodes, (*ppSpot)->Id );
+    if ( !Kit_TruthIsEqualWithPhase( pTruthRec, pInOut, nVars ) )
+    {
+        assert( 0 );
+        return 0;
+    }
+
+
+    // allocate storage for costs
+    if ( s_pMan->vLabels && Vec_PtrSize(s_pMan->vLabels) < Abc_NtkObjNumMax(pAig) )
+    {
+        Vec_PtrFree( s_pMan->vLabels );
+        s_pMan->vLabels = NULL;
+    }
+    if ( s_pMan->vLabels == NULL )
+        s_pMan->vLabels = Vec_PtrStart( Abc_NtkObjNumMax(pAig) );
+
+    // go through the variables in the new truth table
+    Abc_NtkIncrementTravId( pAig );
+    for ( i = 0; i < nLeaves; i++ )
+    {
+        // get hold of the corresponding fanin
+        pFanin = Abc_ObjFanin( pObj, pCanonPerm[i] )->pCopy;
+        pFanin = Abc_ObjNotCond( pFanin, (uCanonPhase & (1 << i)) );
+        // label the PI of the AIG subgraphs with this fanin
+        pLeaf = Abc_NtkPi( pAig, i );
+        Vec_PtrWriteEntry( s_pMan->vLabels, pLeaf->Id, pFanin );
+        Abc_NodeSetTravIdCurrent( pLeaf );
+    }
+
+    // go through the candidates - and recursively label them
+    for ( pCand = *ppSpot; pCand; pCand = (Abc_Obj_t *)pCand->pEquiv )
+        Abc_NtkRecStrashNodeLabel_rec( pNtkNew, pCand, 0, s_pMan->vLabels );
+
+
+    // allocate storage for costs
+    if ( s_pMan->vCosts && Vec_StrSize(s_pMan->vCosts) < Abc_NtkObjNumMax(pAig) )
+    {
+        Vec_StrFree( s_pMan->vCosts );
+        s_pMan->vCosts = NULL;
+    }
+    if ( s_pMan->vCosts == NULL )
+        s_pMan->vCosts = Vec_StrStart( Abc_NtkObjNumMax(pAig) );
+
+    // find the best subgraph
+    CostMin = ABC_INFINITY;
+    pCandMin = NULL;
+    for ( pCand = *ppSpot; pCand; pCand = (Abc_Obj_t *)pCand->pEquiv )
+    {
+        // label the leaves
+        Abc_NtkIncrementTravId( pAig );
+        // count the number of non-labeled nodes
+        Cost = Abc_NtkRecStrashNodeCount_rec( pCand, s_pMan->vCosts, s_pMan->vLabels );
+        if ( CostMin > Cost )
+        {
+//            printf( "%d ", Cost );
+            CostMin = Cost;
+            pCandMin = pCand;
+        }
+    }
+//    printf( "\n" );
+    assert( pCandMin != NULL );
+    if ( pCandMin == NULL )
+        return 0;
+
+
+    // label the leaves
+    Abc_NtkIncrementTravId( pAig );
+    for ( i = 0; i < nLeaves; i++ )
+        Abc_NodeSetTravIdCurrent( Abc_NtkPi(pAig, i) );
+
+    // implement the subgraph
+    pObj->pCopy = Abc_NtkRecStrashNodeLabel_rec( pNtkNew, pCandMin, 1, s_pMan->vLabels );
+    assert( Abc_ObjRegular(pObj->pCopy)->pNtk == pNtkNew );
+
+    // determine phase difference
+    nOnes = Kit_TruthCountOnes(pTruth, nVars);
+    fCompl = (nOnes > (1<< nVars)/2);
+//    assert( fCompl == ((uCanonPhase & (1 << nVars)) > 0) );
+
+    nOnes = Kit_TruthCountOnes(pTruthRec, nVars);
+    fCompl ^= (nOnes > (1<< nVars)/2);
+    // complement
+    pObj->pCopy = Abc_ObjNotCond( pObj->pCopy, fCompl );
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 6423d10c..8e8e8719 100644
--- a/src/base/abci/abcRenode.c
+++ b/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 )
     {
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 00a94bec..4f48f3bf 100644
--- a/src/base/abci/abcStrash.c
+++ b/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;
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 4791c859..43ddb4fd 100644
--- a/src/base/abci/abcSweep.c
+++ b/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 )
     {
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 1054e071..d4b15d59 100644
--- a/src/base/abci/abcVerify.c
+++ b/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 );
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 71a47ec0..acac466b 100644
--- a/src/base/abci/module.make
+++ b/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 \
diff --git a/src/base/io/io.c b/src/base/io/io.c
index a7801f71..f0dabeb9 100644
--- a/src/base/io/io.c
+++ b/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 )
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index b8b3b83b..4b766a47 100644
--- a/src/base/io/ioWriteBench.c
+++ b/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 )
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index cc9e569a..19889fc4 100644
--- a/src/base/ver/verCore.c
+++ b/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") )
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 759a9801..a440d7ea 100644
--- a/src/map/if/if.h
+++ b/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
 };
 
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 7423bd05..e3f0dfda 100644
--- a/src/map/if/ifMap.c
+++ b/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 );
 }
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 4aa2c816..06ba309d 100644
--- a/src/misc/extra/extra.h
+++ b/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 ================================================================*/
 
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index 6b130e7e..4c51b8b5 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/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;
diff --git a/src/misc/extra/extraUtilTruth.c b/src/misc/extra/extraUtilTruth.c
index 7a22545b..3b0b16eb 100644
--- a/src/misc/extra/extraUtilTruth.c
+++ b/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).
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 6b23d1ac..a53e439a 100644
--- a/src/misc/vec/vecPtr.h
+++ b/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 []
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index 5d37a9e9..d779df7b 100644
--- a/src/opt/kit/kit.h
+++ b/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 );
 
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index 0068a29a..b85aa4a4 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -40,23 +40,23 @@ typedef enum {
 
 struct Dsd_Obj_t_
 { 
-    unsigned       uSupp;              // the support of this node
-    unsigned       Id          :  6;   // the number of this node
-    unsigned       Type        :  3;   // none, const, var, AND, XOR, MUX, PRIME
-    unsigned       fMark       :  1;   // finished checking output
-    unsigned       Offset      : 16;   // offset to the truth table
-    unsigned       nFans       :  6;   // the number of fanins of this node
-    unsigned char  pFans[0];           // the fanin literals
+    unsigned       Id         : 6;  // the number of this node
+    unsigned       Type       : 3;  // none, const, var, AND, XOR, MUX, PRIME
+    unsigned       fMark      : 1;  // finished checking output
+    unsigned       Offset     : 8;  // offset to the truth table
+    unsigned       nRefs      : 8;  // offset to the truth table
+    unsigned       nFans      : 6;  // the number of fanins of this node
+    unsigned char  pFans[0];        // the fanin literals
 };
 
 struct Dsd_Ntk_t_
 {
-    unsigned char  nVars;              // at most 16 (perhaps 18?)
-    unsigned char  nNodesAlloc;        // the number of allocated nodes (at most nVars)
-    unsigned char  nNodes;             // the number of nodes
-    unsigned char  Root;               // the root of the tree
-    unsigned *     pMem;               // memory for the truth tables (memory manager?)
-    Dsd_Obj_t *    pNodes[0];          // the nodes
+    unsigned char  nVars;           // at most 16 (perhaps 18?)
+    unsigned char  nNodesAlloc;     // the number of allocated nodes (at most nVars)
+    unsigned char  nNodes;          // the number of nodes
+    unsigned char  Root;            // the root of the tree
+    unsigned *     pMem;            // memory for the truth tables (memory manager?)
+    Dsd_Obj_t *    pNodes[0];       // the nodes
 };
 
 static inline unsigned     Dsd_ObjOffset( int nFans )        { return (nFans >> 2) + ((nFans & 3) > 0); }
@@ -93,8 +93,8 @@ Dsd_Obj_t * Dsd_ObjAlloc( Dsd_Ntk_t * pNtk, Kit_Dsd_t Type, int nFans )
     int nSize = sizeof(Dsd_Obj_t) + sizeof(unsigned) * (Dsd_ObjOffset(nFans) + (Type == KIT_DSD_PRIME) * Kit_TruthWordNum(nFans));
     pObj = (Dsd_Obj_t *)ALLOC( char, nSize );
     memset( pObj, 0, nSize );
-    pObj->Type = Type;
     pObj->Id = pNtk->nVars + pNtk->nNodes;
+    pObj->Type = Type;
     pObj->nFans = nFans;
     pObj->Offset = Dsd_ObjOffset( nFans );
     // add the object
@@ -298,34 +298,32 @@ int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * pPar )
+void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, unsigned char * pPar )
 {
     Dsd_Obj_t * pRes, * pRes0, * pRes1;
     int nWords = Kit_TruthWordNum(pObj->nFans);
     unsigned * pTruth = Dsd_ObjTruth(pObj);
     unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + nWords };
     unsigned * pCofs4[2][2] = { {pNtk->pMem + 2 * nWords, pNtk->pMem + 3 * nWords}, {pNtk->pMem + 4 * nWords, pNtk->pMem + 5 * nWords} };
-    int nFans0, nFans1, iVar0, iVar1, nPairs;
+    int i, iVar0, iVar1, nFans0, nFans1, nPairs;
     int fEquals[2][2], fOppos, fPairs[4][4];
     unsigned j, k, nFansNew, uSupp0, uSupp1;
-    int i;
 
     assert( pObj->nFans > 0 );
     assert( pObj->Type == KIT_DSD_PRIME );
-    assert( pObj->uSupp == (uSupp0 = (unsigned)Kit_TruthSupport(pTruth, pObj->nFans)) );
+    assert( uSupp == (uSupp0 = (unsigned)Kit_TruthSupport(pTruth, pObj->nFans)) );
 
     // compress the truth table
-    if ( pObj->uSupp != Kit_BitMask(pObj->nFans) )
+    if ( uSupp != Kit_BitMask(pObj->nFans) )
     {
-        nFansNew = Kit_WordCountOnes(pObj->uSupp);
-        Kit_TruthShrink( pNtk->pMem, pTruth, nFansNew, pObj->nFans, pObj->uSupp );
-        Kit_TruthCopy( pTruth, pNtk->pMem, pObj->nFans );
+        nFansNew = Kit_WordCountOnes(uSupp);
+        Kit_TruthShrink( pNtk->pMem, pTruth, nFansNew, pObj->nFans, uSupp, 1 );
         for ( j = k = 0; j < pObj->nFans; j++ )
-            if ( pObj->uSupp & (1 << j) )
+            if ( uSupp & (1 << j) )
                 pObj->pFans[k++] = pObj->pFans[j];
         assert( k == nFansNew );
         pObj->nFans = k;
-        pObj->uSupp = Kit_BitMask(pObj->nFans);
+        uSupp = Kit_BitMask(pObj->nFans);
     }
 
     // consider the single variable case
@@ -363,7 +361,7 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
             // check the MUX decomposition
             uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
             uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
-            assert( pObj->uSupp == (uSupp0 | uSupp1 | (1<<i)) );
+            assert( uSupp == (uSupp0 | uSupp1 | (1<<i)) );
             if ( uSupp0 & uSupp1 )
                 continue;
             // perform MUX decomposition
@@ -376,25 +374,24 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
             }
             Kit_TruthCopy( Dsd_ObjTruth(pRes0), pCofs2[0], pObj->nFans );        
             Kit_TruthCopy( Dsd_ObjTruth(pRes1), pCofs2[1], pObj->nFans ); 
-            pRes0->uSupp = uSupp0;
-            pRes1->uSupp = uSupp1;
             // update the current one
             pObj->Type = KIT_DSD_MUX;
             pObj->nFans = 3;
             pObj->pFans[0] = pObj->pFans[i];
-            pObj->pFans[1] = 2*pRes1->Id;
-            pObj->pFans[2] = 2*pRes0->Id;
+            pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
+            pObj->pFans[2] = 2*pRes0->Id; pRes0->nRefs++;
             // call recursively
-            Kit_DsdDecompose_rec( pNtk, pRes0, pObj->pFans + 2 );
-            Kit_DsdDecompose_rec( pNtk, pRes1, pObj->pFans + 1 );
+            Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 2 );
+            Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1 );
             return;
         }
 //Extra_PrintBinary( stdout, pTruth, 1 << pObj->nFans ); printf( "\n" );
 
         // create the new node
         pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 );
+        pRes->nRefs++;
         pRes->nFans = 2;
-        pRes->pFans[0] = pObj->pFans[i];  pObj->pFans[i] = 127;  pObj->uSupp &= ~(1 << i);
+        pRes->pFans[0] = pObj->pFans[i];  pObj->pFans[i] = 127;  uSupp &= ~(1 << i);
         pRes->pFans[1] = 2*pObj->Id;
         // update the parent pointer
         *pPar = 2 * pRes->Id;
@@ -430,7 +427,7 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
             assert( 0 );
         // decompose the remainder
         assert( Dsd_ObjTruth(pObj) == pTruth );
-        Kit_DsdDecompose_rec( pNtk, pObj, pRes->pFans + 1 );
+        Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1 );
         return;
     }
     pObj->fMark = 1;
@@ -445,11 +442,12 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
         // check the existence of MUX decomposition
         uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
         uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
-        // if one of the cofs is a constant, it is time to check it again
+        assert( uSupp == (uSupp0 | uSupp1 | (1<<i)) );
+        // if one of the cofs is a constant, it is time to check the output again
         if ( uSupp0 == 0 || uSupp1 == 0 )
         {
             pObj->fMark = 0;
-            Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+            Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
             return;
         }
         assert( uSupp0 && uSupp1 );
@@ -475,17 +473,18 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
             {
                 // construct the MUX
                 pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_MUX, 3 );
+                pRes->nRefs++;
                 pRes->nFans = 3;
                 pRes->pFans[0] = pObj->pFans[i];     pObj->pFans[i] = 2 * pRes->Id; // remains in support
-                pRes->pFans[1] = pObj->pFans[iVar1]; pObj->pFans[iVar1] = 127;  pObj->uSupp &= ~(1 << iVar1);
-                pRes->pFans[2] = pObj->pFans[iVar0]; pObj->pFans[iVar0] = 127;  pObj->uSupp &= ~(1 << iVar0);
+                pRes->pFans[1] = pObj->pFans[iVar1]; pObj->pFans[iVar1] = 127;  uSupp &= ~(1 << iVar1);
+                pRes->pFans[2] = pObj->pFans[iVar0]; pObj->pFans[iVar0] = 127;  uSupp &= ~(1 << iVar0);
                 // update the node
                 if ( fEquals[0][0] && fEquals[0][1] )
                     Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
                 else
                     Kit_TruthMux( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
                 // decompose the remainder
-                Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+                Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
                 return;
             }
         }
@@ -499,21 +498,22 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
             Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, k ); // 10 
             Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, k ); // 11 
             // compare equal pairs
-            fPairs[0][1] = fPairs[1][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[0][1], pObj->nFans);
-            fPairs[0][2] = fPairs[2][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[1][0], pObj->nFans);
-            fPairs[0][3] = fPairs[3][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[1][1], pObj->nFans);
-            fPairs[1][2] = fPairs[2][1] = Kit_TruthIsEqual(pCofs4[0][1], pCofs4[1][0], pObj->nFans);
-            fPairs[1][3] = fPairs[3][1] = Kit_TruthIsEqual(pCofs4[0][1], pCofs4[1][1], pObj->nFans);
-            fPairs[2][3] = fPairs[3][2] = Kit_TruthIsEqual(pCofs4[1][0], pCofs4[1][1], pObj->nFans);
+            fPairs[0][1] = fPairs[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[0][1], pObj->nFans );
+            fPairs[0][2] = fPairs[2][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans );
+            fPairs[0][3] = fPairs[3][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans );
+            fPairs[1][2] = fPairs[2][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans );
+            fPairs[1][3] = fPairs[3][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans );
+            fPairs[2][3] = fPairs[3][2] = Kit_TruthIsEqual( pCofs4[1][0], pCofs4[1][1], pObj->nFans );
             nPairs = fPairs[0][1] + fPairs[0][2] + fPairs[0][3] + fPairs[1][2] + fPairs[1][3] + fPairs[2][3];
             if ( nPairs != 3 && nPairs != 2 )
                 continue;
 
             // decomposition exists
             pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 );
+            pRes->nRefs++;
             pRes->nFans = 2;
-            pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id;  // remains the support
-            pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127;       pObj->uSupp &= ~(1 << i);
+            pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id;  // remains in support
+            pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127;       uSupp &= ~(1 << i);
             if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00
             {
                 pRes->pFans[0] ^= 1;  
@@ -548,7 +548,7 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * p
                 Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
             }
             // decompose the remainder
-            Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+            Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
             return;
         }
     }
@@ -569,6 +569,7 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
 {
     Dsd_Ntk_t * pNtk;
     Dsd_Obj_t * pObj;
+    unsigned uSupp;
     int i, nVarsReal;
     assert( nVars <= 16 );
     pNtk = Kit_DsdNtkAlloc( pTruth, nVars );
@@ -579,9 +580,9 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
     for ( i = 0; i < nVars; i++ )
        pObj->pFans[i] = 2*i;
     Kit_TruthCopy( Dsd_ObjTruth(pObj), pTruth, nVars );
-    pObj->uSupp = Kit_TruthSupport( pTruth, nVars );
+    uSupp = Kit_TruthSupport( pTruth, nVars );
     // consider special cases
-    nVarsReal = Kit_WordCountOnes( pObj->uSupp );
+    nVarsReal = Kit_WordCountOnes( uSupp );
     if ( nVarsReal == 0 )
     {
         pObj->Type = KIT_DSD_CONST1;
@@ -593,11 +594,11 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
     {
         pObj->Type = KIT_DSD_VAR;
         pObj->nFans = 1;
-        pObj->pFans[0] = 2 * Kit_WordFindFirstBit( pObj->uSupp );
+        pObj->pFans[0] = 2 * Kit_WordFindFirstBit( uSupp );
         pObj->pFans[0] ^= (pTruth[0] & 1);
         return pNtk;
     }
-    Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], &pNtk->Root );
+    Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root );
     return pNtk;
 }
 
@@ -615,16 +616,15 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
 void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
 {
     Dsd_Ntk_t * pNtk0, * pNtk1;
-    Dsd_Obj_t * pRoot;
+//    Dsd_Obj_t * pRoot;
     unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
     unsigned i, * pTruth;
     int fVerbose = 1;
 
-//    pTruth = pTruthInit;
-
-    pRoot = Dsd_NtkRoot(pNtk);
-    pTruth = Dsd_ObjTruth(pRoot);
-    assert( pRoot->nFans == pNtk->nVars );
+    pTruth = pTruthInit;
+//    pRoot = Dsd_NtkRoot(pNtk);
+//    pTruth = Dsd_ObjTruth(pRoot);
+//    assert( pRoot->nFans == pNtk->nVars );
 
     if ( fVerbose )
     {
@@ -632,6 +632,7 @@ void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
 //        Extra_PrintBinary( stdout, pTruth, (1 << pNtk->nVars) ); 
         Extra_PrintHexadecimal( stdout, pTruth, pNtk->nVars ); 
         printf( "\n" );
+        Kit_DsdPrint( stdout, pNtk );
     }
     for ( i = 0; i < pNtk->nVars; i++ )
     {
@@ -676,8 +677,9 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
 //    if ( Kit_DsdFindLargeBox(pNtk, Dsd_NtkRoot(pNtk)) )
 //        Kit_DsdPrint( stdout, pNtk );
 
-    if ( Dsd_NtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 8 )
-        Kit_DsdTestCofs( pNtk, pTruth );
+//    if ( Dsd_NtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 )
+
+    Kit_DsdTestCofs( pNtk, pTruth );
 
     Kit_DsdNtkFree( pNtk );
 }
diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c
index 5ac85524..62d4cf14 100644
--- a/src/opt/kit/kitTruth.c
+++ b/src/opt/kit/kitTruth.c
@@ -168,7 +168,7 @@ void Kit_TruthSwapAdjacentVars2( unsigned * pIn, unsigned * pOut, int nVars, int
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase )
+void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
 {
     unsigned * pTemp;
     int i, k, Var = nVars - 1, Counter = 0;
@@ -185,7 +185,7 @@ void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
         }
     assert( Var == -1 );
     // swap if it was moved an even number of times
-    if ( !(Counter & 1) )
+    if ( fReturnIn ^ !(Counter & 1) )
         Kit_TruthCopy( pOut, pIn, nVarsAll );
 }
 
@@ -202,7 +202,7 @@ void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase )
+void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
 {
     unsigned * pTemp;
     int i, k, Var = 0, Counter = 0;
@@ -219,7 +219,7 @@ void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
         }
     assert( Var == nVars );
     // swap if it was moved an even number of times
-    if ( !(Counter & 1) )
+    if ( fReturnIn ^ !(Counter & 1) )
         Kit_TruthCopy( pOut, pIn, nVarsAll );
 }
 
@@ -1080,6 +1080,28 @@ void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of 1's in each cofactor.]
+
+  Description [Verifies the above procedure.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux )
+{
+    int i;
+    for ( i = 0; i < nVars; i++ )
+    {
+        Kit_TruthCofactor0New( pAux, pTruth, nVars, i );
+        pStore[2*i+0] = Kit_TruthCountOnes( pAux, nVars ) / 2;
+        Kit_TruthCofactor1New( pAux, pTruth, nVars, i );
+        pStore[2*i+1] = Kit_TruthCountOnes( pAux, nVars ) / 2;
+    }
+}
 
 /**Function*************************************************************
 
@@ -1191,6 +1213,7 @@ unsigned Kit_TruthHash( unsigned * pIn, int nWords )
 ***********************************************************************/
 unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore )
 {
+//    short pStore2[32];
     unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
     int nWords = Kit_TruthWordNum( nVars );
     int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
@@ -1198,20 +1221,26 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
 
     // canonicize output
     uCanonPhase = 0;
+/*
     nOnes = Kit_TruthCountOnes(pIn, nVars);
-    if ( (nOnes > nWords * 16) || ((nOnes == nWords * 16) && (pIn[0] & 1)) )
+    if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
     {
         uCanonPhase |= (1 << nVars);
         Kit_TruthNot( pIn, pIn, nVars );
     }
-
+*/
     // collect the minterm counts
     Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
+//    Kit_TruthCountOnesInCofsSlow( pIn, nVars, pStore2, pAux );
+//    for ( i = 0; i < 2*nVars; i++ )
+//    {
+//        assert( pStore[i] == pStore2[i] );
+//    }
 
     // canonicize phase
     for ( i = 0; i < nVars; i++ )
     {
-        if ( pStore[2*i+0] <= pStore[2*i+1] )
+        if ( pStore[2*i+0] >= pStore[2*i+1] )
             continue;
         uCanonPhase |= (1 << i);
         Temp = pStore[2*i+0];
@@ -1229,7 +1258,7 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
         fChange = 0;
         for ( i = 0; i < nVars-1; i++ )
         {
-            if ( pStore[2*i] <= pStore[2*(i+1)] )
+            if ( pStore[2*i] >= pStore[2*(i+1)] )
                 continue;
             Counter++;
             fChange = 1;
@@ -1246,17 +1275,24 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
             pStore[2*i+1] = pStore[2*(i+1)+1];
             pStore[2*(i+1)+1] = Temp;
 
+            // if the polarity of variables is different, swap them
+            if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
+            {
+                uCanonPhase ^= (1 << i);
+                uCanonPhase ^= (1 << (i+1));
+            }
+
             Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
             pTemp = pIn; pIn = pOut; pOut = pTemp;
         }
     } while ( fChange );
 
 /*
-    Kit_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
+    Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
     for ( i = 0; i < nVars; i++ )
         printf( "%d=%d/%d  ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
     printf( "  C = %d\n", Counter );
-    Kit_PrintHexadecimal( stdout, pIn, nVars );
+    Extra_PrintHexadecimal( stdout, pIn, nVars );
     printf( "\n" );
 */
 
@@ -1337,6 +1373,144 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
     return uCanonPhase;
 }
 
+ 
+/**Function*************************************************************
+
+  Synopsis    [Fast counting minterms in the cofactors of a function.]
+
+  Description [Returns the total number of minterms in the function.
+  The resulting array (pRes) contains the number of minterms in 0-cofactor
+  w.r.t. each variables. The additional array (pBytes) is used for internal 
+  storage. It should have the size equal to the number of truth table bytes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pBytes )
+{
+    // the number of 1s if every byte as well as in the 0-cofactors w.r.t. three variables
+    static unsigned Table[256] = {
+        0x00000000, 0x01010101, 0x01010001, 0x02020102, 0x01000101, 0x02010202, 0x02010102, 0x03020203,
+        0x01000001, 0x02010102, 0x02010002, 0x03020103, 0x02000102, 0x03010203, 0x03010103, 0x04020204,
+        0x00010101, 0x01020202, 0x01020102, 0x02030203, 0x01010202, 0x02020303, 0x02020203, 0x03030304,
+        0x01010102, 0x02020203, 0x02020103, 0x03030204, 0x02010203, 0x03020304, 0x03020204, 0x04030305,
+        0x00010001, 0x01020102, 0x01020002, 0x02030103, 0x01010102, 0x02020203, 0x02020103, 0x03030204,
+        0x01010002, 0x02020103, 0x02020003, 0x03030104, 0x02010103, 0x03020204, 0x03020104, 0x04030205,
+        0x00020102, 0x01030203, 0x01030103, 0x02040204, 0x01020203, 0x02030304, 0x02030204, 0x03040305,
+        0x01020103, 0x02030204, 0x02030104, 0x03040205, 0x02020204, 0x03030305, 0x03030205, 0x04040306,
+        0x00000101, 0x01010202, 0x01010102, 0x02020203, 0x01000202, 0x02010303, 0x02010203, 0x03020304,
+        0x01000102, 0x02010203, 0x02010103, 0x03020204, 0x02000203, 0x03010304, 0x03010204, 0x04020305,
+        0x00010202, 0x01020303, 0x01020203, 0x02030304, 0x01010303, 0x02020404, 0x02020304, 0x03030405,
+        0x01010203, 0x02020304, 0x02020204, 0x03030305, 0x02010304, 0x03020405, 0x03020305, 0x04030406,
+        0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
+        0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
+        0x00020203, 0x01030304, 0x01030204, 0x02040305, 0x01020304, 0x02030405, 0x02030305, 0x03040406,
+        0x01020204, 0x02030305, 0x02030205, 0x03040306, 0x02020305, 0x03030406, 0x03030306, 0x04040407,
+        0x00000001, 0x01010102, 0x01010002, 0x02020103, 0x01000102, 0x02010203, 0x02010103, 0x03020204,
+        0x01000002, 0x02010103, 0x02010003, 0x03020104, 0x02000103, 0x03010204, 0x03010104, 0x04020205,
+        0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
+        0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
+        0x00010002, 0x01020103, 0x01020003, 0x02030104, 0x01010103, 0x02020204, 0x02020104, 0x03030205,
+        0x01010003, 0x02020104, 0x02020004, 0x03030105, 0x02010104, 0x03020205, 0x03020105, 0x04030206,
+        0x00020103, 0x01030204, 0x01030104, 0x02040205, 0x01020204, 0x02030305, 0x02030205, 0x03040306,
+        0x01020104, 0x02030205, 0x02030105, 0x03040206, 0x02020205, 0x03030306, 0x03030206, 0x04040307,
+        0x00000102, 0x01010203, 0x01010103, 0x02020204, 0x01000203, 0x02010304, 0x02010204, 0x03020305,
+        0x01000103, 0x02010204, 0x02010104, 0x03020205, 0x02000204, 0x03010305, 0x03010205, 0x04020306,
+        0x00010203, 0x01020304, 0x01020204, 0x02030305, 0x01010304, 0x02020405, 0x02020305, 0x03030406,
+        0x01010204, 0x02020305, 0x02020205, 0x03030306, 0x02010305, 0x03020406, 0x03020306, 0x04030407,
+        0x00010103, 0x01020204, 0x01020104, 0x02030205, 0x01010204, 0x02020305, 0x02020205, 0x03030306,
+        0x01010104, 0x02020205, 0x02020105, 0x03030206, 0x02010205, 0x03020306, 0x03020206, 0x04030307,
+        0x00020204, 0x01030305, 0x01030205, 0x02040306, 0x01020305, 0x02030406, 0x02030306, 0x03040407,
+        0x01020205, 0x02030306, 0x02030206, 0x03040307, 0x02020306, 0x03030407, 0x03030307, 0x04040408
+    };
+    unsigned uSum;
+    unsigned char * pTruthC, * pLimit;
+    int i, iVar, Step, nWords, nBytes, nTotal;
+
+    assert( nVars <= 20 );
+
+    // clear storage
+    memset( pRes, 0, sizeof(int) * nVars );
+
+    // count the number of one's in 0-cofactors of the first three variables
+    nTotal = uSum = 0;
+    nWords = Kit_TruthWordNum( nVars );
+    nBytes = nWords * 4;
+    pTruthC = (unsigned char *)pTruth;
+    pLimit = pTruthC + nBytes;
+    for ( ; pTruthC < pLimit; pTruthC++ )
+    {
+        uSum += Table[*pTruthC];
+        *pBytes++ = (Table[*pTruthC] & 0xff);
+        if ( (uSum & 0xff) > 246 )
+        {
+            nTotal += (uSum & 0xff);
+            pRes[0] += ((uSum >>  8) & 0xff);
+            pRes[2] += ((uSum >> 16) & 0xff);
+            pRes[3] += ((uSum >> 24) & 0xff);
+            uSum = 0;
+        }
+    }
+    if ( uSum )
+    {
+        nTotal += (uSum & 0xff);
+        pRes[0] += ((uSum >>  8) & 0xff);
+        pRes[1] += ((uSum >> 16) & 0xff);
+        pRes[2] += ((uSum >> 24) & 0xff);
+    }
+
+    // count all other variables
+    for ( iVar = 3, Step = 1; Step < nBytes; Step *= 2, iVar++ )
+        for ( i = 0; i < nBytes; i += Step + Step )
+        {
+            pRes[iVar] += pBytes[i];
+            pBytes[i] += pBytes[i+Step];
+        }
+    assert( pBytes[0] == nTotal );
+    assert( iVar == nVars );
+    return nTotal;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fast counting minterms for the functions.]
+
+  Description [Returns 0 if the function is a constant.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_TruthCountMintermsPrecomp()
+{
+    int bit_count[256] = {
+      0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+      1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+      1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+      2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+      1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+      2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+      2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+      3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+    };
+    unsigned i, uWord;
+    for ( i = 0; i < 256; i++ )
+    {
+        if ( i % 8 == 0 )
+            printf( "\n" );
+        uWord  =  bit_count[i];
+        uWord |= (bit_count[i & 0x55] <<  8);
+        uWord |= (bit_count[i & 0x33] << 16);
+        uWord |= (bit_count[i & 0x0f] << 24);
+        printf( "0x" );
+        Extra_PrintHexadecimal( stdout, &uWord, 5 );
+        printf( ", " );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 9d27e892..5872f5bc 100644
--- a/src/sat/csat/csat_apis.c
+++ b/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 )