Version abc51002

10 files changed, 938 insertions, 557 deletions

diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index ecdfed72..9908f6a8 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -29,32 +29,40 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#define CUT_SIZE_MIN    3      // the min K of the K-feasible cut computation
+#define CUT_SIZE_MAX    8      // the max K of the K-feasible cut computation
+
+#define CUT_SHIFT       8      // the number of bits for storing latch number in the cut leaves
+#define CUT_MASK        0xFF   // the mask to get the stored latch number
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
 typedef struct Cut_ManStruct_t_         Cut_Man_t;
+typedef struct Cut_OracleStruct_t_      Cut_Oracle_t;
 typedef struct Cut_CutStruct_t_         Cut_Cut_t;
 typedef struct Cut_ParamsStruct_t_      Cut_Params_t;
 
 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
+    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                fRecord;           // record the cut computation flow
+    int                fVerbose;          // the verbosiness flag
 };
 
 struct Cut_CutStruct_t_
 {
-    unsigned           uTruth     : 16;   // truth table for 4-input cuts
-    unsigned           uPhase     :  6;   // the phase when mapping into a canonical form
+    unsigned           Num0       : 11;   // temporary number
+    unsigned           Num1       : 11;   // temporary number
     unsigned           fSimul     :  1;   // the value of cut's output at 000.. pattern
     unsigned           fCompl     :  1;   // the cut is complemented
     unsigned           nVarsMax   :  4;   // the max number of vars [4-6]
@@ -64,15 +72,13 @@ struct Cut_CutStruct_t_
     int                pLeaves[0];        // the array of leaves
 };
 
-static inline unsigned * Cut_CutReadTruth( Cut_Cut_t * p )     {  if ( p->nVarsMax == 4 )  return (unsigned *)p;  return (unsigned *)(p->pLeaves + p->nVarsMax); }
-static inline unsigned   Cut_CutReadPhase( Cut_Cut_t * p )     {  return p->uPhase;    }
 static inline int        Cut_CutReadLeaveNum( Cut_Cut_t * p )  {  return p->nLeaves;   }
 static inline int *      Cut_CutReadLeaves( Cut_Cut_t * p )    {  return p->pLeaves;   }
-
+static inline unsigned * Cut_CutReadTruth( Cut_Cut_t * p )     {  return (unsigned *)(p->pLeaves + p->nVarsMax); }
 static inline void       Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth )  { 
-    if ( p->nVarsMax == 4 )  { p->uTruth = *puTruth;  return; }
-    p->pLeaves[p->nVarsMax] = (int)puTruth[0];
-    if ( p->nVarsMax == 6 )  p->pLeaves[p->nVarsMax + 1] = (int)puTruth[1];
+    int i;
+    for ( i = (p->nVarsMax <= 5) ? 0 : ((1 << (p->nVarsMax - 5)) - 1); i >= 0; i-- )
+        p->pLeaves[p->nVarsMax + i] = (int)puTruth[i];
 }
 
 ////////////////////////////////////////////////////////////////////////
@@ -104,14 +110,21 @@ extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName
 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, 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_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, 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 );
+/*=== cutOracle.c ==========================================================*/
+extern Cut_Oracle_t *   Cut_OracleStart( Cut_Man_t * pMan );
+extern void             Cut_OracleStop( Cut_Oracle_t * p );
+extern void             Cut_OracleSetFanoutCounts( Cut_Oracle_t * p, Vec_Int_t * vFanCounts );
+extern int              Cut_OracleReadDrop( Cut_Oracle_t * p );
+extern void             Cut_OracleNodeSetTriv( Cut_Oracle_t * p, int Node );
+extern Cut_Cut_t *      Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 );
+extern void             Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutCut.c b/src/opt/cut/cutCut.c
index 95916960..2039f0c4 100644
--- a/src/opt/cut/cutCut.c
+++ b/src/opt/cut/cutCut.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "cutInt.h"
-#include "npn.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -31,7 +30,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Start the cut computation.]
+  Synopsis    [Allocates the cut.]
 
   Description []
                
@@ -58,7 +57,7 @@ Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Start the cut computation.]
+  Synopsis    [Recybles the cut.]
 
   Description []
                
