Version abc51001

author: Alan Mishchenko <alanmi@berkeley.edu> 2005-10-01 08:01:00 -0700
committer: Alan Mishchenko <alanmi@berkeley.edu> 2005-10-01 08:01:00 -0700
commit: 78fbd336aa584c4d285123ad18617aa9277016b4 (patch)
tree: 5d65fe6b080dc85b1456320f60555ba33bab9b09 /src
parent: 0af9acd0cd07dcb37c195c6a0832b82c0eca1193 (diff)
download: abc-78fbd336aa584c4d285123ad18617aa9277016b4.tar.gz
abc-78fbd336aa584c4d285123ad18617aa9277016b4.tar.bz2
abc-78fbd336aa584c4d285123ad18617aa9277016b4.zip
35 files changed, 2283 insertions, 217 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 50787d9b..64df9fc5 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -439,7 +439,8 @@ extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t *
 extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
 /*=== abcCut.c ==========================================================*/
 extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj );
-extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj );
+extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti );
+extern void               Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst );
 extern void *             Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
 extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
 /*=== abcDfs.c ==========================================================*/
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 639f4926..3f7f8d7c 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -1231,7 +1231,6 @@ void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan )
             {
                 int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id;
                 int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id;
-                int x = 0;
                 printf( "Node %d has incorrect ordering of fanins.\n", pEnt->Id );
             }
         }
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index e36f5219..cc8b90f6 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -111,7 +111,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
     Abc_NtkForEachObj( pNtk, pNode, i )
         Vec_PtrPush( vNodes, pNode );
     // write the DOT file
-    Io_WriteDot( pNtk, vNodes, NULL, FileNameDot );
+    Io_WriteDot( pNtk, vNodes, NULL, FileNameDot, 0 );
     Vec_PtrFree( vNodes );
 
     // visualize the file 
@@ -120,6 +120,66 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Visualizes AIG with choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkShowMulti( Abc_Ntk_t * pNtk )
+{
+    FILE * pFile;
+    Abc_Obj_t * pNode;
+    Vec_Ptr_t * vNodes;
+    char FileNameDot[200];
+    int i;
+    extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkBalanceLevel( Abc_Ntk_t * pNtk );
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    // create the file name
+    Abc_ShowGetFileName( pNtk->pName, FileNameDot );
+    // check that the file can be opened
+    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+
+    // get the implication supergates
+    Abc_NtkBalanceAttach( pNtk );
+    // set the levels based on the implication supergates
+    Abc_NtkBalanceLevel( pNtk );
+
+    // collect all nodes that are roots
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        Vec_PtrPush( vNodes, pNode );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy || Abc_ObjFaninNum(pNode) == 0 )
+            Vec_PtrPush( vNodes, pNode );
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        Vec_PtrPush( vNodes, pNode );
+
+    // write the DOT file
+    Io_WriteDot( pNtk, vNodes, NULL, FileNameDot, 1 );
+    Vec_PtrFree( vNodes );
+
+    // undo the supergates
+    Abc_NtkBalanceDetach( pNtk );
+    // set the normal levels
+    Abc_NtkGetLevelNum( pNtk );
+
+    // visualize the file 
+    Abc_ShowFile( FileNameDot );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Visualizes a reconvergence driven cut at the node.]
 
   Description []
@@ -170,7 +230,7 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
     // add the root node to the cone (for visualization)
     Vec_PtrPush( vCutSmall, pNode );
     // write the DOT file
-    Io_WriteDot( pNode->pNtk, vInside, vCutSmall, FileNameDot );
+    Io_WriteDot( pNode->pNtk, vInside, vCutSmall, FileNameDot, 0 );
     // stop the cut computation manager
     Abc_NtkManCutStop( p );
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 38472a0c..4e2e14a2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -932,20 +932,24 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
+    int fMulti;
     extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkShowMulti( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fMulti = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "mh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'h':
-            goto usage;
+        case 'm':
+            fMulti ^= 1;
+            break;
         default:
             goto usage;
         }
@@ -962,7 +966,16 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\" or \"seq\").\n" );
         return 1;
     }
-    Abc_NtkShowAig( pNtk );
+    if ( fMulti && !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Visualizing multi-input ANDs cannot be done for sequential network (run \"unseq\").\n" );
+        return 1;
+    }
+
+    if ( !fMulti )
+        Abc_NtkShowAig( pNtk );
+    else
+        Abc_NtkShowMulti( pNtk );
     return 0;
 
 usage:
@@ -972,6 +985,7 @@ usage:
     fprintf( pErr, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
     fprintf( pErr, "       (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
 #endif
+    fprintf( pErr, "\t-m    : toggles visualization of multi-input ANDs [default = %s].\n", fMulti? "yes": "no" );  
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -1300,8 +1314,8 @@ usage:
     fprintf( pErr, "\t-F num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
     fprintf( pErr, "\t-T num  : the threshold for AIG node duplication [default = %d]\n", nThresh );
     fprintf( pErr, "\t          (an AIG node is the root of a new node after renoding\n" );
-    fprintf( pErr, "\t          if doing so prevents duplication of more than %d AIG nodes,\n", nThresh );
-    fprintf( pErr, "\t          that is, if [(numFanouts(Node)-1) * size(MFFC(Node))] > %d)\n", nThresh );
+    fprintf( pErr, "\t          if this leads to duplication of no more than %d AIG nodes,\n", nThresh );
+    fprintf( pErr, "\t          that is, if [(numFanouts(Node)-1) * size(MFFC(Node))] <= %d)\n", nThresh );
     fprintf( pErr, "\t-m      : creates multi-input AND graph [default = %s]\n", fMulti? "yes": "no" );
     fprintf( pErr, "\t-s      : creates a simple AIG (no renoding) [default = %s]\n", fSimple? "yes": "no" );
     fprintf( pErr, "\t-c      : performs renoding to derive the CNF [default = %s]\n", fCnf? "yes": "no" );
@@ -2733,13 +2747,14 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     memset( pParams, 0, sizeof(Cut_Params_t) );
     pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
-    pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
+    pParams->nKeepMax  = 1000;  // the max number of cuts kept at a node
     pParams->fTruth    = 0;     // compute truth tables
     pParams->fFilter   = 1;     // filter dominated cuts
     pParams->fDrop     = 0;     // drop cuts on the fly
+    pParams->fMulti    = 0;     // use multi-input AND-gates
     pParams->fVerbose  = 0;     // the verbosiness flag
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "KMtfdvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "KMtfdmvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2774,6 +2789,9 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pParams->fDrop ^= 1;
             break;
+        case 'm':
+            pParams->fMulti ^= 1;
+            break;
         case 'v':
             pParams->fVerbose ^= 1;
             break;
@@ -2800,13 +2818,14 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdvh]\n" );
+    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdmvh]\n" );
     fprintf( pErr, "\t         computes k-feasible cuts for the AIG\n" );
     fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",     pParams->nVarsMax );
     fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
     fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth? "yes": "no" );
     fprintf( pErr, "\t-f     : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter? "yes": "no" );
     fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",    pParams->fDrop? "yes": "no" );
+    fprintf( pErr, "\t-m     : toggle using multi-input AND-gates [default = %s]\n",       pParams->fMulti? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -2839,9 +2858,9 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     memset( pParams, 0, sizeof(Cut_Params_t) );
     pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
-    pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
+    pParams->nKeepMax  = 1000;  // the max number of cuts kept at a node
     pParams->fTruth    = 0;     // compute truth tables
-    pParams->fFilter   = 0;     // filter dominated cuts
+    pParams->fFilter   = 1;     // filter dominated cuts
     pParams->fSeq      = 1;     // compute sequential cuts
     pParams->fVerbose  = 0;     // the verbosiness flag
     util_getopt_reset();
@@ -4347,8 +4366,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fForward;
     int fBackward;
     int fInitial;
-
-    extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
+    int fVerbose;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -4358,8 +4376,9 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     fForward  = 0;
     fBackward = 0;
     fInitial  = 0;
+    fVerbose  = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "fbih" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "fbivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4372,6 +4391,9 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'i':
             fInitial ^= 1;
             break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -4393,13 +4415,13 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     if ( fForward )
-        Abc_NtkSeqRetimeForward( pNtk );
+        Abc_NtkSeqRetimeForward( pNtk, fVerbose );
     else if ( fBackward )
-        Abc_NtkSeqRetimeBackward( pNtk );
+        Abc_NtkSeqRetimeBackward( pNtk, fVerbose );
     else if ( fInitial )
-        Abc_NtkSeqRetimeInitial( pNtk );
+        Abc_NtkSeqRetimeInitial( pNtk, fVerbose );
     else
-        Abc_NtkSeqRetimeDelay( pNtk );
+        Abc_NtkSeqRetimeDelay( pNtk, fVerbose );
     return 0;
 
 usage:
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 035a2d1a..c612a1ce 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -242,6 +242,167 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst,
 }
 
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes in the implication supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeFindCone_rec( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNodeC, * pNodeT, * pNodeE;
+    int RetValue, i;
+    assert( !Abc_ObjIsComplement(pNode) );
+    if ( Abc_ObjIsCi(pNode) )
+        return NULL;
+    // start the new array
+    vNodes = Vec_PtrAlloc( 4 );
+    // if the node is the MUX collect its fanins
+    if ( Abc_NodeIsMuxType(pNode) )
+    {
+        pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
+        Vec_PtrPush( vNodes, Abc_ObjRegular(pNodeC) );
+        Vec_PtrPushUnique( vNodes, Abc_ObjRegular(pNodeT) );
+        Vec_PtrPushUnique( vNodes, Abc_ObjRegular(pNodeE) );
+    }
+    else
+    {
+        // collect the nodes in the implication supergate
+        RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, 1 );
+        assert( vNodes->nSize > 1 );
+        // unmark the visited nodes
+        Vec_PtrForEachEntry( vNodes, pNode, i )
+            Abc_ObjRegular(pNode)->fMarkB = 0;
+        // if we found the node and its complement in the same implication supergate, 
+        // return empty set of nodes (meaning that we should use constant-0 node)
+        if ( RetValue == -1 )
+            vNodes->nSize = 0;
+    }
+    // call for the fanin
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        pNode = Abc_ObjRegular(pNode);
+        if ( pNode->pCopy )
+            continue;
+        pNode->pCopy = (Abc_Obj_t *)Abc_NodeFindCone_rec( pNode );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Attaches the implication supergates to internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Abc_NtkCleanCopy( pNtk );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pNode = Abc_ObjFanin0(pNode);
+        if ( pNode->pCopy )
+            continue;
+        pNode->pCopy = (Abc_Obj_t *)Abc_NodeFindCone_rec( pNode );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Attaches the implication supergates to internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy )
+        {
+            Vec_PtrFree( (Vec_Ptr_t *)pNode->pCopy );
+            pNode->pCopy = NULL;
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute levels of implication supergates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkBalanceLevel_rec( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vSuper;
+    Abc_Obj_t * pFanin;
+    int i, LevelMax;
+    assert( !Abc_ObjIsComplement(pNode) );
+    if ( pNode->Level > 0 )
+        return pNode->Level;
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
+    vSuper = (Vec_Ptr_t *)pNode->pCopy;
+    assert( vSuper != NULL );
+    LevelMax = 0;
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    {
+        pFanin = Abc_ObjRegular(pFanin);
+        Abc_NtkBalanceLevel_rec(pFanin);
+        if ( LevelMax < (int)pFanin->Level )
+            LevelMax = pFanin->Level;
+    }
+    pNode->Level = LevelMax + 1;
+    return pNode->Level;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compute levels of implication supergates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBalanceLevel( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        pNode->Level = 0;
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_NtkBalanceLevel_rec( Abc_ObjFanin0(pNode) );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 64dec4a4..7cc3d65b 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -25,6 +25,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq );
+static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -49,7 +52,12 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     int i;
     int clk = clock();
 
+    extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
+
     assert( Abc_NtkIsStrash(pNtk) );
+    if ( pParams->fMulti )
+        Abc_NtkBalanceAttach(pNtk);
 
     // start the manager
     pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
@@ -76,7 +84,13 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
         if ( Abc_NodeIsConst(pObj) )
             continue;
         // compute the cuts to the internal node
-        Abc_NodeGetCuts( p, pObj );  
+        Abc_NodeGetCuts( p, pObj, pParams->fMulti );  
+        // consider dropping the fanins cuts
+        if ( pParams->fDrop )
+        {
+            Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId1(pObj) );
+        }
         // add cuts due to choices
         if ( Abc_NodeIsAigChoice(pObj) )
         {
@@ -88,7 +102,11 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     }
     Vec_PtrFree( vNodes );
     Vec_IntFree( vChoices );
+    if ( pParams->fMulti )
+        Abc_NtkBalanceDetach(pNtk);
 PRT( "Total", clock() - clk );
+Abc_NtkPrintCuts_( p, pNtk, 0 );
+//    Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
     return p;
 }
 
