Version abc51001

12 files changed, 735 insertions, 140 deletions

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;
 }