@@ -67,29 +66,145 @@ Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
+void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut )
+{
+    p->nCutsDealloc++;
+    p->nCutsCur--;
+    if ( pCut->nLeaves == 1 )
+        p->nCutsTriv--;
+    Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_CutCompare( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 )
+{
+    int i;
+    if ( pCut1->nLeaves < pCut2->nLeaves )
+        return -1;
+    if ( pCut1->nLeaves > pCut2->nLeaves )
+        return 1;
+    for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+    {
+        if ( pCut1->pLeaves[i] < pCut2->pLeaves[i] )
+            return -1;
+        if ( pCut1->pLeaves[i] > pCut2->pLeaves[i] )
+            return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutDupList( Cut_Man_t * p, Cut_Cut_t * pList )
+{
+    Cut_Cut_t * pHead = NULL, ** ppTail = &pHead;
+    Cut_Cut_t * pTemp, * pCopy;
+    if ( pList == NULL )
+        return NULL;
+    Cut_ListForEachCut( pList, pTemp )
+    {
+        pCopy = (Cut_Cut_t *)Extra_MmFixedEntryFetch( p->pMmCuts );
+        memcpy( pCopy, pTemp, p->EntrySize );
+        *ppTail = pCopy;
+        ppTail = &pCopy->pNext;
+    }
+    *ppTail = NULL;
+    return pHead;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CutRecycleList( Cut_Man_t * p, Cut_Cut_t * pList )
+{
+    Cut_Cut_t * pCut, * pCut2;
+    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+        Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of cuts in the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_CutCountList( Cut_Cut_t * pList )
+{
+    int Counter = 0;
+    Cut_ListForEachCut( pList, pList )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two NULL-terminated linked lists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeLists( Cut_Cut_t * pList1, Cut_Cut_t * pList2 )
 {
+    Cut_Cut_t * pList = NULL, ** ppTail = &pList;
     Cut_Cut_t * pCut;
-    if ( p->pParams->fSeq )
-        Node <<= 8;
-    pCut = Cut_CutAlloc( p );
-    pCut->nLeaves    = 1;
-    pCut->pLeaves[0] = Node;
-    pCut->uSign      = Cut_NodeSign( Node );
-    if ( p->pParams->fTruth )
+    while ( pList1 && pList2 )
     {
-        if ( pCut->nVarsMax == 4 )
-            Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
+        if ( Cut_CutCompare(pList1, pList2) < 0 )
+        {
+            pCut = pList1;
+            pList1 = pList1->pNext;
+        }
         else
-            Extra_BitCopy( pCut->nLeaves, p->uTruths[0], (uint8*)Cut_CutReadTruth(pCut) );
+        {
+            pCut = pList2;
+            pList2 = pList2->pNext;
+        }
+        *ppTail = pCut;
+        ppTail = &pCut->pNext;
     }
-    p->nCutsTriv++;
-    return pCut;
-} 
+    *ppTail = pList1? pList1: pList2;
+    return pList;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Start the cut computation.]
+  Synopsis    [Sets the number of the cuts in the list.]
 
   Description []
                
@@ -98,15 +213,51 @@ Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut )
+void Cut_CutNumberList( Cut_Cut_t * pList )
 {
-    p->nCutsDealloc++;
-    p->nCutsCur--;
-    if ( pCut->nLeaves == 1 )
-        p->nCutsTriv--;
-    Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
+    Cut_Cut_t * pCut;
+    int i = 0;
+    Cut_ListForEachCut( pList, pCut )
+        pCut->Num0 = i++;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates the trivial cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
+{
+    Cut_Cut_t * pCut;
+    if ( p->pParams->fSeq )
+        Node <<= CUT_SHIFT;
+    pCut = Cut_CutAlloc( p );
+    pCut->nLeaves    = 1;
+    pCut->pLeaves[0] = Node;
+    pCut->uSign      = Cut_NodeSign( Node );
+    if ( p->pParams->fTruth )
+    {
+/*
+        if ( pCut->nVarsMax == 4 )
+            Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
+        else
+            Extra_BitCopy( pCut->nLeaves, p->uTruths[0], (uint8*)Cut_CutReadTruth(pCut) );
+*/
+        unsigned * pTruth = Cut_CutReadTruth(pCut);
+        int i;
+        for ( i = 0; i < p->nTruthWords; i++ )
+            pTruth[i] = 0xAAAAAAAA;
+    }
+    p->nCutsTriv++;
+    return pCut;
+} 
+
 
 /**Function*************************************************************
 
@@ -128,9 +279,9 @@ void Cut_CutPrint( Cut_Cut_t * pCut, int fSeq )
     {
         if ( fSeq )
         {
-            printf( " %d", pCut->pLeaves[i] >> 8 );
-            if ( pCut->pLeaves[i] & 0xFF )
-                printf( "(%d)", pCut->pLeaves[i] & 0xFF );
+            printf( " %d", pCut->pLeaves[i] >> CUT_SHIFT );
+            if ( pCut->pLeaves[i] & CUT_MASK )
+                printf( "(%d)", pCut->pLeaves[i] & CUT_MASK );
         }
         else
             printf( " %d", pCut->pLeaves[i] );
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index f4178ec8..28068abf 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -29,14 +29,12 @@
 #include "extra.h"
 #include "vec.h"
 #include "cut.h"
+#include "cutList.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#define CUT_SIZE_MAX 8
-#include "cutList.h"
-
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -55,6 +53,7 @@ struct Cut_ManStruct_t_
     // memory management
     Extra_MmFixed_t *  pMmCuts;
     int                EntrySize;
+    int                nTruthWords;
     // temporary variables
     Cut_Cut_t *        pReady;
     Vec_Ptr_t *        vTemp;
@@ -62,12 +61,14 @@ struct Cut_ManStruct_t_
     int                fCompl1;
     int                fSimul;
     int                nNodeCuts;
-    // precomputations
-    uint8              uTruths[8][32];
-    unsigned           uTruthVars[6][2];
-    unsigned short **  pPerms43;
-    unsigned **        pPerms53;
-    unsigned **        pPerms54;
+    Cut_Cut_t *        pStore0[2];
+    Cut_Cut_t *        pStore1[2];
+    Cut_Cut_t *        pCompareOld;
+    Cut_Cut_t *        pCompareNew;
+    // record of the cut computation
+    Vec_Int_t *        vNodeCuts;        // the number of cuts for each node
+    Vec_Int_t *        vNodeStarts;      // the number of the starting cut of each node
+    Vec_Int_t *        vCutPairs;        // the pairs of parent cuts for each cut
     // statistics
     int                nCutsCur;
     int                nCutsMulti;
@@ -108,7 +109,8 @@ struct Cut_ManStruct_t_
 ////////////////////////////////////////////////////////////////////////
 
 // computes signature of the node
-static inline unsigned Cut_NodeSign( int Node )  { return (1 << (Node % 31)); }
+static inline unsigned Cut_NodeSign( int Node )        { return (1 << (Node % 31));                        }
+static inline int      Cut_TruthWords( int nVarsMax )  { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -116,11 +118,20 @@ static inline unsigned Cut_NodeSign( int Node )  { return (1 << (Node % 31)); }
 
 /*=== cutCut.c ==========================================================*/
 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 int                 Cut_CutCompare( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 );
+extern Cut_Cut_t *         Cut_CutDupList( Cut_Man_t * p, Cut_Cut_t * pList );
+extern void                Cut_CutRecycleList( Cut_Man_t * p, Cut_Cut_t * pList );
+extern int                 Cut_CutCountList( Cut_Cut_t * pList );
+extern Cut_Cut_t *         Cut_CutMergeLists( Cut_Cut_t * pList1, Cut_Cut_t * pList2 ); 
+extern void                Cut_CutNumberList( Cut_Cut_t * pList );
+extern Cut_Cut_t *         Cut_CutCreateTriv( Cut_Man_t * p, int Node );
 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 );
+/*=== cutNode.c ==========================================================*/
+extern void                Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv ); 
+extern int                 Cut_CutListVerify( Cut_Cut_t * pList );
 /*=== cutTable.c ==========================================================*/
 extern Cut_HashTable_t *   Cut_TableStart( int Size );
 extern void                Cut_TableStop( Cut_HashTable_t * pTable );
@@ -128,7 +139,7 @@ extern int                 Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t
 extern void                Cut_TableClear( Cut_HashTable_t * pTable );
 extern int                 Cut_TableReadTime( Cut_HashTable_t * pTable );
 /*=== cutTruth.c ==========================================================*/
-extern void                Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+extern void                Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutList.h b/src/opt/cut/cutList.h
index fd707e6e..ab540908 100644
--- a/src/opt/cut/cutList.h
+++ b/src/opt/cut/cutList.h
@@ -89,7 +89,42 @@ static inline void Cut_ListAdd( Cut_List_t * p, Cut_Cut_t * pCut )
 
 /**Function*************************************************************
 
-  Synopsis    [Adds one cut to the cut list.]
+  Synopsis    [Adds one cut to the cut list while preserving order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cut_ListAdd2( Cut_List_t * p, Cut_Cut_t * pCut )
+{
+    extern int Cut_CutCompare( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 );
+    Cut_Cut_t * pTemp, ** ppSpot;
+    assert( pCut->nLeaves > 0 && pCut->nLeaves <= CUT_SIZE_MAX );
+    if ( p->pHead[pCut->nLeaves] != NULL )
+    {
+        ppSpot = &p->pHead[pCut->nLeaves];
+        for ( pTemp = p->pHead[pCut->nLeaves]; pTemp; pTemp = pTemp->pNext )
+        {
+            if ( Cut_CutCompare(pCut, pTemp) < 0 )
+            {
+                *ppSpot = pCut;
+                pCut->pNext = pTemp;
+                return;
+            }
+            else
+                ppSpot = &pTemp->pNext;
+        }
+    }
+    *p->ppTail[pCut->nLeaves] = pCut;
+    p->ppTail[pCut->nLeaves] = &pCut->pNext;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive the super list from the linked list of cuts.]
 
   Description []
                
@@ -153,7 +188,7 @@ static inline Cut_Cut_t * Cut_ListFinish( Cut_List_t * p )
 {
     Cut_Cut_t * pHead = NULL, ** ppTail = &pHead;
     int i;
-    for ( i = 1; i < CUT_SIZE_MAX; i++ )
+    for ( i = 1; i <= CUT_SIZE_MAX; i++ )
     {
         if ( p->pHead[i] == NULL )
             continue;
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index c9dccb6a..30517d54 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -45,7 +45,7 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
 {
     Cut_Man_t * p;
     int clk = clock();
-    assert( pParams->nVarsMax >= 4 && pParams->nVarsMax <= CUT_SIZE_MAX );
+    assert( pParams->nVarsMax >= 3 && pParams->nVarsMax <= CUT_SIZE_MAX );
     p = ALLOC( Cut_Man_t, 1 );
     memset( p, 0, sizeof(Cut_Man_t) );
     // set and correct parameters
@@ -65,19 +65,28 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
     assert( !pParams->fTruth || pParams->nVarsMax <= 5 );
     // entry size
     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);
+    if ( pParams->fTruth )
+    {
+        if ( pParams->nVarsMax > 8 )
+        {
+            pParams->fTruth = 0;
+            printf( "Skipping computation of truth table for more than 8 inputs.\n" );
+        }
+        else
+        {
+            p->nTruthWords = Cut_TruthWords( pParams->nVarsMax );
+            p->EntrySize += p->nTruthWords * sizeof(unsigned);
+        }
+    }
+    // enable cut computation recording
+    if ( pParams->fRecord )
+    {
+        p->vNodeCuts   = Vec_IntStart( pParams->nIdsMax );
+        p->vNodeStarts = Vec_IntStart( pParams->nIdsMax );
+        p->vCutPairs   = Vec_IntAlloc( 0 );
+    }
     // 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
-    p->uTruthVars[3][1] = p->uTruthVars[3][0] = 0xFF00FF00;    // 1111 1111 0000 0000 1111 1111 0000 0000
-    p->uTruthVars[4][1] = p->uTruthVars[4][0] = 0xFFFF0000;    // 1111 1111 1111 1111 0000 0000 0000 0000
-    p->uTruthVars[5][0] = 0x00000000;
-    p->uTruthVars[5][1] = 0xFFFFFFFF;
     p->vTemp = Vec_PtrAlloc( 100 );
     return p;
 }
@@ -102,14 +111,16 @@ void Cut_ManStop( Cut_Man_t * p )
         {
             int k = 0;
         }
-    if ( p->vCutsNew )   Vec_PtrFree( p->vCutsNew );
-    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 );
-    if ( p->pPerms54 )   free( p->pPerms54 );
-    if ( p->vTemp )      Vec_PtrFree( p->vTemp );
+    if ( p->vCutsNew )    Vec_PtrFree( p->vCutsNew );
+    if ( p->vCutsOld )    Vec_PtrFree( p->vCutsOld );
+    if ( p->vCutsTemp )   Vec_PtrFree( p->vCutsTemp );
+    if ( p->vFanCounts )  Vec_IntFree( p->vFanCounts );
+    if ( p->vTemp )       Vec_PtrFree( p->vTemp );
+
+    if ( p->vNodeCuts )   Vec_IntFree( p->vNodeCuts );
+    if ( p->vNodeStarts ) Vec_IntFree( p->vNodeStarts );
+    if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
+
     Extra_MmFixedStop( p->pMmCuts, 0 );
     free( p );
 }
@@ -146,8 +157,9 @@ 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 );
+//    printf( "Nodes = %d. Multi = %d.  Cuts = %d. Multi = %d.\n", 
+//        p->nNodes, p->nNodesMulti, p->nCutsCur-p->nCutsTriv, p->nCutsMulti );
+//    printf( "Count0 = %d. Count1 = %d. Count2 = %d.\n\n", p->Count0, p->Count1, p->Count2 );
 }
 
     
diff --git a/src/opt/cut/cutMerge.c b/src/opt/cut/cutMerge.c
index f9c059bf..a38d1cef 100644
--- a/src/opt/cut/cutMerge.c
+++ b/src/opt/cut/cutMerge.c
@@ -526,7 +526,7 @@ Cut_Cut_t * Cut_CutMergeTwo5( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut
                     return NULL;
             }
             pRes = Cut_CutAlloc( p );
-            pRes->uTruth = (uSign1 << 8);
+            pRes->Num1 = uSign1;
         }
         for ( i = 0; i < (int)pCut0->nLeaves; i++ )
             pRes->pLeaves[i] = pCut0->pLeaves[i];
@@ -645,7 +645,8 @@ Cut_Cut_t * Cut_CutMergeTwo5( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut
     }
     assert( Count == nNodes );
     pRes->nLeaves = nNodes;
-    pRes->uTruth = (uSign1 << 8) | uSign0;
+    pRes->Num1 = uSign1;
+    pRes->Num0 = uSign0;
     return pRes;
 }
 
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 0d0ac04c..672463b4 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -189,9 +189,6 @@ static inline int Cut_CutFilterOld( Cut_Man_t * p, Cut_Cut_t * pList, Cut_Cut_t
 {
     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 )
@@ -250,7 +247,7 @@ static inline int Cut_CutFilterOld( Cut_Man_t * p, Cut_Cut_t * pList, Cut_Cut_t
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
+static inline int Cut_CutProcessTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
 {
     Cut_Cut_t * pCut;
     // merge the cuts
@@ -260,13 +257,11 @@ 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;
-//    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;
+    if ( p->pParams->fRecord )
+        pCut->Num0 = pCut0->Num0, pCut->Num1 = pCut1->Num0;
     // check containment
     if ( p->pParams->fFilter )
     {
@@ -274,15 +269,15 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0,
             return 0;
         if ( p->pParams->fSeq )
         {
-            if ( Cut_CutFilterOld(p, Cut_NodeReadCutsOld(p, Root), pCut) )
+            if ( p->pCompareOld && Cut_CutFilterOld(p, p->pCompareOld, pCut) )
                 return 0;
-            if ( Cut_CutFilterOld(p, Cut_NodeReadCutsNew(p, Root), pCut) )
+            if ( p->pCompareNew && Cut_CutFilterOld(p, p->pCompareNew, pCut) )
                 return 0;
         }
     }
     // compute the truth table
     if ( p->pParams->fTruth )
-        Cut_TruthCompute( p, pCut, pCut0, pCut1 );
+        Cut_TruthCompute( pCut, pCut0, pCut1, p->fCompl0, p->fCompl1 );
     // add to the list
     Cut_ListAdd( pSuperList, pCut );
     // return status (0 if okay; 1 if exceeded the limit)
@@ -300,16 +295,36 @@ 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, int fNew0, int fNew1, int fTriv )
+Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv )
 {
-    Cut_Cut_t * pList;
-    int clk = clock();
+    Cut_List_t Super, * pSuper = &Super;
+    Cut_Cut_t * pList, * pCut;
+    int clk;
     // start the number of cuts at the node
     p->nNodes++;
     p->nNodeCuts = 0;
+    // prepare information for recording
+    if ( p->pParams->fRecord )
+    {
+        Cut_CutNumberList( Cut_NodeReadCutsNew(p, Node0) );
+        Cut_CutNumberList( Cut_NodeReadCutsNew(p, Node1) );
+    }
     // compute the cuts
-    pList = Cut_NodeDoComputeCuts( p, Node, Node0, Node1, fCompl0, fCompl1, fNew0, fNew1, fTriv );
+clk = clock();
+    Cut_ListStart( pSuper );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, Cut_NodeReadCutsNew(p, Node0), Cut_NodeReadCutsNew(p, Node1), fTriv );
+    pList = Cut_ListFinish( pSuper );
 p->timeMerge += clock() - clk;
+    // verify the result of cut computation
+//    Cut_CutListVerify( pList );
+    // performing the recording
+    if ( p->pParams->fRecord )
+    {
+        Vec_IntWriteEntry( p->vNodeStarts, Node, Vec_IntSize(p->vCutPairs) );
+        Cut_ListForEachCut( pList, pCut )
+            Vec_IntPush( p->vCutPairs, ((pCut->Num1 << 16) | pCut->Num0) );
+        Vec_IntWriteEntry( p->vNodeCuts, Node, Vec_IntSize(p->vCutPairs) - Vec_IntEntry(p->vNodeStarts, Node) );
+    }
     // check if the node is over the list
     if ( p->nNodeCuts == p->pParams->nKeepMax )
         p->nCutsLimit++;
@@ -336,20 +351,15 @@ p->timeMerge += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-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 )
+void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fCompl0, int fCompl1, Cut_Cut_t * pList0, Cut_Cut_t * pList1, int fTriv )
 {
-    Cut_List_t SuperList;
-    Cut_Cut_t * pList0, * pList1, * pStop0, * pStop1, * pTemp0, * pTemp1;
+    Cut_Cut_t * pStop0, * pStop1, * pTemp0, * pTemp1;
     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;
+        return;
     // start the new list
     nCutsOld = p->nCutsCur;
-    Cut_ListStart( &SuperList );
     Limit = p->pParams->nVarsMax;
     // get the simultation bit of the node
     p->fSimul = (fCompl0 ^ pList0->fSimul) & (fCompl1 ^ pList1->fSimul);
@@ -367,23 +377,23 @@ Cut_Cut_t * Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1
     if ( fTriv ) 
     {
         pTemp0 = Cut_CutCreateTriv( p, Node );
-        Cut_ListAdd( &SuperList, pTemp0 );
+        Cut_ListAdd( pSuper, 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 ) )
-            return Cut_ListFinish( &SuperList );
+        if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
+            return;
     // small by large
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCut( pStop1, pTemp1 )
     {
         if ( (pTemp0->uSign & pTemp1->uSign) != pTemp0->uSign )
             continue;
-        if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
-            return Cut_ListFinish( &SuperList );
+        if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
+            return;
     }
     // small by large
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
@@ -391,8 +401,8 @@ Cut_Cut_t * Cut_NodeDoComputeCuts( 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 ) )
-            return Cut_ListFinish( &SuperList );
+        if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
+            return;
     }
     // large by large
     Cut_ListForEachCut( pStop0, pTemp0 )
@@ -406,15 +416,14 @@ Cut_Cut_t * Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1
                 break;
         if ( i < Limit )
             continue;
-        if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
-            return Cut_ListFinish( &SuperList );
+        if ( Cut_CutProcessTwo( p, pTemp0, pTemp1, pSuper ) )
+            return;
     } 
     if ( fTriv ) 
     {
         p->nCutsMulti += p->nCutsCur - nCutsOld;         
         p->nNodesMulti++;
     }
-    return Cut_ListFinish( &SuperList );
 }
 
 /**Function*************************************************************
@@ -430,15 +439,13 @@ Cut_Cut_t * Cut_NodeDoComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1
 ***********************************************************************/
 Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
 {
-    Cut_List_t SuperList;
+    Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop;
     int i, k, Node, Root, Limit = p->pParams->nVarsMax;
     int clk = clock();
 
-    assert( p->pParams->nVarsMax <= 6 );
-
     // start the new list
-    Cut_ListStart( &SuperList );
+    Cut_ListStart( pSuper );
 
     // remember the root node to save the resulting cuts
     Root = Vec_IntEntry( vNodes, 0 );
@@ -457,7 +464,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
         pList->pNext = NULL;
         // save or recycle the elementary cut
         if ( i == 0 )
-            Cut_ListAdd( &SuperList, pList ), pTop = pList;
+            Cut_ListAdd( pSuper, pList ), pTop = pList;
         else
             Cut_CutRecycle( p, pList );
         // save all the cuts that are smaller than the limit
@@ -469,14 +476,14 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
                 break;
             }
             // check containment
-            if ( p->pParams->fFilter && Cut_CutFilterOne( p, &SuperList, pCut ) )
+            if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) )
                 continue;
             // set the complemented bit by comparing the first cut with the current cut
             pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
             pListStart = pCut->pNext;
             pCut->pNext = NULL;
             // add to the list
-            Cut_ListAdd( &SuperList, pCut );
+            Cut_ListAdd( pSuper, pCut );
             if ( ++p->nNodeCuts == p->pParams->nKeepMax )
             {
                 // recycle the rest of the cuts of this node
@@ -499,14 +506,14 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
         Cut_ListForEachCutSafe( pList, pCut, pCut2 )
         {
             // check containment
-            if ( p->pParams->fFilter && Cut_CutFilterOne( p, &SuperList, pCut ) )
+            if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) )
                 continue;
             // set the complemented bit
             pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
             pListStart = pCut->pNext;
             pCut->pNext = NULL;
             // add to the list
-            Cut_ListAdd( &SuperList, pCut );
+            Cut_ListAdd( pSuper, pCut );
             if ( ++p->nNodeCuts == p->pParams->nKeepMax )
             {
                 // recycle the rest of the cuts
@@ -523,7 +530,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
 finish :
     // set the cuts at the node
     assert( Cut_NodeReadCutsNew(p, Root) == NULL );
-    pList = Cut_ListFinish( &SuperList );
+    pList = Cut_ListFinish( pSuper );
     Cut_NodeWriteCutsNew( p, Root, pList );
 p->timeUnion += clock() - clk;
     // filter the cuts
@@ -536,6 +543,38 @@ p->timeUnion += clock() - clk;
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Verifies that the list contains only non-dominated cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_CutListVerify( Cut_Cut_t * pList )
+{ 
+    Cut_Cut_t * pCut, * pDom;
+    Cut_ListForEachCut( pList, pCut )
+    {
+        Cut_ListForEachCutStop( pList, pDom, pCut )
+        {
+            if ( Cut_CutCheckDominance( pDom, pCut ) )
+            {
+                int x = 0;
+                printf( "******************* These are contained cuts:\n" );
+                Cut_CutPrint( pDom, 1 );
+                Cut_CutPrint( pDom, 1 );
+                
+                return 0;
+            }
+        }
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/cut/cutOracle.c b/src/opt/cut/cutOracle.c
new file mode 100644
index 00000000..a254fd96
--- /dev/null
+++ b/src/opt/cut/cutOracle.c
@@ -0,0 +1,428 @@
+/**CFile****************************************************************
+
+  FileName    [cutOracle.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Procedures to compute cuts for a node using the oracle.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutOracle.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Cut_OracleStruct_t_
+{
+    // cut comptupatation parameters
+    Cut_Params_t *     pParams;
+    Vec_Int_t *        vFanCounts;
+    int                fSimul;
+    // storage for cuts
+    Vec_Ptr_t *        vCutsNew;
+    Vec_Ptr_t *        vCuts0;
+    Vec_Ptr_t *        vCuts1;
+    // oracle info 
+    Vec_Int_t *        vNodeCuts;
+    Vec_Int_t *        vNodeStarts;
+    Vec_Int_t *        vCutPairs;
+    // memory management
+    Extra_MmFixed_t *  pMmCuts;
+    int                EntrySize;
+    int                nTruthWords;
+    // stats
+    int                timeTotal;
+    int                nCuts;
+    int                nCutsTriv;
+};
+
+static Cut_Cut_t * Cut_CutStart( Cut_Oracle_t * p );
+static Cut_Cut_t * Cut_CutTriv( Cut_Oracle_t * p, int Node );
+static Cut_Cut_t * Cut_CutMerge( Cut_Oracle_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut oracle.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Oracle_t * Cut_OracleStart( Cut_Man_t * pMan )
+{
+    Cut_Oracle_t * p;
+    int clk = clock();
+
+    assert( pMan->pParams->nVarsMax >= 3 && pMan->pParams->nVarsMax <= CUT_SIZE_MAX );
+    assert( pMan->pParams->fRecord );
+
+    p = ALLOC( Cut_Oracle_t, 1 );
+    memset( p, 0, sizeof(Cut_Oracle_t) );
+
+    // set and correct parameters
+    p->pParams     = pMan->pParams;
+
+    // transfer the recording info
+    p->vNodeCuts   = pMan->vNodeCuts;    pMan->vNodeCuts   = NULL;
+    p->vNodeStarts = pMan->vNodeStarts;  pMan->vNodeStarts = NULL;
+    p->vCutPairs   = pMan->vCutPairs;    pMan->vCutPairs   = NULL;
+
+    // prepare storage for cuts
+    p->vCutsNew = Vec_PtrAlloc( p->pParams->nIdsMax );
+    Vec_PtrFill( p->vCutsNew, p->pParams->nIdsMax, NULL );
+    p->vCuts0 = Vec_PtrAlloc( 100 );
+    p->vCuts1 = Vec_PtrAlloc( 100 );
+
+    // entry size
+    p->EntrySize = sizeof(Cut_Cut_t) + p->pParams->nVarsMax * sizeof(int);
+    if ( p->pParams->fTruth )
+    {
+        if ( p->pParams->nVarsMax > 8 )
+        {
+            p->pParams->fTruth = 0;
+            printf( "Skipping computation of truth table for more than 8 inputs.\n" );
+        }
+        else
+        {
+            p->nTruthWords = Cut_TruthWords( p->pParams->nVarsMax );
+            p->EntrySize += p->nTruthWords * sizeof(unsigned);
+        }
+    }
+    // memory for cuts
+    p->pMmCuts = Extra_MmFixedStart( p->EntrySize );
+    return p;
+}
+/**Function*************************************************************
+
+  Synopsis    [Stop the cut oracle.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_OracleStop( Cut_Oracle_t * p )
+{
+    Cut_Cut_t * pCut;
+    int i;
+
+//    if ( p->pParams->fVerbose )
+    {
+        printf( "Cut computation statistics with oracle:\n" );
+        printf( "Current cuts      = %8d. (Trivial = %d.)\n", p->nCuts-p->nCutsTriv, p->nCutsTriv );
+        PRT( "Total time ", p->timeTotal );
+    }
+
+    Vec_PtrForEachEntry( p->vCutsNew, pCut, i )
+        if ( pCut != NULL )
+        {
+            int k = 0;
+        }
+    if ( p->vCuts0 )      Vec_PtrFree( p->vCuts0 );
+    if ( p->vCuts1 )      Vec_PtrFree( p->vCuts1 );
+    if ( p->vCutsNew )    Vec_PtrFree( p->vCutsNew );
+    if ( p->vFanCounts )  Vec_IntFree( p->vFanCounts );
+
+    if ( p->vNodeCuts )   Vec_IntFree( p->vNodeCuts );
+    if ( p->vNodeStarts ) Vec_IntFree( p->vNodeStarts );
+    if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
+
+    Extra_MmFixedStop( p->pMmCuts, 0 );
+    free( p ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_OracleSetFanoutCounts( Cut_Oracle_t * p, Vec_Int_t * vFanCounts )
+{
+    p->vFanCounts = vFanCounts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_OracleReadDrop( Cut_Oracle_t * p )
+{
+    return p->pParams->fDrop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the trivial cut for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_OracleNodeSetTriv( Cut_Oracle_t * p, int Node )
+{
+    assert( Vec_PtrEntry( p->vCutsNew, Node ) == NULL );
+    Vec_PtrWriteEntry( p->vCutsNew, Node, Cut_CutTriv(p, Node) );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutStart( Cut_Oracle_t * p )
+{
+    Cut_Cut_t * pCut;
+    // cut allocation
+    pCut = (Cut_Cut_t *)Extra_MmFixedEntryFetch( p->pMmCuts );
+    memset( pCut, 0, sizeof(Cut_Cut_t) );
+    pCut->nVarsMax   = p->pParams->nVarsMax;
+    pCut->fSimul     = p->fSimul;
+    p->nCuts++;
+    return pCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the trivial cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutTriv( Cut_Oracle_t * p, int Node )
+{
+    Cut_Cut_t * pCut;
+    pCut = Cut_CutStart( p );
+    pCut->nLeaves    = 1;
+    pCut->pLeaves[0] = Node;
+    if ( p->pParams->fTruth )
+    {
+        unsigned * pTruth = Cut_CutReadTruth(pCut);
+        int i;
+        for ( i = 0; i < p->nTruthWords; i++ )
+            pTruth[i] = 0xAAAAAAAA;
+    }
+    p->nCutsTriv++;
+    return pCut;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMerge( Cut_Oracle_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+    Cut_Cut_t * pCut;
+    int Limit, i, k, c;
+    // create the leaves of the new cut
+    pCut = Cut_CutStart( p );
+    Limit = p->pParams->nVarsMax;
+    for ( i = k = c = 0; c < Limit; c++ )
+    {
+        if ( k == (int)pCut1->nLeaves )
+        {
+            if ( i == (int)pCut0->nLeaves )
+            {
+                pCut->nLeaves = c;
+                return pCut;
+            }
+            pCut->pLeaves[c] = pCut0->pLeaves[i++];
+            continue;
+        }
+        if ( i == (int)pCut0->nLeaves )
+        {
+            if ( k == (int)pCut1->nLeaves )
+            {
+                pCut->nLeaves = c;
+                return pCut;
+            }
+            pCut->pLeaves[c] = pCut1->pLeaves[k++];
+            continue;
+        }
+        if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] )
+        {
+            pCut->pLeaves[c] = pCut0->pLeaves[i++];
+            continue;
+        }
+        if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] )
+        {
+            pCut->pLeaves[c] = pCut1->pLeaves[k++];
+            continue;
+        }
+        pCut->pLeaves[c] = pCut0->pLeaves[i++]; 
+        k++;
+    }
+    assert( i == (int)pCut0->nLeaves && k == (int)pCut1->nLeaves );
+    pCut->nLeaves = c;
+    return pCut;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstruct the cuts of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 )
+{
+    Cut_Cut_t * pList = NULL, ** ppTail = &pList;
+    Cut_Cut_t * pCut, * pCut0, * pCut1, * pList0, * pList1;
+    int iCutStart, nCuts, i, Entry;
+    int clk = clock();
+
+    // get the cuts of the children
+    pList0 = Vec_PtrEntry( p->vCutsNew, Node0 );
+    pList1 = Vec_PtrEntry( p->vCutsNew, Node1 );
+    assert( pList0 && pList1 );
+
+    // get the complemented attribute of the cut
+    p->fSimul = (fCompl0 ^ pList0->fSimul) & (fCompl1 ^ pList1->fSimul);
+
+    // collect the cuts
+    Vec_PtrClear( p->vCuts0 );
+    Cut_ListForEachCut( pList0, pCut )
+        Vec_PtrPush( p->vCuts0, pCut );
+    Vec_PtrClear( p->vCuts1 );
+    Cut_ListForEachCut( pList1, pCut )
+        Vec_PtrPush( p->vCuts1, pCut );
+
+    // get the first and last cuts of this node
+    nCuts = Vec_IntEntry(p->vNodeCuts, Node);
+    iCutStart = Vec_IntEntry(p->vNodeStarts, Node);
+
+    // create trivial cut
+    assert( Vec_IntEntry(p->vCutPairs, iCutStart) == 0 );
+    pCut = Cut_CutTriv( p, Node );
+    *ppTail = pCut;
+    ppTail = &pCut->pNext;
+    // create other cuts
+    for ( i = 1; i < nCuts; i++ )
+    {
+        Entry = Vec_IntEntry( p->vCutPairs, iCutStart + i );
+        pCut0 = Vec_PtrEntry( p->vCuts0, Entry & 0xFFFF );
+        pCut1 = Vec_PtrEntry( p->vCuts1, Entry >> 16 );
+        pCut  = Cut_CutMerge( p, pCut0, pCut1 );
+        *ppTail = pCut;
+        ppTail = &pCut->pNext;
+        // compute the truth table
+        if ( p->pParams->fTruth )
+            Cut_TruthCompute( pCut, pCut0, pCut1, fCompl0, fCompl1 );
+    }
+    *ppTail = NULL;
+
+    // write the new cut
+    assert( Vec_PtrEntry( p->vCutsNew, Node ) == NULL );
+    Vec_PtrWriteEntry( p->vCutsNew, Node, pList );
+p->timeTotal += clock() - clk;
+    return pList;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the cuts at the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_OracleFreeCuts( Cut_Oracle_t * p, int Node )
+{
+    Cut_Cut_t * pList, * pCut, * pCut2;
+    pList = Vec_PtrEntry( p->vCutsNew, Node );
+    if ( pList == NULL )
+        return;
+    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+        Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
+    Vec_PtrWriteEntry( p->vCutsNew, Node, pList );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Consider dropping cuts if they are useless by now.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node )
+{
+    int nFanouts;
+    assert( p->vFanCounts );
+    nFanouts = Vec_IntEntry( p->vFanCounts, Node );
+    assert( nFanouts > 0 );
+    if ( --nFanouts == 0 )
+        Cut_OracleFreeCuts( p, Node );
+    Vec_IntWriteEntry( p->vFanCounts, Node, nFanouts );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutSeq.c b/src/opt/cut/cutSeq.c
index a1887608..001d3e01 100644
--- a/src/opt/cut/cutSeq.c
+++ b/src/opt/cut/cutSeq.c
@@ -24,16 +24,13 @@
 ///                        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.]
+  Synopsis    [Shifts all cut leaves of the node by the given number of latches.]
 
   Description []
                
@@ -42,44 +39,99 @@ static int  Cut_ListCount( Cut_Cut_t * pList );
   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 )
+static inline void Cut_NodeShiftCutLeaves( Cut_Cut_t * pList, int nLat )
 {
-    Cut_List_t List1, List2, List3;
-    Cut_Cut_t * pList1, * pList2, * pList3, * pListNew;
-    int clk = clock();
+    Cut_Cut_t * pTemp;
+    int i;
+    // shift the cuts by as many latches
+    Cut_ListForEachCut( pList, pTemp )
+    {
+        pTemp->uSign = 0;
+        for ( i = 0; i < (int)pTemp->nLeaves; i++ )
+        {
+            pTemp->pLeaves[i] += nLat;
+            pTemp->uSign      |= Cut_NodeSign( pTemp->pLeaves[i] );
+        }
+    }
+}
+
+/**Function*************************************************************
 
-//    assert( Node != Node0 );
-//    assert( Node != Node1 );
+  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 Super, * pSuper = &Super;
+    Cut_Cut_t * pListNew;
+    int clk;
+    
     // get the number of cuts at the node
-    p->nNodeCuts = Cut_ListCount( Cut_NodeReadCutsOld(p, Node) );
+    p->nNodeCuts = Cut_CutCountList( 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 );
+    // store the fanin lists
+    p->pStore0[0] = Cut_NodeReadCutsOld( p, Node0 );
+    p->pStore0[1] = Cut_NodeReadCutsNew( p, Node0 );
+    p->pStore1[0] = Cut_NodeReadCutsOld( p, Node1 );
+    p->pStore1[1] = Cut_NodeReadCutsNew( p, Node1 );
+
+    // duplicate the cut lists if fanin nodes are non-standard
+    if ( Node == Node0 || Node == Node1 || Node0 == Node1 )
+    {
+        p->pStore0[0] = Cut_CutDupList( p, p->pStore0[0] );
+        p->pStore0[1] = Cut_CutDupList( p, p->pStore0[1] );
+        p->pStore1[0] = Cut_CutDupList( p, p->pStore1[0] );
+        p->pStore1[1] = Cut_CutDupList( p, p->pStore1[1] );
+    }
+
+    // shift the cuts by as many latches and recompute signatures
+    if ( nLat0 ) Cut_NodeShiftCutLeaves( p->pStore0[0], nLat0 );
+    if ( nLat0 ) Cut_NodeShiftCutLeaves( p->pStore0[1], nLat0 );
+    if ( nLat1 ) Cut_NodeShiftCutLeaves( p->pStore1[0], nLat1 );
+    if ( nLat1 ) Cut_NodeShiftCutLeaves( p->pStore1[1], nLat1 );
+
+    // store the original lists for comparison
+    p->pCompareOld = Cut_NodeReadCutsOld( p, Node );
+    p->pCompareNew = Cut_NodeReadCutsNew( p, Node );
+
+    // merge the old and the new
+clk = clock();
+    Cut_ListStart( pSuper );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[0], p->pStore1[1], 0 );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[0], 0 );
+    Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[1], fTriv );
+    pListNew = Cut_ListFinish( pSuper );
 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 );
+    // shift the cuts by as many latches and recompute signatures
+    if ( Node == Node0 || Node == Node1 || Node0 == Node1 )
+    {
+        Cut_CutRecycleList( p, p->pStore0[0] );
+        Cut_CutRecycleList( p, p->pStore0[1] );
+        Cut_CutRecycleList( p, p->pStore1[0] );
+        Cut_CutRecycleList( p, p->pStore1[1] );
+    }
+    else
+    {
+        if ( nLat0 ) Cut_NodeShiftCutLeaves( p->pStore0[0], -nLat0 );
+        if ( nLat0 ) Cut_NodeShiftCutLeaves( p->pStore0[1], -nLat0 );
+        if ( nLat1 ) Cut_NodeShiftCutLeaves( p->pStore1[0], -nLat1 );
+        if ( nLat1 ) Cut_NodeShiftCutLeaves( p->pStore1[1], -nLat1 );
+    }
 
     // set the lists at the node
-    pListNew = Cut_ListFinish( &List1 );
     if ( CutSetNum >= 0 )
     {
         assert( Cut_NodeReadCutsTemp(p, CutSetNum) == NULL );
@@ -91,17 +143,14 @@ p->timeMerge += clock() - clk;
         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 );
-
+    // mark the node if we exceeded the number of cuts
     if ( p->nNodeCuts >= p->pParams->nKeepMax )
         p->nCutsLimit++;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Merges the new cuts with the old cuts.]
 
   Description []
                
@@ -112,8 +161,7 @@ p->timeMerge += clock() - clk;
 ***********************************************************************/
 void Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node )
 {
-    Cut_List_t Old, New;
-    Cut_Cut_t * pListOld, * pListNew;
+    Cut_Cut_t * pListOld, * pListNew, * pList;
     // get the new cuts
     pListNew = Cut_NodeReadCutsNew( p, Node );
     if ( pListNew == NULL )
@@ -127,19 +175,16 @@ void Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node )
         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 );
+    pList = Cut_CutMergeLists( pListOld, pListNew );
+    Cut_NodeWriteCutsOld( p, Node, pList );
 }
 
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if something was transferred.]
+  Synopsis    [Transfers the temporary cuts to be the new cuts.]
 