@@ -105,7 +123,68 @@ PRT( "Total", clock() - clk );
 ***********************************************************************/
 Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
 {
-    return NULL;
+    Cut_Man_t *  p;
+    Abc_Obj_t * pObj;
+    int i, nIters, fStatus;
+    int clk = clock();
+
+    assert( Abc_NtkIsSeq(pNtk) );
+    assert( pParams->fSeq );
+
+    // start the manager
+    pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
+    pParams->nCutSet = pNtk->vLats->nSize;
+    p = Cut_ManStart( pParams );
+
+    // set cuts for PIs
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Cut_NodeSetTriv( p, pObj->Id );
+    // label the cutset nodes and set their number in the array
+    // assign the elementary cuts to the cutset nodes
+    Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+    {
+        assert( pObj->fMarkC == 0 );
+        pObj->fMarkC = 1;
+        pObj->pCopy = (Abc_Obj_t *)i;
+        Cut_NodeSetTriv( p, pObj->Id );
+    }
+
+    // process the nodes
+    for ( nIters = 0; nIters < 10; nIters++ )
+    {
+//printf( "ITERATION %d:\n", nIters );
+        // compute the cuts for the internal nodes
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            Abc_NodeGetCutsSeq( p, pObj, nIters==0 );
+Abc_NtkPrintCuts( p, pNtk, 1 );
+        // merge the new cuts with the old cuts
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Cut_NodeNewMergeWithOld( p, pObj->Id );
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            Cut_NodeNewMergeWithOld( p, pObj->Id );
+        // for the cutset, merge temp with new
+        fStatus = 0;
+        Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+            fStatus |= Cut_NodeTempTransferToNew( p, pObj->Id, i );
+        if ( fStatus == 0 )
+            break;
+    }
+
+    // if the status is not finished, transfer new to old for the cutset
+    Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+        Cut_NodeNewMergeWithOld( p, pObj->Id );
+
+    // transfer the old cuts to the new positions
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        Cut_NodeOldTransferToNew( p, pObj->Id );
+
+    // unlabel the cutset nodes
+    Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+        pObj->fMarkC = 0;
+PRT( "Total", clock() - clk );
+printf( "Converged after %d iterations.\n", nIters );
+Abc_NtkPrintCuts( p, pNtk, 1 );
+    return p;
 }
 
 /**Function*************************************************************
@@ -126,7 +205,7 @@ void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj )
         return pList;
     Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj) );
     Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj) );
-    return Abc_NodeGetCuts( p, pObj );
+    return Abc_NodeGetCuts( p, pObj, 0 );
 }
 
 /**Function*************************************************************
@@ -140,10 +219,35 @@ void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj )
+void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti )
 {
+    int fTriv = (!fMulti) || (pObj->pCopy != NULL);
+    assert( Abc_NtkIsStrash(pObj->pNtk) );
+    assert( Abc_ObjFaninNum(pObj) == 2 );
     return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
-        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), 1, 1, fTriv );  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv )
+{
+    int CutSetNum;
+    assert( Abc_NtkIsSeq(pObj->pNtk) );
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+//    fTriv     = pObj->fMarkC ? 0 : fTriv;
+    CutSetNum = pObj->fMarkC ? (int)pObj->pCopy : -1;
+    Cut_NodeComputeCutsSeq( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj), fTriv, CutSetNum );  
 }
 
 /**Function*************************************************************
@@ -159,7 +263,7 @@ void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj )
 ***********************************************************************/
 void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj )
 {
-    return Cut_NodeReadCuts( p, pObj->Id );  
+    return Cut_NodeReadCutsNew( p, pObj->Id );  
 }
 
 /**Function*************************************************************
@@ -178,6 +282,54 @@ void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj )
     Cut_NodeFreeCuts( p, pObj->Id );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq )
+{
+    Cut_Man_t * pMan = p;
+    Cut_Cut_t * pList;
+    Abc_Obj_t * pObj;
+    int i;
+    printf( "Cuts of the network:\n" );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        pList = Abc_NodeReadCuts( p, pObj );
+        printf( "Node %s:\n", Abc_ObjName(pObj) );
+        Cut_CutPrintList( pList, fSeq );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq )
+{
+    Cut_Man_t * pMan = p;
+    Cut_Cut_t * pList;
+    Abc_Obj_t * pObj;
+    pObj = Abc_NtkObj( pNtk, 2 * Abc_NtkObjNum(pNtk) / 3 );
+    pList = Abc_NodeReadCuts( p, pObj );
+    printf( "Node %s:\n", Abc_ObjName(pObj) );
+    Cut_CutPrintList( pList, fSeq );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index b70d30e6..a14718c4 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -192,7 +192,7 @@ void Abc_NodePrintCuts( Abc_Obj_t * pNode )
     {
         Extra_PrintBinary( stdout, (unsigned *)&pCut->uSign, 16 ); 
         printf( "   " );
-        Cut_CutPrint( pCut );   
+        Cut_CutPrint( pCut, 0 );   
         printf( "\n" );
     }
 }
diff --git a/src/base/abcs/abcRetCore.c b/src/base/abcs/abcRetCore.c
index f6ba0c59..22735597 100644
--- a/src/base/abcs/abcRetCore.c
+++ b/src/base/abcs/abcRetCore.c
@@ -46,7 +46,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk )
+void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Vec_Ptr_t * vMoves;
     Abc_Obj_t * pNode;
@@ -72,7 +72,7 @@ void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
+void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Vec_Ptr_t * vMoves;
     Abc_Obj_t * pNode;
@@ -83,7 +83,7 @@ void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
     Vec_PtrForEachEntryReverse( vMoves, pNode, i )
         Abc_ObjRetimeForwardTry( pNode, 1 );
     // implement this backward retiming
-    RetValue = Abc_NtkImplementRetimingBackward( pNtk, vMoves );
+    RetValue = Abc_NtkImplementRetimingBackward( pNtk, vMoves, fVerbose );
     Vec_PtrFree( vMoves ); 
     if ( RetValue == 0 )
         printf( "Retiming completed but initial state computation has failed.\n" );
@@ -100,14 +100,14 @@ void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk )
+void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Vec_Str_t * vLags;
     int RetValue;
     // get the retiming vector
-    vLags = Abc_NtkSeqRetimeDelayLags( pNtk );
+    vLags = Abc_NtkSeqRetimeDelayLags( pNtk, fVerbose );
     // implement this retiming
-    RetValue = Abc_NtkImplementRetiming( pNtk, vLags );
+    RetValue = Abc_NtkImplementRetiming( pNtk, vLags, fVerbose );
     Vec_StrFree( vLags ); 
     if ( RetValue == 0 )
         printf( "Retiming completed but initial state computation has failed.\n" );
@@ -124,14 +124,14 @@ void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSeqRetimeInitial( Abc_Ntk_t * pNtk )
+void Abc_NtkSeqRetimeInitial( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Vec_Str_t * vLags;
     int RetValue;
     // get the retiming vector
-    vLags = Abc_NtkSeqRetimeDelayLags( pNtk );
+    vLags = Abc_NtkSeqRetimeDelayLags( pNtk, fVerbose );
     // implement this retiming
-    RetValue = Abc_NtkImplementRetiming( pNtk, vLags );
+    RetValue = Abc_NtkImplementRetiming( pNtk, vLags, fVerbose );
     Vec_StrFree( vLags ); 
     if ( RetValue == 0 )
         printf( "Retiming completed but initial state computation has failed.\n" );
diff --git a/src/base/abcs/abcRetDelay.c b/src/base/abcs/abcRetDelay.c
index 277e7750..0697c699 100644
--- a/src/base/abcs/abcRetDelay.c
+++ b/src/base/abcs/abcRetDelay.c
@@ -31,8 +31,8 @@ static inline void Abc_NodeSetLValue( Abc_Obj_t * pNode, int Value )  { Vec_IntW
 static inline int  Abc_NodeGetLag( int LValue, int Fi )               { return (LValue + 256*Fi)/Fi - 256 - (int)(LValue % Fi == 0); }
 
 // the internal procedures
-static int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax );
-static int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi );
+static int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose );
+static int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose );
 static int Abc_NodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
 
 // node status after updating its arrival time
@@ -55,15 +55,15 @@ static void Abc_RetimingExperiment( Abc_Ntk_t * pNtk, Vec_Str_t * vLags );
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
+Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Vec_Str_t * vLags;
     Abc_Obj_t * pNode;
-    int i, FiMax, FiBest;
+    int i, FiMax, FiBest, RetValue;
     assert( Abc_NtkIsSeq( pNtk ) );
 
     // start storage for sequential arrival times
-//    assert( pNtk->pData == NULL );
+    assert( pNtk->pData == NULL );
     pNtk->pData = Vec_IntAlloc( 0 );
 
     // get the upper bound on the clock period
@@ -75,11 +75,17 @@ Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
     FiMax += 2;
 
     // make sure this clock period is feasible
-    assert( Abc_NtkRetimeForPeriod( pNtk, FiMax ) );
+    assert( Abc_NtkRetimeForPeriod( pNtk, FiMax, fVerbose ) );
 
     // search for the optimal clock period between 0 and nLevelMax
-    FiBest = Abc_NtkRetimeSearch_rec( pNtk, 0, FiMax );
+    FiBest = Abc_NtkRetimeSearch_rec( pNtk, 0, FiMax, fVerbose );
+
+    // recompute the best LValues
+    RetValue = Abc_NtkRetimeForPeriod( pNtk, FiBest, fVerbose );
+    assert( RetValue );
+
     // print the result
+    if ( fVerbose )
     printf( "The best clock period is %3d.\n", FiBest );
 
     // convert to lags
@@ -91,9 +97,6 @@ Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
     Abc_AigForEachAnd( pNtk, pNode, i )
         printf( "%d=%d ", i, Abc_NodeReadLValue(pNode) );
     printf( "\n" );
-*/
-
-/*
     printf( "Lags : " );
     Abc_AigForEachAnd( pNtk, pNode, i )
         if ( Vec_StrEntry(vLags,i) != 0 )
@@ -101,8 +104,6 @@ Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
     printf( "\n" );
 */
 
-//    Abc_RetimingExperiment( pNtk, vLags );
-
     // free storage
     Vec_IntFree( pNtk->pData );
     pNtk->pData = NULL;
@@ -120,17 +121,17 @@ Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax )
+int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose )
 {
     int Median;
     assert( FiMin < FiMax );
     if ( FiMin + 1 == FiMax )
         return FiMax;
     Median = FiMin + (FiMax - FiMin)/2;
-    if ( Abc_NtkRetimeForPeriod( pNtk, Median ) )
-        return Abc_NtkRetimeSearch_rec( pNtk, FiMin, Median ); // Median is feasible
+    if ( Abc_NtkRetimeForPeriod( pNtk, Median, fVerbose ) )
+        return Abc_NtkRetimeSearch_rec( pNtk, FiMin, Median, fVerbose ); // Median is feasible
     else 
-        return Abc_NtkRetimeSearch_rec( pNtk, Median, FiMax ); // Median is infeasible
+        return Abc_NtkRetimeSearch_rec( pNtk, Median, FiMax, fVerbose ); // Median is infeasible
 }
 
 /**Function*************************************************************
@@ -213,7 +214,7 @@ int Abc_NtkRetimeForPeriod2( Abc_Ntk_t * pNtk, int Fi )
         printf( "Period = %3d.  Updated nodes = %6d.    Infeasible %s\n", Fi, vFrontier->nSize, pReason );
     else
         printf( "Period = %3d.  Updated nodes = %6d.    Feasible\n",   Fi, vFrontier->nSize );
-//    Vec_PtrFree( vFrontier );
+    Vec_PtrFree( vFrontier );
     return RetValue != ABC_UPDATE_FAIL;
 }
 
@@ -228,7 +229,7 @@ int Abc_NtkRetimeForPeriod2( Abc_Ntk_t * pNtk, int Fi )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
+int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose )
 {
     Abc_Obj_t * pObj;
     int i, c, RetValue, fChange, Counter;
@@ -237,11 +238,13 @@ int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
     // set l-values of all nodes to be minus infinity
     Vec_IntFill( pNtk->pData, Abc_NtkObjNumMax(pNtk), -ABC_INFINITY );
 
+    // set l-values for the constant and PIs
     pObj = Abc_NtkObj( pNtk, 0 );
     Abc_NodeSetLValue( pObj, 0 );
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_NodeSetLValue( pObj, 0 );
 
+    // update all values iteratively
     Counter = 0;
     for ( c = 0; c < 20; c++ )
     {
@@ -272,10 +275,13 @@ int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
     }
 
     // report the results
-    if ( RetValue == ABC_UPDATE_FAIL )
-        printf( "Period = %3d.  Iterations = %3d.  Updates = %6d.  Infeasible %s\n", Fi, c, Counter, pReason );
-    else
-        printf( "Period = %3d.  Iterations = %3d.  Updates = %6d.  Feasible\n",   Fi, c, Counter );
+    if ( fVerbose )
+    {
+        if ( RetValue == ABC_UPDATE_FAIL )
+            printf( "Period = %3d.  Iterations = %3d.  Updates = %6d.  Infeasible %s\n", Fi, c, Counter, pReason );
+        else
+            printf( "Period = %3d.  Iterations = %3d.  Updates = %6d.  Feasible\n",   Fi, c, Counter );
+    }
     return RetValue != ABC_UPDATE_FAIL;
 }
 
diff --git a/src/base/abcs/abcRetImpl.c b/src/base/abcs/abcRetImpl.c
index 0082ff22..93d5566d 100644
--- a/src/base/abcs/abcRetImpl.c
+++ b/src/base/abcs/abcRetImpl.c
@@ -44,7 +44,7 @@ static void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
+int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose )
 {
     Vec_Int_t * vSteps;
     Vec_Ptr_t * vMoves;
@@ -53,8 +53,10 @@ int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
     // forward retiming
     vSteps = Abc_NtkUtilRetimingSplit( vLags, 1 );
     // translate each set of steps into moves
+    if ( fVerbose )
     printf( "The number of forward steps  = %6d.\n", Vec_IntSize(vSteps) );
     vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 1 );
+    if ( fVerbose )
     printf( "The number of forward moves  = %6d.\n", Vec_PtrSize(vMoves) );
     // implement this retiming
     Abc_NtkImplementRetimingForward( pNtk, vMoves );
@@ -64,11 +66,13 @@ int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
     // backward retiming
     vSteps = Abc_NtkUtilRetimingSplit( vLags, 0 );
     // translate each set of steps into moves
+    if ( fVerbose )
     printf( "The number of backward steps = %6d.\n", Vec_IntSize(vSteps) );
     vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 0 );
+    if ( fVerbose )
     printf( "The number of backward moves = %6d.\n", Vec_PtrSize(vMoves) );
     // implement this retiming
-    RetValue = Abc_NtkImplementRetimingBackward( pNtk, vMoves );
+    RetValue = Abc_NtkImplementRetimingBackward( pNtk, vMoves, fVerbose );
     Vec_IntFree( vSteps );
     Vec_PtrFree( vMoves );
     return RetValue;
@@ -156,7 +160,7 @@ void Abc_ObjRetimeForward( Abc_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
+int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose )
 {
     Abc_RetEdge_t RetEdge;
     stmm_table * tTable;
@@ -216,6 +220,7 @@ int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
     Abc_NtkDelete( pNtkProb );
     Vec_IntFree( vValues );
 
+    if ( fVerbose )
     printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) );
 
     // transform the miter into a logic network for efficient CNF construction
@@ -225,6 +230,7 @@ int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
     // solve the miter
 clk = clock();
     RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 );
+if ( fVerbose )
 if ( clock() - clk > 500 )
 {
 PRT( "SAT solving time", clock() - clk );
@@ -289,7 +295,7 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t
     // consider the case when all fanout latchs have don't-care values
     // the new values on the fanin edges will be don't-cares
     if ( !fMet0 && !fMet1 && !fMetN )
-   {
+    {
         // update the fanout edges
         Abc_ObjForEachFanout( pObj, pFanout, i )
             Abc_ObjFaninLDeleteLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout) );
diff --git a/src/base/abcs/abcRetUtil.c b/src/base/abcs/abcRetUtil.c
index b8f2cf25..94825c25 100644
--- a/src/base/abcs/abcRetUtil.c
+++ b/src/base/abcs/abcRetUtil.c
@@ -175,6 +175,14 @@ Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, b
         if ( !fChange )
         {
             printf( "Warning: %d strange steps.\n", Vec_IntSize(vSteps) );
+            /*
+            Vec_IntForEachEntry( vSteps, Number, i )
+            {
+                RetStep = Abc_Int2RetStep( Number );
+                printf( "%d(%d) ", RetStep.iNode, RetStep.nLatches );
+            }
+            printf( "\n" );
+            */
             break;
         }
     }
diff --git a/src/base/abcs/abcs.h b/src/base/abcs/abcs.h
index 9e0669d4..fb45efba 100644
--- a/src/base/abcs/abcs.h
+++ b/src/base/abcs/abcs.h
@@ -214,6 +214,8 @@ static inline void Abc_ObjFaninLInsertLast( Abc_Obj_t * pObj, int Edge, Abc_Init
     unsigned EntryNew = EntryCur | (Init << (2 * Abc_ObjFaninL(pObj, Edge)));
     assert( Init >= 0 && Init < 4 );
     assert( Abc_ObjFaninL(pObj, Edge) < ABC_MAX_EDGE_LATCH );
+    if ( Abc_ObjFaninL(pObj, Edge) >= ABC_MAX_EDGE_LATCH )
+        printf( "The limit on latched on the edge (%d) is exceeded.\n", ABC_MAX_EDGE_LATCH );
     Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
     Abc_ObjAddFaninL( pObj, Edge, 1 );
 }
@@ -293,16 +295,16 @@ static inline void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches )
 ////////////////////////////////////////////////////////////////////////
 
 /*=== abcRetCore.c ===========================================================*/
-extern void               Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkSeqRetimeInitial( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fVerbose );
+extern void               Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fVerbose );
+extern void               Abc_NtkSeqRetimeInitial( Abc_Ntk_t * pNtk, int fVerbose );
+extern void               Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fVerbose );
 /*=== abcRetDelay.c ==========================================================*/
-extern Vec_Str_t *        Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk );
+extern Vec_Str_t *        Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose );
 /*=== abcRetImpl.c ===========================================================*/
-extern int                Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags );
+extern int                Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose );
 extern void               Abc_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves );
-extern int                Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves );
+extern int                Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose );
 /*=== abcRetUtil.c ===========================================================*/
 extern Vec_Ptr_t *        Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward );
 extern Vec_Ptr_t *        Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vNodes, bool fForward );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 7a6ca49f..2f7bd229 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -891,7 +891,7 @@ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
     FileName = argv[util_optind];
     // write the file
     vNodes = Abc_NtkCollectObjects( pAbc->pNtkCur );
-    Io_WriteDot( pAbc->pNtkCur, vNodes, NULL, FileName );
+    Io_WriteDot( pAbc->pNtkCur, vNodes, NULL, FileName, 0 );
     Vec_PtrFree( vNodes );
     return 0;
 
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 6bf3a85c..a5aae529 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -76,7 +76,7 @@ extern int                Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteCnf.c ==========================================================*/
 extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteDot.c ==========================================================*/
-extern void               Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName );
+extern void               Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fMulti );
 /*=== abcWriteEqn.c ==========================================================*/
 extern void               Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteGml.c ==========================================================*/
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index cd297db7..cf4e3d15 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -31,7 +31,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the graph structure of AIG in DOT.]
+  Synopsis    [Writes the graph structure of AIG for DOT.]
 
   Description [Useful for graph visualization using tools such as GraphViz: 
   http://www.graphviz.org/]
@@ -41,7 +41,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName )
+void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fMulti )
 {
     FILE * pFile;
     Abc_Obj_t * pNode, * pTemp, * pPrev;
@@ -177,7 +177,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
     fprintf( pFile, "          fontsize=18,\n" );
     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
     fprintf( pFile, "          label=\"" );
-    fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin );
+    fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin + 1 );
     fprintf( pFile, "\\n" );
     fprintf( pFile, "\"\n" );
     fprintf( pFile, "         ];\n" );