-  Description []
+  Description [Returns 1 if something was transferred.]
                
   SideEffects []
 
@@ -148,16 +193,16 @@ void Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node )
 ***********************************************************************/
 int Cut_NodeTempTransferToNew( Cut_Man_t * p, int Node, int CutSetNum )
 {
-    Cut_Cut_t * pCut;
-    pCut = Cut_NodeReadCutsTemp( p, CutSetNum );
+    Cut_Cut_t * pList;
+    pList = Cut_NodeReadCutsTemp( p, CutSetNum );
     Cut_NodeWriteCutsTemp( p, CutSetNum, NULL );
-    Cut_NodeWriteCutsNew( p, Node, pCut );
-    return pCut != NULL;
+    Cut_NodeWriteCutsNew( p, Node, pList );
+    return pList != NULL;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if something was transferred.]
+  Synopsis    [Transfers the old cuts to be the new cuts.]
 
   Description []
                
@@ -168,66 +213,11 @@ int Cut_NodeTempTransferToNew( Cut_Man_t * p, int Node, int CutSetNum )
 ***********************************************************************/
 void Cut_NodeOldTransferToNew( Cut_Man_t * p, int Node )
 {
-    Cut_Cut_t * pCut;
-    pCut = Cut_NodeReadCutsOld( p, Node );
+    Cut_Cut_t * pList;
+    pList = 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 []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_ListCount( Cut_Cut_t * pList )
-{
-    int Counter = 0;
-    Cut_ListForEachCut( pList, pList )
-        Counter++;
-    return Counter;
+    Cut_NodeWriteCutsNew( p, Node, pList );
+//    Cut_CutListVerify( pList );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c
index ca09f22c..344884f0 100644
--- a/src/opt/cut/cutTruth.c
+++ b/src/opt/cut/cutTruth.c
@@ -19,16 +19,11 @@
 ***********************************************************************/
 
 #include "cutInt.h"
-#include "npn.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Cut_TruthCompute4( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
-static void Cut_TruthCompute5( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
-static void Cut_TruthCompute6( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -72,340 +67,46 @@ static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-int clk = clock();
-    if ( pCut->nVarsMax == 4 )
-        Cut_TruthCompute4( p, pCut, pCut0, pCut1 );
-    else if ( pCut->nVarsMax == 5 )
-        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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs truth table computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TruthCompute4( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-    unsigned * puTruthCut0, * puTruthCut1;
-    unsigned uTruth0, uTruth1, uPhase;
-
-    puTruthCut0 = Cut_CutReadTruth(pCut0);
-    puTruthCut1 = Cut_CutReadTruth(pCut1);
-
-    uPhase  = Cut_TruthPhase( pCut, pCut0 );
-    uTruth0 = Extra_TruthPerm4One( *puTruthCut0, uPhase );
-    uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
-
-    uPhase  = Cut_TruthPhase( pCut, pCut1 );
-    uTruth1 = Extra_TruthPerm4One( *puTruthCut1, uPhase );
-    uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
-
-    uTruth1 = uTruth0 & uTruth1;
-    if ( pCut->fCompl )
-        uTruth1 = ~uTruth1;
-    if ( pCut->nVarsMax == 4 )
-        uTruth1 &= 0xFFFF; 
-    Cut_CutWriteTruth( pCut, &uTruth1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs truth table computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TruthCompute5( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-    unsigned * puTruthCut0, * puTruthCut1;
-    unsigned uTruth0, uTruth1, uPhase;
-
-    puTruthCut0 = Cut_CutReadTruth(pCut0);
-    puTruthCut1 = Cut_CutReadTruth(pCut1);
-
-    uPhase  = Cut_TruthPhase( pCut, pCut0 );
-    uTruth0 = Extra_TruthPerm5One( *puTruthCut0, uPhase );
-    uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
-
-    uPhase  = Cut_TruthPhase( pCut, pCut1 );
-    uTruth1 = Extra_TruthPerm5One( *puTruthCut1, uPhase );
-    uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
-
-    uTruth1 = uTruth0 & uTruth1;
-    if ( pCut->fCompl )
-        uTruth1 = ~uTruth1;
-    Cut_CutWriteTruth( pCut, &uTruth1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs truth table computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TruthCompute6( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 )
 {
-    unsigned * puTruthCut0, * puTruthCut1;
-    unsigned uTruth0[2], uTruth1[2], uPhase;
-
-    puTruthCut0 = Cut_CutReadTruth(pCut0);
-    puTruthCut1 = Cut_CutReadTruth(pCut1);
+    static unsigned uTruth0[8], uTruth1[8];
+    int nTruthWords = Cut_TruthWords( pCut->nVarsMax );
+    unsigned * pTruthRes;
+    int i, uPhase;
 
+    // permute the first table
     uPhase = Cut_TruthPhase( pCut, pCut0 );
-    Extra_TruthPerm6One( puTruthCut0, uPhase, uTruth0 );
-    uTruth0[0] = p->fCompl0? ~uTruth0[0]: uTruth0[0];
-    uTruth0[1] = p->fCompl0? ~uTruth0[1]: uTruth0[1];
-
-    uPhase = Cut_TruthPhase( pCut, pCut1 );
-    Extra_TruthPerm6One( puTruthCut1, uPhase, uTruth1 );
-    uTruth1[0] = p->fCompl1? ~uTruth1[0]: uTruth1[0];
-    uTruth1[1] = p->fCompl1? ~uTruth1[1]: uTruth1[1];
-
-    uTruth1[0] = uTruth0[0] & uTruth1[0];
-    uTruth1[1] = uTruth0[1] & uTruth1[1];
-    if ( pCut->fCompl )
-    {
-        uTruth1[0] = ~uTruth0[0];
-        uTruth1[1] = ~uTruth0[1];
-    }
-    Cut_CutWriteTruth( pCut, uTruth1 );
-}
-
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Performs truth table computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TruthComputeOld( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-    unsigned uTruth0, uTruth1, uPhase;
-    int clk = clock();
-
-    assert( pCut->nVarsMax < 6 );
-
-    // assign the truth table
-    if ( pCut0->nLeaves == pCut->nLeaves )
-        uTruth0 = *Cut_CutReadTruth(pCut0);
-    else
+    Extra_TruthExpand( pCut->nVarsMax, nTruthWords, Cut_CutReadTruth(pCut0), uPhase, uTruth0 );
+    if ( fCompl0 ) 
     {
-        assert( pCut0->nLeaves < pCut->nLeaves );
-        uPhase = Cut_TruthPhase( pCut, pCut0 );
-        if ( pCut->nVarsMax == 4 )
-        {
-            assert( pCut0->nLeaves < 4 );
-            assert( uPhase < 16 );
-            uTruth0 = p->pPerms43[pCut0->uTruth & 0xFF][uPhase];
-        }
-        else
-        {
-            assert( pCut->nVarsMax == 5 );
-            assert( pCut0->nLeaves < 5 );
-            assert( uPhase < 32 );
-            if ( pCut0->nLeaves == 4 )
-            {
-//                Count4++;
-/*
-                if ( uPhase == 31-16 ) // 01111
-                    uTruth0 = pCut0->uTruth;
-                else if ( uPhase == 31-8 ) // 10111
-                    uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][0];
-                else if ( uPhase == 31-4 ) // 11011
-                    uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][1];
-                else if ( uPhase == 31-2 ) // 11101
-                    uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][2];
-                else if ( uPhase == 31-1 ) // 11110
-                    uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][3];
-                else
-                    assert( 0 );
-*/
-                uTruth0 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut0), uPhase );
-            }
-            else
-            {
-//                Count5++;
-//                uTruth0 = p->pPerms53[pCut0->uTruth & 0xFF][uPhase];
-                uTruth0 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut0), uPhase );
-            }
-        }
+        for ( i = 0; i < nTruthWords; i++ )
+            uTruth0[i] = ~uTruth0[i];
     }
-    uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
 
-    // assign the truth table
-    if ( pCut1->nLeaves == pCut->nLeaves )
-        uTruth0 = *Cut_CutReadTruth(pCut1);
-    else
+    // permute the second table
+    uPhase = Cut_TruthPhase( pCut, pCut1 );
+    Extra_TruthExpand( pCut->nVarsMax, nTruthWords, Cut_CutReadTruth(pCut1), uPhase, uTruth1 );
+    if ( fCompl1 ) 
     {
-        assert( pCut1->nLeaves < pCut->nLeaves );
-        uPhase = Cut_TruthPhase( pCut, pCut1 );
-        if ( pCut->nVarsMax == 4 )
-        {
-            assert( pCut1->nLeaves < 4 );
-            assert( uPhase < 16 );
-            uTruth1 = p->pPerms43[pCut1->uTruth & 0xFF][uPhase];
-        }
-        else
-        {
-            assert( pCut->nVarsMax == 5 );
-            assert( pCut1->nLeaves < 5 );
-            assert( uPhase < 32 );
-            if ( pCut1->nLeaves == 4 )
-            {
-//                Count4++;
-/*
-                if ( uPhase == 31-16 ) // 01111
-                    uTruth1 = pCut1->uTruth;
-                else if ( uPhase == 31-8 ) // 10111
-                    uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][0];
-                else if ( uPhase == 31-4 ) // 11011
-                    uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][1];
-                else if ( uPhase == 31-2 ) // 11101
-                    uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][2];
-                else if ( uPhase == 31-1 ) // 11110
-                    uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][3];
-                else
-                    assert( 0 );
-*/
-                uTruth1 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut1), uPhase );
-            }
-            else
-            {
-//                Count5++;
-//                uTruth1 = p->pPerms53[pCut1->uTruth & 0xFF][uPhase];
-                uTruth1 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut1), uPhase );
-            }
-        }
+        for ( i = 0; i < nTruthWords; i++ )
+            uTruth1[i] = ~uTruth1[i];
     }
-    uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
-    uTruth1 = uTruth0 & uTruth1;
-    if ( pCut->fCompl )
-        uTruth1 = ~uTruth1;
-    if ( pCut->nVarsMax == 4 )
-        uTruth1 &= 0xFFFF; 
-    Cut_CutWriteTruth( pCut, &uTruth1 );
-p->timeTruth += clock() - clk;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Expands the truth table according to the phase.]
-
-  Description []
-               
-  SideEffects []
 
-  SeeAlso     []
+    // write the resulting table
+    pTruthRes = Cut_CutReadTruth(pCut);
 
-***********************************************************************/
-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-- )
+    if ( pCut->fCompl )
     {
-        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 );
+        for ( i = 0; i < nTruthWords; i++ )
+            pTruthRes[i] = ~(uTruth0[i] & uTruth1[i]);
     }
-}
-
-/**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 )
+    else
     {
-        Cut_TruthCompute4( p, pCut, pCut0, pCut1 );
-        return;
+        for ( i = 0; i < nTruthWords; i++ )
+            pTruthRes[i] = uTruth0[i] & uTruth1[i];
     }
-
-    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                                ///
 ////////////////////////////////////////////////////////////////////////