@@ -284,6 +284,29 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
     {
         if ( Abc_ObjFaninNum(pNode) == 0 )
             continue;
+        if ( fMulti && Abc_ObjIsNode(pNode) )
+        {
+            Vec_Ptr_t * vSuper;
+            Abc_Obj_t * pFanin;
+            int k, fCompl;
+            vSuper = (Vec_Ptr_t *)pNode->pCopy;
+            assert( vSuper != NULL );
+            Vec_PtrForEachEntry( vSuper, pFanin, k )
+            {
+                fCompl = Abc_ObjIsComplement(pFanin);
+                pFanin = Abc_ObjRegular(pFanin);
+                if ( !pFanin->fMarkC )
+                    continue;
+                fprintf( pFile, "Node%d",  pNode->Id );
+                fprintf( pFile, " -> " );
+                fprintf( pFile, "Node%d%s",  pFanin->Id, (Abc_ObjIsLatch(pFanin)? "_out":"") );
+                fprintf( pFile, " [" );
+                fprintf( pFile, "style = %s", fCompl? "dotted" : "bold" );
+                fprintf( pFile, "]" );
+                fprintf( pFile, ";\n" );
+            }
+            continue;
+        }
         // generate the edge from this node to the next
         if ( Abc_ObjFanin0(pNode)->fMarkC )
         {
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 6668d088..9311e9ea 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -53,11 +53,14 @@ int main( int argc, char * argv[] )
     char * sCommand, * sOutFile, * sInFile;
     int  fStatus = 0;
     bool fBatch, fInitSource, fInitRead, fFinalWrite;
-    
+
     // added to detect memory leaks:
 #ifdef _DEBUG
     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
 #endif
+    
+//    Npn_Experiment();
+//    Npn_Generate();
 
     // get global frame (singleton pattern)
     // will be initialized on first call
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 904d550f..5305ae31 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -261,6 +261,8 @@ extern int         Extra_Power3( int Num );
 /* the number of combinations of k elements out of n */
 extern int         Extra_NumCombinations( int k, int n  );
 extern int *       Extra_DeriveRadixCode( int Number, int Radix, int nDigits );
+/* counts the number of 1s in the bitstring */
+extern int         Extra_CountOnes( unsigned char * pBytes, int nBytes );
 /* the factorial of number */
 extern int         Extra_Factorial( int n );
 /* the permutation of the given number of elements */
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index 6d771990..75e91cbc 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -209,6 +209,37 @@ int * Extra_DeriveRadixCode( int Number, int Radix, int nDigits )
     return Code;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of ones in the bitstring.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_CountOnes( unsigned char * pBytes, int nBytes )
+{
+    static 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
+    };
+
+    int i, Counter;
+    Counter = 0;
+    for ( i = 0; i < nBytes; i++ )
+        Counter += bit_count[ *(pBytes+i) ];
+    return Counter;
+}
+
 /**Function********************************************************************
 
   Synopsis    [Computes the factorial.]
diff --git a/src/misc/npn/npn.c b/src/misc/npn/npn.c
new file mode 100644
index 00000000..ad4b4de6
--- /dev/null
+++ b/src/misc/npn/npn.c
@@ -0,0 +1,202 @@
+/**CFile****************************************************************
+
+  FileName    [npn.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName []
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: npn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+#include "npn.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int Npn_CompareVecs( void ** p0, void ** p1 );
+static Vec_Int_t * Npn_GetSignature( unsigned uTruth, int nVars );
+static void Npn_VecPrint( FILE * pFile, Vec_Int_t * vVec );
+static int Npn_VecProperty( Vec_Int_t * vVec );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Npn_Experiment()
+{
+    Vec_Int_t ** pVecs;
+    FILE * pFile;
+    int nFuncs, Num, i;
+
+    pFile = fopen( "npn5.txt", "r" );
+    pVecs = ALLOC( Vec_Int_t *, 1000000 );
+    for ( i = 0; ; i++ )
+    {
+        if ( fscanf( pFile, "%x", &Num ) != 1 )
+            break;
+        pVecs[i] = Npn_GetSignature( Num, 5 );
+        if ( Npn_VecProperty( pVecs[i] ) )
+        {
+            printf( "1s = %2d. ", Extra_CountOnes((unsigned char *)&Num, (1 << 5) / 8) );
+            Extra_PrintHex( stdout, Num, 5 ); fprintf( stdout, "\n" );
+        }
+        
+    }
+    nFuncs = i;
+    printf( "Read %d numbers.\n", nFuncs );
+    fclose( pFile );
+    /*
+    // sort the vectors
+    qsort( (void *)pVecs, nFuncs, sizeof(void *), 
+            (int (*)(const void *, const void *)) Npn_CompareVecs );
+    pFile = fopen( "npn5ar.txt", "w" );
+    for ( i = 0; i < nFuncs; i++ )
+    {
+        Npn_VecPrint( pFile, pVecs[i] );
+        Vec_IntFree( pVecs[i] );
+    }
+    fclose( pFile );
+    */
+
+    free( pVecs );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Npn_GetSignature( unsigned uTruth, int nVars )
+{
+    // elementary truth tables
+    static unsigned Signs[5] = {
+        0xAAAAAAAA,    // 1010 1010 1010 1010 1010 1010 1010 1010
+        0xCCCCCCCC,    // 1010 1010 1010 1010 1010 1010 1010 1010
+        0xF0F0F0F0,    // 1111 0000 1111 0000 1111 0000 1111 0000
+        0xFF00FF00,    // 1111 1111 0000 0000 1111 1111 0000 0000
+        0xFFFF0000     // 1111 1111 1111 1111 0000 0000 0000 0000
+    };
+    Vec_Int_t * vVec;
+    unsigned uCofactor;
+    int Count0, Count1, i;
+    int nBytes = (1 << nVars) / 8;
+
+    // collect the number of 1s in each cofactor
+    vVec = Vec_IntAlloc( 5 );
+    for ( i = 0; i < nVars; i++ )
+    {
+        uCofactor = uTruth & ~Signs[i];
+        Count0 = Extra_CountOnes( (unsigned char *)&uCofactor, nBytes );
+        uCofactor = uTruth &  Signs[i];
+        Count1 = Extra_CountOnes( (unsigned char *)&uCofactor, nBytes );
+        if ( Count0 < Count1 )
+            Vec_IntPush( vVec, Count0 );
+        else
+            Vec_IntPush( vVec, Count1 );
+    }
+    // sort them
+    Vec_IntSort( vVec, 0 );
+    return vVec;
+    
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Npn_CompareVecs( void ** p0, void ** p1 )
+{
+    Vec_Int_t * vVec0 = *p0;
+    Vec_Int_t * vVec1 = *p1;
+    int i;
+    assert( vVec0->nSize == vVec1->nSize );
+    for ( i = 0; i < vVec0->nSize; i++ )
+        if ( vVec0->pArray[i] < vVec1->pArray[i] )
+            return -1;
+        else if ( vVec0->pArray[i] > vVec1->pArray[i] )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Npn_VecPrint( FILE * pFile, Vec_Int_t * vVec )
+{
+    int i;
+    for ( i = 0; i < vVec->nSize; i++ )
+        fprintf( pFile, "%2d ", vVec->pArray[i] );
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Npn_VecProperty( Vec_Int_t * vVec )
+{
+    int i;
+    for ( i = 0; i < vVec->nSize; i++ )
+        if ( vVec->pArray[i] != i + 1 )
+            return 0;
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/npn/npn.h b/src/misc/npn/npn.h
new file mode 100644
index 00000000..61aa6297
--- /dev/null
+++ b/src/misc/npn/npn.h
@@ -0,0 +1,105 @@
+/**CFile****************************************************************
+
+  FileName    [npn.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName []
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: npn.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __NPN_H__
+#define __NPN_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+#define EXTRA_WORD_VARS     5
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Extra_BitCharNum( int nVars )  {  if ( nVars <= 3 )  return 1;                return 1 << (nVars - 3); }
+static inline int Extra_BitWordNum( int nVars )  {  if ( nVars <= EXTRA_WORD_VARS )  return 1;  return 1 << (nVars - EXTRA_WORD_VARS); }
+
+static inline int  Extra_BitRead( uint8 * pBits, int iBit )  { return ( (pBits[iBit/8] & (1 << (iBit%8))) > 0 ); }
+static inline void Extra_BitSet( uint8 * pBits, int iBit )   { pBits[iBit/8] |= (1 << (iBit%8));                 }
+static inline void Extra_BitXor( uint8 * pBits, int iBit )   { pBits[iBit/8] ^= (1 << (iBit%8));                 }
+
+static inline void Extra_BitClean( int nVars, uint8 * pBits )
+{
+    unsigned * pWords = (unsigned *)pBits;
+    int i;
+    for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
+        pWords[i] = 0;
+}
+static inline void Extra_BitNot( int nVars, uint8 * pBits )
+{
+    unsigned * pWords = (unsigned *)pBits;
+    int i;
+    for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
+        pWords[i] = ~pWords[i];
+}
+static inline void Extra_BitCopy( int nVars, uint8 * pBits1, uint8 * pBits )
+{
+    unsigned * pWords  = (unsigned *)pBits;
+    unsigned * pWords1 = (unsigned *)pBits1;
+    int i;
+    for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
+        pWords[i] = pWords1[i];
+}
+static inline void Extra_BitAnd( int nVars, uint8 * pBits1, uint8 * pBits2, uint8 * pBits )
+{
+    unsigned * pWords  = (unsigned *)pBits;
+    unsigned * pWords1 = (unsigned *)pBits1;
+    unsigned * pWords2 = (unsigned *)pBits2;
+    int i;
+    for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
+        pWords[i] = pWords1[i] & pWords2[i];
+}
+static inline void Extra_BitSharp( int nVars, uint8 * pBits1, uint8 * pBits2, uint8 * pBits )
+{
+    unsigned * pWords  = (unsigned *)pBits;
+    unsigned * pWords1 = (unsigned *)pBits1;
+    unsigned * pWords2 = (unsigned *)pBits2;
+    int i;
+    for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
+        pWords[i] = pWords1[i] & ~pWords2[i];
+}
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== zzz.c ==========================================================*/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/misc/npn/npnGenStr.c b/src/misc/npn/npnGenStr.c
new file mode 100644
index 00000000..adbfdcdf
--- /dev/null
+++ b/src/misc/npn/npnGenStr.c
@@ -0,0 +1,473 @@
+/**CFile****************************************************************
+
+  FileName    [npnUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName []
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: npnUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+#include "npn.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Vec_Ptr_t * Npn_Generate_rec( int nVars, int fFold );
+static void Npn_GenerateMerge( Vec_Ptr_t * vVec1, Vec_Ptr_t * vVec2, Vec_Ptr_t * vVec );
+static void Npn_GenerateFree( Vec_Ptr_t * vVec );
+static Vec_Ptr_t * Npn_GenerateFold( Vec_Ptr_t * vVec );
+static void Npn_GenerateEmbed( Vec_Ptr_t * vVec );
+static void Npn_GeneratePrint( Vec_Ptr_t * vVec );
+
+
+static void Npn_RewritePrint( Vec_Ptr_t * vVec );
+static Vec_Ptr_t * Npn_Rewrite( char * pStruct );
+
+static int Npn_RewriteNumEntries( char * pString );
+static int Npn_RewriteLastAnd( char * pBeg, char * pString );
+static int Npn_RewriteLastExor( char * pBeg, char * pString );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Npn_Generate()
+{
+    Vec_Ptr_t * vVec;
+    vVec = Npn_Generate_rec( 7, 1 );
+    Npn_GenerateEmbed( vVec );
+    Npn_GeneratePrint( vVec );
+    Npn_GenerateFree( vVec );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Npn_Generate_rec( int nVars, int fFold )
+{
+    char Buffer[20], * pChar;
+    Vec_Ptr_t * vVec, * vVec1, * vVec2, * pTemp;
+    int i;
+
+    vVec = Vec_PtrAlloc( 100 );
+
+    // generate the combination
+    pChar = Buffer;
+    for ( i = 0; i < nVars; i++ )
+        *pChar++ = '.';
+    *pChar++ = 0;
+
+    Vec_PtrPush( vVec, util_strsav(Buffer) );
+    if ( nVars == 2 || !fFold )
+        return vVec;
+
+    assert( nVars > 2 );
+    for ( i = 2; i < nVars; i++ )
+    {
+        vVec1 = Npn_Generate_rec( i, 1 );
+        vVec1 = Npn_GenerateFold( pTemp = vVec1 );
+        Npn_GenerateFree( pTemp );
+        // add folded pairs
+        if ( nVars - i > 1 )
+        {
+            vVec2 = Npn_Generate_rec( nVars - i, 1 );
+            vVec2 = Npn_GenerateFold( pTemp = vVec2 );
+            Npn_GenerateFree( pTemp );
+            Npn_GenerateMerge( vVec1, vVec2, vVec );
+            Npn_GenerateFree( vVec2 );
+        }
+        // add unfolded pairs
+        vVec2 = Npn_Generate_rec( nVars - i, 0 );
+        Npn_GenerateMerge( vVec1, vVec2, vVec );
+        Npn_GenerateFree( vVec2 );
+        Npn_GenerateFree( vVec1 );
+    }
+    return vVec;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Npn_GenerateMerge( Vec_Ptr_t * vVec1, Vec_Ptr_t * vVec2, Vec_Ptr_t * vVec )
+{
+    char Buffer[100];
+    char * pEntry1, * pEntry2, * pEntry;
+    int i, k, m;
+    Vec_PtrForEachEntry( vVec1, pEntry1, i )
+    Vec_PtrForEachEntry( vVec2, pEntry2, k )
+    {
+        if ( *pEntry1 == '(' && *pEntry2 == '(' )
+            if ( strcmp( pEntry1, pEntry2 ) > 0 )
+                continue;
+
+        // get the new entry
+        sprintf( Buffer, "%s%s", pEntry1, pEntry2 );
+        // skip duplicates
+        Vec_PtrForEachEntry( vVec, pEntry, m )
+            if ( strcmp( pEntry, Buffer ) == 0 )
+                break;
+        if ( m != Vec_PtrSize(vVec) )
+            continue;
+        // add the new entry
+        Vec_PtrPush( vVec, util_strsav(Buffer) );
+    }    
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Npn_GenerateFree( Vec_Ptr_t * vVec )
+{
+    char * pEntry;
+    int i;
+    Vec_PtrForEachEntry( vVec, pEntry, i )
+        free( pEntry );
+    Vec_PtrFree( vVec );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Npn_GenerateFold( Vec_Ptr_t * vVec )
+{
+    Vec_Ptr_t * vVecR;
+    char Buffer[100];
+    char * pEntry;
+    int i;
+    vVecR = Vec_PtrAlloc( 10 );
+    Vec_PtrForEachEntry( vVec, pEntry, i )
+    {
+        // add entry without folding if the second part is folded
+        if ( pEntry[strlen(pEntry) - 1] == ')' )
+            Vec_PtrPush( vVecR, util_strsav(pEntry) );
+        // add the entry with folding
+        sprintf( Buffer, "(%s)", pEntry );
+        Vec_PtrPush( vVecR, util_strsav(Buffer) );
+    }
+    return vVecR;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Npn_GenerateEmbed( Vec_Ptr_t * vVec )
+{
+    char Buffer[100];
+    char * pEntry;
+    int i;
+    Vec_PtrForEachEntry( vVec, pEntry, i )
+    {
+        sprintf( Buffer, "(%s)", pEntry );
+        Vec_PtrWriteEntry( vVec, i, util_strsav(Buffer) );
+        free( pEntry );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Npn_GeneratePrint( Vec_Ptr_t * vVec )
+{
+    char * pEntry;
+    int i;
+    Vec_PtrForEachEntry( vVec, pEntry, i )
+    {
+        printf( "%5d : %s\n", i, pEntry );
+
+        {
+            Vec_Ptr_t * vFuncs;
+            vFuncs = Npn_Rewrite( pEntry );
+            Npn_RewritePrint( vFuncs );
+            Vec_PtrFree( vFuncs );
+        }
+    }
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Npn_RewritePrint( Vec_Ptr_t * vVec )
+{
+    char * pEntry;
+    int i;
+    Vec_PtrForEachEntry( vVec, pEntry, i )
+        printf( "    %3d : %s\n", i, pEntry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Npn_Rewrite_rec( char * pStruct, Vec_Ptr_t * vVec, Vec_Str_t * vForm )
+{
+    int nSizeOld;
+    char * pCur;
+    // find the next opening paranthesis
+    for ( pCur = pStruct; *pCur; pCur++ )
+    {
+        if ( *pCur == '(' )
+            break;
+        Vec_StrPush( vForm, *pCur );
+    }
+    // the paranthesis is not found quit
+    if ( *pCur == 0 )
+    {
+        Vec_StrPush( vForm, 0 );
+        Vec_PtrPush( vVec, util_strsav( vForm->pArray ) );
+        return;
+    }
+    assert( *pCur == '(' );
+    pCur++;
+    // remember the current size
+    nSizeOld = vForm->nSize;
+    // add different types
+    if ( Npn_RewriteLastAnd(vForm->pArray, vForm->pArray+vForm->nSize) )
+    {
+        Vec_StrPush( vForm, 'N' );
+        Vec_StrPush( vForm, '(' );
+        Npn_Rewrite_rec( pCur, vVec, vForm );
+        Vec_StrShrink( vForm, nSizeOld );
+    }
+    else
+    {
+        Vec_StrPush( vForm, 'A' );
+        Vec_StrPush( vForm, '(' );
+        Npn_Rewrite_rec( pCur, vVec, vForm );
+        Vec_StrShrink( vForm, nSizeOld );
+    }
+    // add different types
+    if ( Npn_RewriteNumEntries(pCur) == 3 )
+    {
+        Vec_StrPush( vForm, 'P' );
+        Vec_StrPush( vForm, '(' );
+        Npn_Rewrite_rec( pCur, vVec, vForm );
+        Vec_StrShrink( vForm, nSizeOld );
+    }
+    // add different types
+    if ( !Npn_RewriteLastExor(vForm->pArray, vForm->pArray+vForm->nSize) )
+    {
+        Vec_StrPush( vForm, 'X' );
+        Vec_StrPush( vForm, '(' );
+        Npn_Rewrite_rec( pCur, vVec, vForm );
+        Vec_StrShrink( vForm, nSizeOld );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Npn_Rewrite( char * pStruct )
+{
+    Vec_Ptr_t * vVec;
+    Vec_Str_t * vForm;
+    vVec  = Vec_PtrAlloc( 10 );
+    vForm = Vec_StrAlloc( 10 );
+    Npn_Rewrite_rec( pStruct, vVec, vForm );
+    Vec_StrFree( vForm );
+    return vVec;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Npn_RewriteNumEntries( char * pString )
+{
+    char * pCur;
+    int Counter = 0;
+    int nPars = 0;
+    for ( pCur = pString; *pCur; pCur++ )
+    {
+        if ( nPars == 0 )
+        {
+            if ( *pCur == '.' )
+                Counter++;
+            else if ( *pCur == '(' )
+            {
+                Counter++;
+                nPars++;
+            }
+            else if ( *pCur == ')' )
+                nPars--;
+        }
+        else if ( nPars > 0 )
+        {
+            if ( *pCur == '(' )
+                nPars++;
+            else if ( *pCur == ')' )
+                nPars--;
+        }
+        else
+            break;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the last was EXOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Npn_RewriteLastAnd( char * pBeg, char * pEnd )
+{
+    char * pCur;
+    int nPars = 1;
+    for ( pCur = pEnd - 1; pCur >= pBeg; pCur-- )
+    {
+            if ( *pCur == ')' )
+                nPars++;
+            else if ( *pCur == '(' )
+                nPars--;
+
+            if ( nPars == 0 && *pCur == 'A' )
+                return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the last was EXOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Npn_RewriteLastExor( char * pBeg, char * pEnd )
+{
+    char * pCur;
+    int nPars = 1;
+    for ( pCur = pEnd - 1; pCur >= pBeg; pCur-- )
+    {
+            if ( *pCur == ')' )
+                nPars++;
+            else if ( *pCur == '(' )
+                nPars--;
+
+            if ( nPars == 0 && *pCur == 'X' )
+                return 1;
+    }
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/npn/npnTruth.c b/src/misc/npn/npnTruth.c
new file mode 100644
index 00000000..b6be775b
--- /dev/null
+++ b/src/misc/npn/npnTruth.c
@@ -0,0 +1,137 @@
+/**CFile****************************************************************
+
+  FileName    [npnUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName []
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: npnUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+#include "npn.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the variable belongs to the support.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_TruthCofactors( int nVars, uint8 * puTruth, uint8 * puElem[][32], 
+    uint8 * puTruthCofs0[][32], uint8 * puTruthCofs1[][32] )
+{
+    int v;
+    for ( v = 0; v < nVars; v++ )
+    {
+        Extra_BitSharp( nVars, puTruth, puElem[v], (uint8 *)puTruthCofs0[v] );
+        Extra_BitAnd  ( nVars, puTruth, puElem[v], (uint8 *)puTruthCofs1[v] );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the variable belongs to the support.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_TruthCountCofactorOnes( int nVars, uint8 * puTruthCofs[][32], int * pCounts )
+{
+    int v, nBytes;
+    nBytes = Extra_BitCharNum( nVars );
+    for ( v = 0; v < nVars; v++ )
+        pCounts[v] = Extra_CountOnes( puTruthCofs[v], nBytes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the variable belongs to the support.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Extra_TruthHasVar( int nVars, uint8 * puTruth, int iVar )
+{
+    // elementary truth tables
+    static uint8 Signs[3] = {
+        0xAA,    // 1010 1010
+        0xCC,    // 1100 1100
+        0xF0     // 1111 0000
+    };
+    int nChars, nShift, i;
+    assert( iVar < nVars );
+    nChars = Extra_BitCharNum( nVars );
+    if ( iVar < 3 )
+    {
+        nShift = (1 << iVar);
+        for ( i = 0; i < nChars; i++ )
+            if ( ((puTruth[i] & Signs[iVar]) >> nShift) != (puTruth[i] & ~Signs[iVar]) )
+                return 1;
+    }
+    else
+    {
+        nShift = (1 << (iVar-3));
+        for ( i = 0; i < nChars; i++, i = (i % nShift)? i : i + nShift )
+            if ( puTruth[i] != puTruth[i+nShift] )
+                return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the variable belongs to the support.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Npn_VarsTest( int nVars, uint8 * puTruth )
+{
+    int v;
+    int Counter = 0;
+    for ( v = 0; v < nVars; v++ )
+        Counter += Extra_TruthHasVar( nVars, puTruth, v );
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/npn/npnUtil.c b/src/misc/npn/npnUtil.c
new file mode 100644
index 00000000..b12ad092
--- /dev/null
+++ b/src/misc/npn/npnUtil.c
@@ -0,0 +1,78 @@
+/**CFile****************************************************************
+
+  FileName    [npnUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName []
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: npnUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+#include "npn.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Npn_StartTruth8( uint8 uTruths[][32] )
+{
+    // elementary truth tables
+    static uint8 Signs[3] = {
+        0xAA,    // 1010 1010
+        0xCC,    // 1100 1100
+        0xF0     // 1111 0000
+    };
+    int v, i, nShift;
+    for ( v = 0; v < 3; v++ )
+        for ( i = 0; i < 32; i++ )
+            uTruths[v][i] = Signs[v];
+    for ( v = 3; v < 8; v++ )
+    {
+        nShift = (1 << (v-3));
+        for ( i = 0; i < 32; i++, i = (i % nShift)? i : i + nShift )
+        {
+            uTruths[v][i]          = 0;
+            uTruths[v][i + nShift] = 0xFF;
+        }
+    }
+/*
+    for ( v = 0; v < 8; v++ )
+    {
+        Extra_PrintBinary( stdout, (unsigned int*)uTruths[v], 90 );
+        printf( "\n" );
+    }
+*/
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index 49dde875..ecdfed72 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -42,21 +42,23 @@ struct Cut_ParamsStruct_t_
     int  nVarsMax;      // the max cut size ("k" of the k-feasible cuts)
     int  nKeepMax;      // the max number of cuts kept at a node
     int  nIdsMax;       // the max number of IDs of cut objects
+    int  nCutSet;       // the number of nodes in the cut set
     int  fTruth;        // compute truth tables
     int  fFilter;       // filter dominated cuts
     int  fSeq;          // compute sequential cuts
     int  fDrop;         // drop cuts on the fly
+    int  fMulti;        // compute cuts in multi-input AND gate graph
     int  fVerbose;      // the verbosiness flag
 };
 
 struct Cut_CutStruct_t_
 {
     unsigned           uTruth     : 16;   // truth table for 4-input cuts
-    unsigned           uPhase     :  8;   // the phase when mapping into a canonical form
+    unsigned           uPhase     :  6;   // the phase when mapping into a canonical form
     unsigned           fSimul     :  1;   // the value of cut's output at 000.. pattern
     unsigned           fCompl     :  1;   // the cut is complemented
-    unsigned           nVarsMax   :  3;   // the max number of vars [4-6]
-    unsigned           nLeaves    :  3;   // the number of leaves [4-6]
+    unsigned           nVarsMax   :  4;   // the max number of vars [4-6]
+    unsigned           nLeaves    :  4;   // the number of leaves [4-6]
     unsigned           uSign;             // the signature
     Cut_Cut_t *        pNext;             // the next cut in the list
     int                pLeaves[0];        // the array of leaves
@@ -82,22 +84,34 @@ static inline void       Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth )
 ////////////////////////////////////////////////////////////////////////
 
 /*=== cutApi.c ==========================================================*/
-extern Cut_Cut_t *      Cut_NodeReadCuts( Cut_Man_t * p, int Node );
-extern void             Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList );
+extern Cut_Cut_t *      Cut_NodeReadCutsNew( Cut_Man_t * p, int Node );
+extern Cut_Cut_t *      Cut_NodeReadCutsOld( Cut_Man_t * p, int Node );
+extern Cut_Cut_t *      Cut_NodeReadCutsTemp( Cut_Man_t * p, int Node );
+extern void             Cut_NodeWriteCutsNew( Cut_Man_t * p, int Node, Cut_Cut_t * pList );
+extern void             Cut_NodeWriteCutsOld( Cut_Man_t * p, int Node, Cut_Cut_t * pList );
+extern void             Cut_NodeWriteCutsTemp( Cut_Man_t * p, int Node, Cut_Cut_t * pList );
 extern void             Cut_NodeSetTriv( Cut_Man_t * p, int Node );
 extern void             Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node );
 extern void             Cut_NodeFreeCuts( Cut_Man_t * p, int Node );
 /*=== cutCut.c ==========================================================*/
-extern void             Cut_CutPrint( Cut_Cut_t * pCut );
+extern void             Cut_CutPrint( Cut_Cut_t * pCut, int fSeq );
+extern void             Cut_CutPrintList( Cut_Cut_t * pList, int fSeq );
 /*=== cutMan.c ==========================================================*/
 extern Cut_Man_t *      Cut_ManStart( Cut_Params_t * pParams );
 extern void             Cut_ManStop( Cut_Man_t * p );
 extern void             Cut_ManPrintStats( Cut_Man_t * p );
+extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, int TimeTotal );
 extern void             Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
 extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
 /*=== cutNode.c ==========================================================*/
-extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 ); 
+extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fNew0, int fNew1, int fTriv ); 
+extern Cut_Cut_t *      Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fNew0, int fNew1, int fTriv ); 
 extern Cut_Cut_t *      Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
+/*=== cutSeq.c ==========================================================*/
+extern void             Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int nLat0, int nLat1, int fTriv, int CutSetNum );
+extern void             Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node );
+extern int              Cut_NodeTempTransferToNew( Cut_Man_t * p, int Node, int CutSetNum );
+extern void             Cut_NodeOldTransferToNew( Cut_Man_t * p, int Node );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutApi.c b/src/opt/cut/cutApi.c
index 0e7c2506..8751f521 100644
--- a/src/opt/cut/cutApi.c
+++ b/src/opt/cut/cutApi.c
@@ -39,11 +39,11 @@
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
+Cut_Cut_t * Cut_NodeReadCutsNew( Cut_Man_t * p, int Node )
 {
-    if ( Node >= p->vCuts->nSize )
+    if ( Node >= p->vCutsNew->nSize )
         return NULL;
-    return Vec_PtrEntry( p->vCuts, Node );
+    return Vec_PtrEntry( p->vCutsNew, Node );
 }
 
 /**Function*************************************************************
@@ -57,9 +57,75 @@ Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
+Cut_Cut_t * Cut_NodeReadCutsOld( Cut_Man_t * p, int Node )
 {
-    Vec_PtrWriteEntry( p->vCuts, Node, pList );
+    assert( Node < p->vCutsOld->nSize );
+    return Vec_PtrEntry( p->vCutsOld, Node );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the linked list of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeReadCutsTemp( Cut_Man_t * p, int Node )
+{
+    assert( Node < p->vCutsTemp->nSize );
+    return Vec_PtrEntry( p->vCutsTemp, Node );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the linked list of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeWriteCutsNew( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
+{
+    Vec_PtrWriteEntry( p->vCutsNew, Node, pList );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the linked list of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeWriteCutsOld( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
+{
+    Vec_PtrWriteEntry( p->vCutsOld, Node, pList );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the linked list of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeWriteCutsTemp( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
+{
+    Vec_PtrWriteEntry( p->vCutsTemp, Node, pList );
 }
 
 /**Function*************************************************************
@@ -75,8 +141,8 @@ void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
 ***********************************************************************/
 void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
 {
-    assert( Cut_NodeReadCuts(p, Node) == NULL );
-    Cut_NodeWriteCuts( p, Node, Cut_CutCreateTriv(p, Node) );
+    assert( Cut_NodeReadCutsNew(p, Node) == NULL );
+    Cut_NodeWriteCutsNew( p, Node, Cut_CutCreateTriv(p, Node) );
 }
 
 /**Function*************************************************************
@@ -115,12 +181,12 @@ void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node )
 void Cut_NodeFreeCuts( Cut_Man_t * p, int Node )
 {
     Cut_Cut_t * pList, * pCut, * pCut2;
-    pList = Cut_NodeReadCuts( p, Node );
+    pList = Cut_NodeReadCutsNew( p, Node );
     if ( pList == NULL )
         return;
     Cut_ListForEachCutSafe( pList, pCut, pCut2 )
         Cut_CutRecycle( p, pCut );
-    Cut_NodeWriteCuts( p, Node, NULL );
+    Cut_NodeWriteCutsNew( p, Node, NULL );
 }
 
 
diff --git a/src/opt/cut/cutCut.c b/src/opt/cut/cutCut.c
index d2cce61f..95916960 100644
--- a/src/opt/cut/cutCut.c
+++ b/src/opt/cut/cutCut.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "cutInt.h"
+#include "npn.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -69,12 +70,19 @@ Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p )
 Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
 {
     Cut_Cut_t * pCut;
+    if ( p->pParams->fSeq )
+        Node <<= 8;
     pCut = Cut_CutAlloc( p );
     pCut->nLeaves    = 1;
     pCut->pLeaves[0] = Node;
-    pCut->uSign      = (1 << (Node % 32));
+    pCut->uSign      = Cut_NodeSign( Node );
     if ( p->pParams->fTruth )
-        Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
+    {
+        if ( pCut->nVarsMax == 4 )
+            Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
+        else
+            Extra_BitCopy( pCut->nLeaves, p->uTruths[0], (uint8*)Cut_CutReadTruth(pCut) );
+    }
     p->nCutsTriv++;
     return pCut;
 } 
@@ -111,14 +119,43 @@ void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_CutPrint( Cut_Cut_t * pCut )
+void Cut_CutPrint( Cut_Cut_t * pCut, int fSeq )
 {
     int i;
     assert( pCut->nLeaves > 0 );
     printf( "%d : {", pCut->nLeaves );
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
-        printf( " %d", pCut->pLeaves[i] );
+    {
+        if ( fSeq )
+        {
+            printf( " %d", pCut->pLeaves[i] >> 8 );
+            if ( pCut->pLeaves[i] & 0xFF )
+                printf( "(%d)", pCut->pLeaves[i] & 0xFF );
+        }
+        else
+            printf( " %d", pCut->pLeaves[i] );
+    }
     printf( " }" );
+//    printf( "\nSign = " );
+//    Extra_PrintBinary( stdout, &pCut->uSign, 32 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CutPrintList( Cut_Cut_t * pList, int fSeq )
+{
+    Cut_Cut_t * pCut;
+    for ( pCut = pList; pCut; pCut = pCut->pNext )
+        Cut_CutPrint( pCut, fSeq ), printf( "\n" );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index 2d4443f1..f4178ec8 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -34,6 +34,9 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#define CUT_SIZE_MAX 8
+#include "cutList.h"
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -41,13 +44,14 @@
 typedef struct Cut_HashTableStruct_t_ Cut_HashTable_t;
 
 struct Cut_ManStruct_t_
-{
+{ 
     // user preferences
     Cut_Params_t *     pParams;          // computation parameters
     Vec_Int_t *        vFanCounts;       // the array of fanout counters
     // storage for cuts
-    Vec_Ptr_t *        vCuts;            // cuts by ID
-    Vec_Ptr_t *        vCutsNew;         // cuts by ID
+    Vec_Ptr_t *        vCutsNew;         // new cuts by node ID
+    Vec_Ptr_t *        vCutsOld;         // old cuts by node ID
+    Vec_Ptr_t *        vCutsTemp;        // temp cuts for cutset nodes by cutset node number
     // memory management
     Extra_MmFixed_t *  pMmCuts;
     int                EntrySize;
@@ -59,12 +63,14 @@ struct Cut_ManStruct_t_
     int                fSimul;
     int                nNodeCuts;
     // precomputations
+    uint8              uTruths[8][32];
     unsigned           uTruthVars[6][2];
     unsigned short **  pPerms43;
     unsigned **        pPerms53;
     unsigned **        pPerms54;
     // statistics
     int                nCutsCur;
+    int                nCutsMulti;
     int                nCutsAlloc;
     int                nCutsDealloc;
     int                nCutsPeak;
@@ -72,6 +78,7 @@ struct Cut_ManStruct_t_
     int                nCutsFilter;
     int                nCutsLimit;
     int                nNodes;
+    int                nNodesMulti;
     // runtime
     int                timeMerge;
     int                timeUnion;
@@ -100,6 +107,9 @@ struct Cut_ManStruct_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+// computes signature of the node
+static inline unsigned Cut_NodeSign( int Node )  { return (1 << (Node % 31)); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -108,7 +118,6 @@ struct Cut_ManStruct_t_
 extern Cut_Cut_t *         Cut_CutAlloc( Cut_Man_t * p );
 extern Cut_Cut_t *         Cut_CutCreateTriv( Cut_Man_t * p, int Node );
 extern void                Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut );
-extern void                Cut_CutPrint( Cut_Cut_t * pCut );
 extern void                Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
 /*=== cutMerge.c ==========================================================*/
 extern Cut_Cut_t *         Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
diff --git a/src/opt/cut/cutList.h b/src/opt/cut/cutList.h
index eb008ef9..fd707e6e 100644
--- a/src/opt/cut/cutList.h
+++ b/src/opt/cut/cutList.h
@@ -36,8 +36,8 @@
 typedef struct Cut_ListStruct_t_         Cut_List_t;
 struct Cut_ListStruct_t_
 {
-    Cut_Cut_t *  pHead[7];
-    Cut_Cut_t ** ppTail[7];
+    Cut_Cut_t *  pHead[CUT_SIZE_MAX+1];
+    Cut_Cut_t ** ppTail[CUT_SIZE_MAX+1];
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -50,7 +50,7 @@ struct Cut_ListStruct_t_
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Start the cut list.]
 
   Description []
                
@@ -62,7 +62,7 @@ struct Cut_ListStruct_t_
 static inline void Cut_ListStart( Cut_List_t * p )
 {
     int i;
-    for ( i = 1; i <= 6; i++ )
+    for ( i = 1; i <= CUT_SIZE_MAX; i++ )
     {
         p->pHead[i] = 0;
         p->ppTail[i] = &p->pHead[i];
@@ -71,7 +71,7 @@ static inline void Cut_ListStart( Cut_List_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Adds one cut to the cut list.]
 
   Description []
                
@@ -82,14 +82,65 @@ static inline void Cut_ListStart( Cut_List_t * p )
 ***********************************************************************/
 static inline void Cut_ListAdd( Cut_List_t * p, Cut_Cut_t * pCut )
 {
-    assert( pCut->nLeaves > 0 && pCut->nLeaves < 7 );
+    assert( pCut->nLeaves > 0 && pCut->nLeaves <= CUT_SIZE_MAX );
     *p->ppTail[pCut->nLeaves] = pCut;
     p->ppTail[pCut->nLeaves] = &pCut->pNext;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Adds one cut to the cut list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cut_ListDerive( Cut_List_t * p, Cut_Cut_t * pList )
+{
+    Cut_Cut_t * pPrev;
+    int nLeaves;
+    Cut_ListStart( p );
+    while ( pList != NULL )
+    {
+        nLeaves = pList->nLeaves;
+        p->pHead[nLeaves] = pList;
+        for ( pPrev = pList, pList = pList->pNext; pList; pPrev = pList, pList = pList->pNext )
+            if ( nLeaves < (int)pList->nLeaves )
+                break;
+        p->ppTail[nLeaves] = &pPrev->pNext;
+        pPrev->pNext = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the second list to the first list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cut_ListAddList( Cut_List_t * pOld, Cut_List_t * pNew )
+{
+    int i;
+    for ( i = 1; i <= CUT_SIZE_MAX; i++ )
+    {
+        if ( pNew->pHead[i] == NULL )
+            continue;
+        *pOld->ppTail[i] = pNew->pHead[i];
+        pOld->ppTail[i] = pNew->ppTail[i];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the cut list linked into one sequence of cuts.]
 
   Description []
                
@@ -100,11 +151,17 @@ static inline void Cut_ListAdd( Cut_List_t * p, Cut_Cut_t * pCut )
 ***********************************************************************/
 static inline Cut_Cut_t * Cut_ListFinish( Cut_List_t * p )
 {
+    Cut_Cut_t * pHead = NULL, ** ppTail = &pHead;
     int i;
-    for ( i = 1; i < 6; i++ )
-        *p->ppTail[i] = p->pHead[i+1];
-    *p->ppTail[6] = NULL;
-    return p->pHead[1];
+    for ( i = 1; i < CUT_SIZE_MAX; i++ )
+    {
+        if ( p->pHead[i] == NULL )
+            continue;
+        *ppTail = p->pHead[i];
+        ppTail = p->ppTail[i];
+    }
+    *ppTail = NULL;
+    return pHead;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index 31e003cf..c9dccb6a 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -24,6 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern void Npn_StartTruth8( uint8 uTruths[][32] );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -43,32 +45,32 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
 {
     Cut_Man_t * p;
     int clk = clock();
-    assert( pParams->nVarsMax >= 4 && pParams->nVarsMax <= 6 );
+    assert( pParams->nVarsMax >= 4 && pParams->nVarsMax <= CUT_SIZE_MAX );
     p = ALLOC( Cut_Man_t, 1 );
     memset( p, 0, sizeof(Cut_Man_t) );
     // set and correct parameters
     p->pParams = pParams;
-    if ( p->pParams->fSeq )
-        p->pParams->fFilter = 1;
-    // space for cuts
-    p->vCuts = Vec_PtrAlloc( pParams->nIdsMax );
-    Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
+    // prepare storage for cuts
+    p->vCutsNew = Vec_PtrAlloc( pParams->nIdsMax );
+    Vec_PtrFill( p->vCutsNew, pParams->nIdsMax, NULL );
+    // prepare storage for sequential cuts
     if ( pParams->fSeq )
     {
-        p->vCutsNew = Vec_PtrAlloc( pParams->nIdsMax );
-        Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
+        p->pParams->fFilter = 1;
+        p->vCutsOld = Vec_PtrAlloc( pParams->nIdsMax );
+        Vec_PtrFill( p->vCutsOld, pParams->nIdsMax, NULL );
+        p->vCutsTemp = Vec_PtrAlloc( pParams->nCutSet );
+        Vec_PtrFill( p->vCutsTemp, pParams->nCutSet, NULL );
     }
+    assert( !pParams->fTruth || pParams->nVarsMax <= 5 );
     // entry size
-    p->EntrySize = sizeof(Cut_Cut_t) + (pParams->nVarsMax + pParams->fSeq) * sizeof(int);
-    if ( pParams->fTruth )
-    {
-        if ( pParams->nVarsMax == 5 )
-            p->EntrySize += sizeof(unsigned);
-        else if ( pParams->nVarsMax == 6 )
-            p->EntrySize += 2 * sizeof(unsigned);
-    }
+    p->EntrySize = sizeof(Cut_Cut_t) + pParams->nVarsMax * sizeof(int);
+    if ( pParams->fTruth && pParams->nVarsMax >= 5 && pParams->nVarsMax <= 8 )
+        p->EntrySize += (1 << (pParams->nVarsMax - 5)) * sizeof(unsigned);
     // memory for cuts
     p->pMmCuts = Extra_MmFixedStart( p->EntrySize );
+    // elementary truth tables
+    Npn_StartTruth8( p->uTruths );
     p->uTruthVars[0][1] = p->uTruthVars[0][0] = 0xAAAAAAAA;    // 1010 1010 1010 1010 1010 1010 1010 1010
     p->uTruthVars[1][1] = p->uTruthVars[1][0] = 0xCCCCCCCC;    // 1010 1010 1010 1010 1010 1010 1010 1010
     p->uTruthVars[2][1] = p->uTruthVars[2][0] = 0xF0F0F0F0;    // 1111 0000 1111 0000 1111 0000 1111 0000
@@ -95,13 +97,14 @@ void Cut_ManStop( Cut_Man_t * p )
 {
     Cut_Cut_t * pCut;
     int i;
-    Vec_PtrForEachEntry( p->vCuts, pCut, i )
+    Vec_PtrForEachEntry( p->vCutsNew, pCut, i )
         if ( pCut != NULL )
         {
             int k = 0;
         }
     if ( p->vCutsNew )   Vec_PtrFree( p->vCutsNew );
-    if ( p->vCuts )      Vec_PtrFree( p->vCuts );
+    if ( p->vCutsOld )   Vec_PtrFree( p->vCutsOld );
+    if ( p->vCutsTemp )  Vec_PtrFree( p->vCutsTemp );
     if ( p->vFanCounts ) Vec_IntFree( p->vFanCounts );
     if ( p->pPerms43 )   free( p->pPerms43 );
     if ( p->pPerms53 )   free( p->pPerms53 );
@@ -124,13 +127,18 @@ void Cut_ManStop( Cut_Man_t * p )
 ***********************************************************************/
 void Cut_ManPrintStats( Cut_Man_t * p )
 {
+    if ( p->pReady )
+    {
+        Cut_CutRecycle( p, p->pReady );
+        p->pReady = NULL;
+    }
     printf( "Cut computation statistics:\n" );
     printf( "Current cuts      = %8d. (Trivial = %d.)\n", p->nCutsCur-p->nCutsTriv, p->nCutsTriv );
     printf( "Peak cuts         = %8d.\n", p->nCutsPeak );
     printf( "Total allocated   = %8d.\n", p->nCutsAlloc );
     printf( "Total deallocated = %8d.\n", p->nCutsDealloc );
     printf( "Cuts filtered     = %8d.\n", p->nCutsFilter );
-    printf( "Nodes with limit  = %8d.\n", p->nCutsLimit );
+    printf( "Nodes saturated   = %8d. (Max cuts = %d.)\n", p->nCutsLimit, p->pParams->nKeepMax );
     printf( "Cuts per node     = %8.1f\n", ((float)(p->nCutsCur-p->nCutsTriv))/p->nNodes );
     printf( "The cut size      = %8d bytes.\n", p->EntrySize );
     printf( "Peak memory       = %8.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
@@ -138,8 +146,35 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     PRT( "Union ", p->timeUnion );
     PRT( "Filter", p->timeFilter );
     PRT( "Truth ", p->timeTruth );
+    printf( "Nodes = %d. Multi = %d.  Cuts = %d. Multi = %d.\n", 
+        p->nNodes, p->nNodesMulti, p->nCutsCur-p->nCutsTriv, p->nCutsMulti );
 }
 
+    
+/**Function*************************************************************
+
+  Synopsis    [Prints some interesting stats.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, int TimeTotal )
+{
+    FILE * pTable;
+    pTable = fopen( "cut_stats.txt", "a+" );
+    fprintf( pTable, "%-20s ", pFileName );
+    fprintf( pTable, "%8d ", p->nNodes );
+    fprintf( pTable, "%6.1f ", ((float)(p->nCutsCur))/p->nNodes );
+    fprintf( pTable, "%6.2f ", ((float)(100.0 * p->nCutsLimit))/p->nNodes );
+    fprintf( pTable, "%6.2f ", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
+    fprintf( pTable, "%6.2f ", (float)(TimeTotal)/(float)(CLOCKS_PER_SEC) );
+    fprintf( pTable, "\n" );
+    fclose( pTable );
+}
 
 /**Function*************************************************************
 
diff --git a/src/opt/cut/cutMerge.c b/src/opt/cut/cutMerge.c
index ba1afce4..f9c059bf 100644
--- a/src/opt/cut/cutMerge.c
+++ b/src/opt/cut/cutMerge.c
@@ -39,7 +39,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+Cut_Cut_t * Cut_CutMergeTwo2( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
 { 
     static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}};
     Cut_Cut_t * pRes;
@@ -164,7 +164,7 @@ Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_CutMergeTwo2( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
 { 
     Cut_Cut_t * pRes;
     int * pLeaves;
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index e8a0bc87..0d0ac04c 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "cutInt.h"
-#include "cutList.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -57,6 +56,54 @@ static inline int Cut_CutCheckDominance( Cut_Cut_t * pDom, Cut_Cut_t * pCut )
 
 /**Function*************************************************************
 
+  Synopsis    [Filters cuts using dominance.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList )
+{ 
+    Cut_Cut_t * pListR, ** ppListR = &pListR;
+    Cut_Cut_t * pCut, * pCut2, * pDom, * pPrev;
+    // save the first cut
+    *ppListR = pList, ppListR = &pList->pNext;
+    // try to filter out other cuts
+    pPrev = pList;
+    Cut_ListForEachCutSafe( pList->pNext, pCut, pCut2 )
+    {
+        assert( pCut->nLeaves > 1 );
+        // go through all the previous cuts up to pCut
+        Cut_ListForEachCutStop( pList->pNext, pDom, pCut )
+        {
+            if ( pDom->nLeaves > pCut->nLeaves )
+                continue;
+            if ( (pDom->uSign & pCut->uSign) != pDom->uSign )
+                continue;
+            if ( Cut_CutCheckDominance( pDom, pCut ) )
+                break;
+        }
+        if ( pDom != pCut ) // pDom is contained in pCut - recycle pCut
+        {
+            // make sure cuts are connected after removing
+            pPrev->pNext = pCut->pNext;
+            // recycle the cut
+            Cut_CutRecycle( p, pCut );
+        }
+        else // pDom is NOT contained in pCut - save pCut
+        {
+            *ppListR = pCut, ppListR = &pCut->pNext;
+            pPrev = pCut;
+        }
+    }
+    *ppListR = NULL;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks containment for one cut.]
 
   Description [Returns 1 if the cut is removed.]
@@ -129,50 +176,67 @@ static inline int Cut_CutFilterOne( Cut_Man_t * p, Cut_List_t * pSuperList, Cut_
 
 /**Function*************************************************************
 
-  Synopsis    [Filters cuts using dominance.]
+  Synopsis    [Checks containment for one cut.]
 
-  Description []
+  Description [Returns 1 if the cut is removed.]
                
-  SideEffects []
+  SideEffects [May remove other cuts in the set.]
 
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList )
-{ 
-    Cut_Cut_t * pListR, ** ppListR = &pListR;
-    Cut_Cut_t * pCut, * pCut2, * pDom, * pPrev;
-    // save the first cut
-    *ppListR = pList, ppListR = &pList->pNext;
-    // try to filter out other cuts
-    pPrev = pList;
-    Cut_ListForEachCutSafe( pList->pNext, pCut, pCut2 )
+static inline int Cut_CutFilterOld( Cut_Man_t * p, Cut_Cut_t * pList, Cut_Cut_t * pCut )
+{
+    Cut_Cut_t * pPrev, * pTemp, * pTemp2, ** ppTail;
+
+    if ( pList == NULL )
+        return 0;
+
+    // check if this cut is filtered out by smaller cuts
+    pPrev = NULL;
+    Cut_ListForEachCut( pList, pTemp )
     {
-        assert( pCut->nLeaves > 1 );
-        // go through all the previous cuts up to pCut
-        Cut_ListForEachCutStop( pList->pNext, pDom, pCut )
+        if ( pTemp->nLeaves > pCut->nLeaves )
+            break;
+        pPrev = pTemp;
+        // skip the non-contained cuts
+        if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+            continue;
+        // check containment seriously
+        if ( Cut_CutCheckDominance( pTemp, pCut ) )
         {
-            if ( pDom->nLeaves > pCut->nLeaves )
-                continue;
-            if ( (pDom->uSign & pCut->uSign) != pDom->uSign )
-                continue;
-            if ( Cut_CutCheckDominance( pDom, pCut ) )
-                break;
+            p->nCutsFilter++;
+            Cut_CutRecycle( p, pCut );
+            return 1;
         }
-        if ( pDom != pCut ) // pDom is contained in pCut - recycle pCut
+    }
+    assert( pPrev->pNext == pTemp );
+
+    // filter out other cuts using this one
+    ppTail = &pPrev->pNext;
+    Cut_ListForEachCutSafe( pTemp, pTemp, pTemp2 )
+    {
+        // skip the non-contained cuts
+        if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
         {
-            // make sure cuts are connected after removing
-            pPrev->pNext = pCut->pNext;
-            // recycle the cut
-            Cut_CutRecycle( p, pCut );
+            ppTail = &pTemp->pNext;
+            continue;
         }
-        else // pDom is NOT contained in pCut - save pCut
+        // check containment seriously
+        if ( Cut_CutCheckDominance( pCut, pTemp ) )
         {
-            *ppListR = pCut, ppListR = &pCut->pNext;
-            pPrev = pCut;
+            p->nCutsFilter++;
+            p->nNodeCuts--;
+            // skip the given cut in the list
+            *ppTail = pTemp->pNext;
+            // recycle pTemp
+            Cut_CutRecycle( p, pTemp );
         }
+        else
+            ppTail = &pTemp->pNext;
     }
-    *ppListR = NULL;
+    assert( *ppTail == NULL );
+    return 0;
 }
 
 /**Function*************************************************************
@@ -189,7 +253,6 @@ static inline void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList )
 static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
 {
     Cut_Cut_t * pCut;
-    int RetValue;
     // merge the cuts
     if ( pCut0->nLeaves >= pCut1->nLeaves )
         pCut = Cut_CutMergeTwo( p, pCut0, pCut1 );
@@ -197,13 +260,26 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0,
         pCut = Cut_CutMergeTwo( p, pCut1, pCut0 );
     if ( pCut == NULL )
         return 0;
-    assert( pCut->nLeaves > 1 );
+//    if ( Root == 5 && (pCut->pLeaves[0] >> 8) == 1 && (pCut->pLeaves[1] >> 8) == 4 && (pCut->pLeaves[2] >> 8) == 6 )
+//    {
+//        int x = 0;
+//    }
+    assert( p->pParams->fSeq || pCut->nLeaves > 1 );
     // set the signature
     pCut->uSign = pCut0->uSign | pCut1->uSign;
     // check containment
-    RetValue = p->pParams->fFilter && Cut_CutFilterOne( p, pSuperList, pCut );
-    if ( RetValue )
-        return 0;
+    if ( p->pParams->fFilter )
+    {
+        if ( Cut_CutFilterOne(p, pSuperList, pCut) )
+            return 0;
+        if ( p->pParams->fSeq )
+        {
+            if ( Cut_CutFilterOld(p, Cut_NodeReadCutsOld(p, Root), pCut) )
+                return 0;
+            if ( Cut_CutFilterOld(p, Cut_NodeReadCutsNew(p, Root), pCut) )
+                return 0;
+        }
+    }
     // compute the truth table
     if ( p->pParams->fTruth )
         Cut_TruthCompute( p, pCut, pCut0, pCut1 );
@@ -212,7 +288,43 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0,
     // return status (0 if okay; 1 if exceeded the limit)
     return ++p->nNodeCuts == p->pParams->nKeepMax;
 }
+ 
+/**Function*************************************************************
 
+  Synopsis    [Computes the cuts by merging cuts at two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fNew0, int fNew1, int fTriv )
+{
+    Cut_Cut_t * pList;
+    int clk = clock();
+    // start the number of cuts at the node
+    p->nNodes++;
+    p->nNodeCuts = 0;
+    // compute the cuts
+    pList = Cut_NodeDoComputeCuts( p, Node, Node0, Node1, fCompl0, fCompl1, fNew0, fNew1, fTriv );
+p->timeMerge += clock() - clk;
+    // check if the node is over the list
+    if ( p->nNodeCuts == p->pParams->nKeepMax )
+        p->nCutsLimit++;
+    // set the list at the node
+    Vec_PtrFillExtra( p->vCutsNew, Node + 1, NULL );
+    assert( Cut_NodeReadCutsNew(p, Node) == NULL );
+    Cut_NodeWriteCutsNew( p, Node, pList );
+    // filter the cuts
+//clk = clock();
+//    if ( p->pParams->fFilter )
+//        Cut_CutFilter( p, pList0 );
+//p->timeFilter += clock() - clk;
+    return pList;
+}
+ 
 /**Function*************************************************************
 
   Synopsis    [Computes the cuts by merging cuts at two nodes.]
@@ -224,20 +336,21 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0,
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 )
+Cut_Cut_t * Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fNew0, int fNew1, int fTriv )
 {
     Cut_List_t SuperList;
     Cut_Cut_t * pList0, * pList1, * pStop0, * pStop1, * pTemp0, * pTemp1;
-    int i, Limit = p->pParams->nVarsMax;
-    int clk = clock();
-    assert( p->pParams->nVarsMax <= 6 );
+    int i, nCutsOld, Limit;
 
+    // get the cut lists of children
+    pList0 = fNew0 ? Cut_NodeReadCutsNew(p, Node0) : Cut_NodeReadCutsOld(p, Node0);
+    pList1 = fNew1 ? Cut_NodeReadCutsNew(p, Node1) : Cut_NodeReadCutsOld(p, Node1);
+    if ( pList0 == NULL || pList1 == NULL )
+        return NULL;
     // start the new list
+    nCutsOld = p->nCutsCur;
     Cut_ListStart( &SuperList );
-    // get the cut lists of children
-    pList0 = Cut_NodeReadCuts( p, Node0 );
-    pList1 = Cut_NodeReadCuts( p, Node1 );
-    assert( pList0 && pList1 );
+    Limit = p->pParams->nVarsMax;
     // get the simultation bit of the node
     p->fSimul = (fCompl0 ^ pList0->fSimul) & (fCompl1 ^ pList1->fSimul);
     // set temporary variables
@@ -251,14 +364,18 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
         if ( pStop1->nLeaves == (unsigned)Limit )
             break;
     // start with the elementary cut
-    pTemp0 = Cut_CutCreateTriv( p, Node );
-    Cut_ListAdd( &SuperList, pTemp0 );
-    p->nNodeCuts = 1;
+    if ( fTriv ) 
+    {
+        pTemp0 = Cut_CutCreateTriv( p, Node );
+        Cut_ListAdd( &SuperList, pTemp0 );
+        p->nNodeCuts++;
+        nCutsOld++;
+    }
     // small by small
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
-            goto finish;
+            return Cut_ListFinish( &SuperList );
     // small by large
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCut( pStop1, pTemp1 )
@@ -266,7 +383,7 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
         if ( (pTemp0->uSign & pTemp1->uSign) != pTemp0->uSign )
             continue;
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
-            goto finish;
+            return Cut_ListFinish( &SuperList );
     }
     // small by large
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
@@ -275,7 +392,7 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
         if ( (pTemp0->uSign & pTemp1->uSign) != pTemp1->uSign )
             continue;
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
-            goto finish;
+            return Cut_ListFinish( &SuperList );
     }
     // large by large
     Cut_ListForEachCut( pStop0, pTemp0 )
@@ -290,30 +407,14 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
         if ( i < Limit )
             continue;
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
-            goto finish;
-    }
-finish :
-    if ( p->nNodeCuts == p->pParams->nKeepMax )
-        p->nCutsLimit++;
-    // set the list at the node
-    Vec_PtrFillExtra( p->vCuts, Node + 1, NULL );
-    assert( Cut_NodeReadCuts(p, Node) == NULL );
-    pList0 = Cut_ListFinish( &SuperList );
-    Cut_NodeWriteCuts( p, Node, pList0 );
-    // consider dropping the fanins cuts
-    if ( p->pParams->fDrop )
+            return Cut_ListFinish( &SuperList );
+    } 
+    if ( fTriv ) 
     {
-        Cut_NodeTryDroppingCuts( p, Node0 );
-        Cut_NodeTryDroppingCuts( p, Node1 );
+        p->nCutsMulti += p->nCutsCur - nCutsOld;         
+        p->nNodesMulti++;
     }
-p->timeMerge += clock() - clk;
-    // filter the cuts
-clk = clock();
-//    if ( p->pParams->fFilter )
-//        Cut_CutFilter( p, pList0 );
-p->timeFilter += clock() - clk;
-    p->nNodes++;
-    return pList0;
+    return Cut_ListFinish( &SuperList );
 }
 
 /**Function*************************************************************
@@ -348,8 +449,8 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
     Vec_IntForEachEntry( vNodes, Node, i )
     {
         // get the cuts of this node
-        pList = Cut_NodeReadCuts( p, Node );
-        Cut_NodeWriteCuts( p, Node, NULL );
+        pList = Cut_NodeReadCutsNew( p, Node );
+        Cut_NodeWriteCutsNew( p, Node, NULL );
         assert( pList );
         // remember the starting point
         pListStart = pList->pNext;
@@ -421,15 +522,15 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
     }
 finish :
     // set the cuts at the node
-    assert( Cut_NodeReadCuts(p, Root) == NULL );
+    assert( Cut_NodeReadCutsNew(p, Root) == NULL );
     pList = Cut_ListFinish( &SuperList );
-    Cut_NodeWriteCuts( p, Root, pList );
+    Cut_NodeWriteCutsNew( p, Root, pList );
 p->timeUnion += clock() - clk;
     // filter the cuts
-clk = clock();
+//clk = clock();
 //    if ( p->pParams->fFilter )
 //        Cut_CutFilter( p, pList );
-p->timeFilter += clock() - clk;
+//p->timeFilter += clock() - clk;
     p->nNodes -= vNodes->nSize - 1;
     return pList;
 }
diff --git a/src/opt/cut/cutSeq.c b/src/opt/cut/cutSeq.c
index 869bd7b3..a1887608 100644
--- a/src/opt/cut/cutSeq.c
+++ b/src/opt/cut/cutSeq.c
@@ -24,12 +24,195 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static void Cut_NodeShiftLat( Cut_Man_t * p, int Node, int nLat );
+static int  Cut_ListCount( Cut_Cut_t * pList );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Computes sequential cuts for the node from its fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int nLat0, int nLat1, int fTriv, int CutSetNum )
+{
+    Cut_List_t List1, List2, List3;
+    Cut_Cut_t * pList1, * pList2, * pList3, * pListNew;
+    int clk = clock();
+
+//    assert( Node != Node0 );
+//    assert( Node != Node1 );
+
+    // get the number of cuts at the node
+    p->nNodeCuts = Cut_ListCount( Cut_NodeReadCutsOld(p, Node) );
+    if ( p->nNodeCuts >= p->pParams->nKeepMax )
+        return;
+    // count only the first visit
+    if ( p->nNodeCuts == 0 )
+        p->nNodes++;
+
+    // shift the cuts by as many latches
+    if ( nLat0 ) Cut_NodeShiftLat( p, Node0, nLat0 );
+    if ( nLat1 ) Cut_NodeShiftLat( p, Node1, nLat1 );
+
+    // merge the old and new
+    pList1 = Cut_NodeDoComputeCuts( p, Node, Node0, Node1, fCompl0, fCompl1, 0, 1, 0 );
+    // merge the new and old
+    pList2 = Cut_NodeDoComputeCuts( p, Node, Node0, Node1, fCompl0, fCompl1, 1, 0, 0 );
+    // merge the new and new
+    pList3 = Cut_NodeDoComputeCuts( p, Node, Node0, Node1, fCompl0, fCompl1, 1, 1, fTriv );
+p->timeMerge += clock() - clk;
+
+    // merge all lists
+    Cut_ListDerive( &List1, pList1 );
+    Cut_ListDerive( &List2, pList2 );
+    Cut_ListDerive( &List3, pList3 );
+    Cut_ListAddList( &List1, &List2 );
+    Cut_ListAddList( &List1, &List3 );
+
+    // set the lists at the node
+    pListNew = Cut_ListFinish( &List1 );
+    if ( CutSetNum >= 0 )
+    {
+        assert( Cut_NodeReadCutsTemp(p, CutSetNum) == NULL );
+        Cut_NodeWriteCutsTemp( p, CutSetNum, pListNew );
+    }
+    else
+    {
+        assert( Cut_NodeReadCutsNew(p, Node) == NULL );
+        Cut_NodeWriteCutsNew( p, Node, pListNew );
+    }
+
+    // shift the cuts by as many latches back
+    if ( nLat0 ) Cut_NodeShiftLat( p, Node0, -nLat0 );
+    if ( nLat1 ) Cut_NodeShiftLat( p, Node1, -nLat1 );
+
+    if ( p->nNodeCuts >= p->pParams->nKeepMax )
+        p->nCutsLimit++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node )
+{
+    Cut_List_t Old, New;
+    Cut_Cut_t * pListOld, * pListNew;
+    // get the new cuts
+    pListNew = Cut_NodeReadCutsNew( p, Node );
+    if ( pListNew == NULL )
+        return;
+    Cut_NodeWriteCutsNew( p, Node, NULL );
+    // get the old cuts
+    pListOld = Cut_NodeReadCutsOld( p, Node );
+    if ( pListOld == NULL )
+    {
+        Cut_NodeWriteCutsOld( p, Node, pListNew );
+        return;
+    }
+    // merge the lists
+    Cut_ListDerive( &Old, pListOld );
+    Cut_ListDerive( &New, pListNew );
+    Cut_ListAddList( &Old, &New );
+    pListOld = Cut_ListFinish( &Old );
+    Cut_NodeWriteCutsOld( p, Node, pListOld );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if something was transferred.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_NodeTempTransferToNew( Cut_Man_t * p, int Node, int CutSetNum )
+{
+    Cut_Cut_t * pCut;
+    pCut = Cut_NodeReadCutsTemp( p, CutSetNum );
+    Cut_NodeWriteCutsTemp( p, CutSetNum, NULL );
+    Cut_NodeWriteCutsNew( p, Node, pCut );
+    return pCut != NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if something was transferred.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeOldTransferToNew( Cut_Man_t * p, int Node )
+{
+    Cut_Cut_t * pCut;
+    pCut = Cut_NodeReadCutsOld( p, Node );
+    Cut_NodeWriteCutsOld( p, Node, NULL );
+    Cut_NodeWriteCutsNew( p, Node, pCut );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeShiftLat( Cut_Man_t * p, int Node, int nLat )
+{
+    Cut_Cut_t * pTemp;
+    int i;
+    // shift the cuts by as many latches
+    Cut_ListForEachCut( Cut_NodeReadCutsOld(p, Node), pTemp )
+    {
+        pTemp->uSign = 0;
+        for ( i = 0; i < (int)pTemp->nLeaves; i++ )
+        {
+            pTemp->pLeaves[i] += nLat;
+            pTemp->uSign      |= Cut_NodeSign( pTemp->pLeaves[i] );
+        }
+    }
+    Cut_ListForEachCut( Cut_NodeReadCutsNew(p, Node), pTemp )
+    {
+        pTemp->uSign = 0;
+        for ( i = 0; i < (int)pTemp->nLeaves; i++ )
+        {
+            pTemp->pLeaves[i] += nLat;
+            pTemp->uSign      |= Cut_NodeSign( pTemp->pLeaves[i] );
+        }
+    }
+}
+
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -39,6 +222,13 @@
   SeeAlso     []
 
 ***********************************************************************/
+int Cut_ListCount( Cut_Cut_t * pList )
+{
+    int Counter = 0;
+    Cut_ListForEachCut( pList, pList )
+        Counter++;
+    return Counter;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c
index cc115042..ca09f22c 100644
--- a/src/opt/cut/cutTruth.c
+++ b/src/opt/cut/cutTruth.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "cutInt.h"
+#include "npn.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -80,6 +81,8 @@ int clk = clock();
         Cut_TruthCompute5( p, pCut, pCut0, pCut1 );
     else // if ( pCut->nVarsMax == 6 )
         Cut_TruthCompute6( p, pCut, pCut0, pCut1 );
+
+//    Npn_VarsTest( pCut->nVarsMax, Cut_CutReadTruth(pCut) );
 p->timeTruth += clock() - clk;
 }
 
@@ -316,6 +319,93 @@ p->timeTruth += clock() - clk;
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Expands the truth table according to the phase.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_TruthExpand( int nVars, uint8 * puTruth, unsigned uPhase, uint8 * puTruthR )
+{
+    int i, k, m, m1;
+    assert( nVars <= 8 );
+    Extra_BitClean( nVars, puTruthR );
+    for ( m = (1 << nVars) - 1; m >= 0; m-- )
+    {
+        m1 = 0;
+        for ( i = k = 0; i < nVars; i++ )
+            if ( uPhase & (1 << i) )
+            {
+                if ( m & (1 << i) )
+                    m1 |= (1 << k);
+                k++;
+            }
+        if ( Extra_BitRead( puTruth, m1 ) )
+            Extra_BitSet( puTruthR, m );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_TruthCompute1( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+    uint8 uTruth0[32], uTruth1[32];
+    unsigned * puTruthCut0, * puTruthCut1, * puTruthCut;
+    unsigned uPhase;
+int clk = clock();
+
+    assert( pCut->nLeaves >= 2 );
+    assert( pCut->nLeaves <= 8 );
+
+    if ( pCut->nVarsMax == 4 )
+    {
+        Cut_TruthCompute4( p, pCut, pCut0, pCut1 );
+        return;
+    }
+
+    puTruthCut0 = Cut_CutReadTruth(pCut0);
+    puTruthCut1 = Cut_CutReadTruth(pCut1);
+    puTruthCut  = Cut_CutReadTruth(pCut);
+
+    uPhase = Cut_TruthPhase( pCut, pCut0 );
+    Extra_TruthExpand( pCut->nVarsMax, (uint8*)puTruthCut0, uPhase, uTruth0 );
+    if ( p->fCompl0 )
+        Extra_BitNot( pCut->nVarsMax, uTruth0 );
+
+    uPhase = Cut_TruthPhase( pCut, pCut1 );
+    Extra_TruthExpand( pCut->nVarsMax, (uint8*)puTruthCut1, uPhase, uTruth1 );
+    if ( p->fCompl1 )
+        Extra_BitNot( pCut->nVarsMax, uTruth1 );
+
+    Extra_BitAnd( pCut->nVarsMax, (uint8*)uTruth0, (uint8*)uTruth1, (uint8*)puTruthCut );
+    if ( pCut->fCompl )
+        Extra_BitNot( pCut->nVarsMax, (uint8*)puTruthCut );
+
+p->timeTruth += clock() - clk;
+
+
+//Extra_PrintBinary( stdout, (unsigned*)uTruth0, 32 ); printf( "\n" );
+//Extra_PrintBinary( stdout, (unsigned*)uTruth1, 32 ); printf( "\n" );
+//Extra_PrintBinary( stdout, puTruthCut , 32 ); printf( "\n" );
+//uPhase = 0;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 6bf1fdbe..f0f7743b 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -159,13 +159,13 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
     PRT( "Update      ", p->timeUpdate );
     PRT( "TOTAL       ", p->timeTotal );
 
-/*
+
     printf( "The scores are:\n" );
     for ( i = 0; i < 222; i++ )
         if ( p->nScores[i] > 0 )
             printf( "%3d = %8d  canon = %5d\n", i, p->nScores[i], p->pMapInv[i] );
     printf( "\n" );
-*/
+
 }
 
 /**Function*************************************************************
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
index d805da72..786b7583 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -586,10 +586,6 @@ int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Out
     }
     // perform the traversal
     RetValue = 3 & Sim_NtkSimTwoPats_rec( Abc_ObjFanin0( Abc_NtkCo(pNtk,Output) ) );
-    if ( RetValue == 0 || RetValue == 3 )
-    {
-        int x = 0;
-    }
 //    assert( RetValue == 1 || RetValue == 2 ); 
     return RetValue == 1 || RetValue == 2;
 }
author	Alan Mishchenko <alanmi@berkeley.edu>	2005-10-01 08:01:00 -0700
committer	Alan Mishchenko <alanmi@berkeley.edu>	2005-10-01 08:01:00 -0700
commit	78fbd336aa584c4d285123ad18617aa9277016b4 (patch)
tree	5d65fe6b080dc85b1456320f60555ba33bab9b09 /src
parent	0af9acd0cd07dcb37c195c6a0832b82c0eca1193 (diff)
download	abc-78fbd336aa584c4d285123ad18617aa9277016b4.tar.gz abc-78fbd336aa584c4d285123ad18617aa9277016b4.tar.bz2 abc-78fbd336aa584c4d285123ad18617aa9277016b4.zip