Version abc50910

11 files changed, 546 insertions, 657 deletions

diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index 6719ed4d..49dde875 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -43,7 +43,6 @@ struct Cut_ParamsStruct_t_
     int  nKeepMax;      // the max number of cuts kept at a node
     int  nIdsMax;       // the max number of IDs of cut objects
     int  fTruth;        // compute truth tables
-    int  fHash;         // hash cuts to detect unique
     int  fFilter;       // filter dominated cuts
     int  fSeq;          // compute sequential cuts
     int  fDrop;         // drop cuts on the fly
@@ -53,28 +52,25 @@ struct Cut_ParamsStruct_t_
 struct Cut_CutStruct_t_
 {
     unsigned           uTruth     : 16;   // truth table for 4-input cuts
-    unsigned           uPhase     :  7;   // the phase when mapping into a canonical form
+    unsigned           uPhase     :  8;   // 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           fSeq       :  1;   // the cut is sequential
     unsigned           nVarsMax   :  3;   // the max number of vars [4-6]
     unsigned           nLeaves    :  3;   // the number of leaves [4-6]
+    unsigned           uSign;             // the signature
     Cut_Cut_t *        pNext;             // the next cut in the list
-    void *             pData;             // the user data
     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 + p->fSeq); }
+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 void *     Cut_CutReadData( Cut_Cut_t * p )      {  return p->pData;     }
 
-static inline void       Cut_CutWriteData( Cut_Cut_t * p, void * pData )  { p->pData = pData;  }
 static inline void       Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth )  { 
     if ( p->nVarsMax == 4 )  { p->uTruth = *puTruth;  return; }
-    p->pLeaves[p->nVarsMax + p->fSeq] = (int)puTruth[0];
-    if ( p->nVarsMax == 6 )  p->pLeaves[p->nVarsMax + p->fSeq + 1] = (int)puTruth[1];
+    p->pLeaves[p->nVarsMax] = (int)puTruth[0];
+    if ( p->nVarsMax == 6 )  p->pLeaves[p->nVarsMax + 1] = (int)puTruth[1];
 }
 
 ////////////////////////////////////////////////////////////////////////
@@ -85,21 +81,23 @@ static inline void       Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth )
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== 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 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 );
 /*=== 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_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
+extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
 /*=== cutNode.c ==========================================================*/
-extern void             Cut_NodeSetTriv( Cut_Man_t * p, int Node );
 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_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
-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 void             Cut_NodeFreeCuts( Cut_Man_t * p, int Node );
-extern void             Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node );
-extern void             Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node );
-extern void             Cut_CutPrint( Cut_Cut_t * pCut );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutApi.c b/src/opt/cut/cutApi.c
new file mode 100644
index 00000000..0e7c2506
--- /dev/null
+++ b/src/opt/cut/cutApi.c
@@ -0,0 +1,131 @@
+/**CFile****************************************************************
+
+  FileName    [cutNode.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Procedures to compute cuts for a node.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the linked list of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
+{
+    if ( Node >= p->vCuts->nSize )
+        return NULL;
+    return Vec_PtrEntry( p->vCuts, Node );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the linked list of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
+{
+    Vec_PtrWriteEntry( p->vCuts, Node, pList );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the trivial cut for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
+{
+    assert( Cut_NodeReadCuts(p, Node) == NULL );
+    Cut_NodeWriteCuts( p, Node, Cut_CutCreateTriv(p, Node) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Consider dropping cuts if they are useless by now.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node )
+{
+    int nFanouts;
+    assert( p->vFanCounts );
+    nFanouts = Vec_IntEntry( p->vFanCounts, Node );
+    assert( nFanouts > 0 );
+    if ( --nFanouts == 0 )
+        Cut_NodeFreeCuts( p, Node );
+    Vec_IntWriteEntry( p->vFanCounts, Node, nFanouts );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the cuts at the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeFreeCuts( Cut_Man_t * p, int Node )
+{
+    Cut_Cut_t * pList, * pCut, * pCut2;
+    pList = Cut_NodeReadCuts( p, Node );
+    if ( pList == NULL )
+        return;
+    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+        Cut_CutRecycle( p, pCut );
+    Cut_NodeWriteCuts( p, Node, NULL );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutCut.c b/src/opt/cut/cutCut.c
new file mode 100644
index 00000000..d2cce61f
--- /dev/null
+++ b/src/opt/cut/cutCut.c
@@ -0,0 +1,171 @@
+/**CFile****************************************************************
+
+  FileName    [cutNode.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Procedures to compute cuts for a node.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start the cut computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutAlloc( Cut_Man_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;
+    // statistics
+    p->nCutsAlloc++;
+    p->nCutsCur++;
+    if ( p->nCutsPeak < p->nCutsAlloc - p->nCutsDealloc )
+        p->nCutsPeak = p->nCutsAlloc - p->nCutsDealloc;
+    return pCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Start the cut computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
+{
+    Cut_Cut_t * pCut;
+    pCut = Cut_CutAlloc( p );
+    pCut->nLeaves    = 1;
+    pCut->pLeaves[0] = Node;
+    pCut->uSign      = (1 << (Node % 32));
+    if ( p->pParams->fTruth )
+        Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
+    p->nCutsTriv++;
+    return pCut;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Start the cut computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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    [Print the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CutPrint( Cut_Cut_t * pCut )
+{
+    int i;
+    assert( pCut->nLeaves > 0 );
+    printf( "%d : {", pCut->nLeaves );
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        printf( " %d", pCut->pLeaves[i] );
+    printf( " }" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Consider dropping cuts if they are useless by now.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{
+    printf( "\n" );
+    printf( "%d : %5d %5d %5d %5d %5d\n", 
+        pCut0->nLeaves, 
+        pCut0->nLeaves > 0 ? pCut0->pLeaves[0] : -1, 
+        pCut0->nLeaves > 1 ? pCut0->pLeaves[1] : -1, 
+        pCut0->nLeaves > 2 ? pCut0->pLeaves[2] : -1, 
+        pCut0->nLeaves > 3 ? pCut0->pLeaves[3] : -1, 
+        pCut0->nLeaves > 4 ? pCut0->pLeaves[4] : -1
+        );
+    printf( "%d : %5d %5d %5d %5d %5d\n", 
+        pCut1->nLeaves, 
+        pCut1->nLeaves > 0 ? pCut1->pLeaves[0] : -1, 
+        pCut1->nLeaves > 1 ? pCut1->pLeaves[1] : -1, 
+        pCut1->nLeaves > 2 ? pCut1->pLeaves[2] : -1, 
+        pCut1->nLeaves > 3 ? pCut1->pLeaves[3] : -1, 
+        pCut1->nLeaves > 4 ? pCut1->pLeaves[4] : -1
+        );
+    if ( pCut == NULL )
+        printf( "Cannot merge\n" );
+    else
+        printf( "%d : %5d %5d %5d %5d %5d\n", 
+            pCut->nLeaves, 
+            pCut->nLeaves > 0 ? pCut->pLeaves[0] : -1, 
+            pCut->nLeaves > 1 ? pCut->pLeaves[1] : -1, 
+            pCut->nLeaves > 2 ? pCut->pLeaves[2] : -1, 
+            pCut->nLeaves > 3 ? pCut->pLeaves[3] : -1, 
+            pCut->nLeaves > 4 ? pCut->pLeaves[4] : -1
+            );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index fe5080b4..2d4443f1 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -48,7 +48,6 @@ struct Cut_ManStruct_t_
     // storage for cuts
     Vec_Ptr_t *        vCuts;            // cuts by ID
     Vec_Ptr_t *        vCutsNew;         // cuts by ID
-    Cut_HashTable_t *  tTable;           // cuts by their leaves (and root)
     // memory management
     Extra_MmFixed_t *  pMmCuts;
     int                EntrySize;
@@ -58,6 +57,7 @@ struct Cut_ManStruct_t_
     int                fCompl0;
     int                fCompl1;
     int                fSimul;
+    int                nNodeCuts;
     // precomputations
     unsigned           uTruthVars[6][2];
     unsigned short **  pPerms43;
@@ -69,7 +69,8 @@ struct Cut_ManStruct_t_
     int                nCutsDealloc;
     int                nCutsPeak;
     int                nCutsTriv;
-    int                nCutsNode;
+    int                nCutsFilter;
+    int                nCutsLimit;
     int                nNodes;
     // runtime
     int                timeMerge;
@@ -79,6 +80,22 @@ struct Cut_ManStruct_t_
     int                timeHash;
 };
 
+// iterator through all the cuts of the list
+#define Cut_ListForEachCut( pList, pCut )                 \
+    for ( pCut = pList;                                   \
+          pCut;                                           \
+          pCut = pCut->pNext )
+#define Cut_ListForEachCutStop( pList, pCut, pStop )      \
+    for ( pCut = pList;                                   \
+          pCut != pStop;                                  \
+          pCut = pCut->pNext )
+#define Cut_ListForEachCutSafe( pList, pCut, pCut2 )      \
+    for ( pCut = pList,                                   \
+          pCut2 = pCut? pCut->pNext: NULL;                \
+          pCut;                                           \
+          pCut = pCut2,                                   \
+          pCut2 = pCut? pCut->pNext: NULL )
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
@@ -87,10 +104,14 @@ struct Cut_ManStruct_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== 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 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 );
-/*=== cutNode.c ==========================================================*/
-extern Cut_Cut_t *         Cut_CutAlloc( Cut_Man_t * p );
 /*=== cutTable.c ==========================================================*/
 extern Cut_HashTable_t *   Cut_TableStart( int Size );
 extern void                Cut_TableStop( Cut_HashTable_t * pTable );
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index 4ad3a66a..31e003cf 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -49,7 +49,7 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
     // set and correct parameters
     p->pParams = pParams;
     if ( p->pParams->fSeq )
-        p->pParams->fHash = 1;
+        p->pParams->fFilter = 1;
     // space for cuts
     p->vCuts = Vec_PtrAlloc( pParams->nIdsMax );
     Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
@@ -58,25 +58,17 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
         p->vCutsNew = Vec_PtrAlloc( pParams->nIdsMax );
         Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
     }
-    // hash tables
-    if ( pParams->fHash )
-        p->tTable = Cut_TableStart( p->pParams->nKeepMax );
     // entry size
     p->EntrySize = sizeof(Cut_Cut_t) + (pParams->nVarsMax + pParams->fSeq) * sizeof(int);
-    if ( pParams->nVarsMax == 5 )
-        p->EntrySize += sizeof(unsigned);
-    else if ( pParams->nVarsMax == 6 )
-        p->EntrySize += 2 * sizeof(unsigned);
+    if ( pParams->fTruth )
+    {
+        if ( pParams->nVarsMax == 5 )
+            p->EntrySize += sizeof(unsigned);
+        else if ( pParams->nVarsMax == 6 )
+            p->EntrySize += 2 * sizeof(unsigned);
+    }
     // memory for cuts
     p->pMmCuts = Extra_MmFixedStart( p->EntrySize );
-    // precomputations
-//    if ( pParams->fTruth && pParams->nVarsMax == 4 )
-//        p->pPerms43 = Extra_TruthPerm43();
-//    else if ( pParams->fTruth )
-//    {
-//        p->pPerms53 = Extra_TruthPerm53();
-//        p->pPerms54 = Extra_TruthPerm54();
-//    }
     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
@@ -104,13 +96,10 @@ void Cut_ManStop( Cut_Man_t * p )
     Cut_Cut_t * pCut;
     int i;
     Vec_PtrForEachEntry( p->vCuts, pCut, i )
-    {
         if ( pCut != NULL )
         {
             int k = 0;
         }
-    }
-
     if ( p->vCutsNew )   Vec_PtrFree( p->vCutsNew );
     if ( p->vCuts )      Vec_PtrFree( p->vCuts );
     if ( p->vFanCounts ) Vec_IntFree( p->vFanCounts );
@@ -118,7 +107,6 @@ void Cut_ManStop( Cut_Man_t * p )
     if ( p->pPerms53 )   free( p->pPerms53 );
     if ( p->pPerms54 )   free( p->pPerms54 );
     if ( p->vTemp )      Vec_PtrFree( p->vTemp );
-    if ( p->tTable )     Cut_TableStop( p->tTable );
     Extra_MmFixedStop( p->pMmCuts, 0 );
     free( p );
 }
@@ -141,12 +129,13 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     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( "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) );
     PRT( "Merge ", p->timeMerge );
     PRT( "Union ", p->timeUnion );
-    PRT( "Hash  ", Cut_TableReadTime(p->tTable) );
     PRT( "Filter", p->timeFilter );
     PRT( "Truth ", p->timeTruth );
 }
@@ -168,6 +157,22 @@ void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts )
     p->vFanCounts = vFanCounts;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_ManReadVarsMax( Cut_Man_t * p )
+{
+    return p->pParams->nVarsMax;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 8d16ac8a..e8a0bc87 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -25,36 +25,13 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node );
-static inline void        Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut );
-static inline int         Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList );
-
-static void               Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
-static void               Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList );
-
-// iterator through all the cuts of the list
-#define Cut_ListForEachCut( pList, pCut )                 \
-    for ( pCut = pList;                                   \
-          pCut;                                           \
-          pCut = pCut->pNext )
-#define Cut_ListForEachCutStop( pList, pCut, pStop )      \
-    for ( pCut = pList;                                   \
-          pCut != pStop;                                  \
-          pCut = pCut->pNext )
-#define Cut_ListForEachCutSafe( pList, pCut, pCut2 )      \
-    for ( pCut = pList,                                   \
-          pCut2 = pCut? pCut->pNext: NULL;                \
-          pCut;                                           \
-          pCut = pCut2,                                   \
-          pCut2 = pCut? pCut->pNext: NULL )
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the pointer to the linked list of cuts.]
+  Synopsis    [Returns 1 if pDom is contained in pCut.]
 
   Description []
                
@@ -63,49 +40,96 @@ static void               Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList );
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
+static inline int Cut_CutCheckDominance( Cut_Cut_t * pDom, Cut_Cut_t * pCut )
 {
-    if ( Node >= p->vCuts->nSize )
-        return NULL;
-    return Vec_PtrEntry( p->vCuts, Node );
+    int i, k;
+    for ( i = 0; i < (int)pDom->nLeaves; i++ )
+    {
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
+                break;
+        if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
+            return 0;
+    }
+    // every node in pDom is contained in pCut
+    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the pointer to the linked list of cuts.]
+  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     []
 
 ***********************************************************************/
-void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
+static inline int Cut_CutFilterOne( Cut_Man_t * p, Cut_List_t * pSuperList, Cut_Cut_t * pCut )
 {
-    Vec_PtrWriteEntry( p->vCuts, Node, pList );
-}
+    Cut_Cut_t * pTemp, * pTemp2, ** ppTail;
+    int a;
 
-/**Function*************************************************************
-
-  Synopsis    [Sets the trivial cut for the node.]
-
-  Description []
-               
-  SideEffects []
+    // check if this cut is filtered out by smaller cuts
+    for ( a = 2; a <= (int)pCut->nLeaves; a++ )
+    {
+        Cut_ListForEachCut( pSuperList->pHead[a], pTemp )
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+                continue;
+            // check containment seriously
+            if ( Cut_CutCheckDominance( pTemp, pCut ) )
+            {
+                p->nCutsFilter++;
+                Cut_CutRecycle( p, pCut );
+                return 1;
+            }
+        }
+    }
 
-  SeeAlso     []
+    // filter out other cuts using this one
+    for ( a = pCut->nLeaves + 1; a <= (int)pCut->nVarsMax; a++ )
+    {
+        ppTail = pSuperList->pHead + a;
+        Cut_ListForEachCutSafe( pSuperList->pHead[a], pTemp, pTemp2 )
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
+            {
+                ppTail = &pTemp->pNext;
+                continue;
+            }
+            // check containment seriously
+            if ( Cut_CutCheckDominance( pCut, pTemp ) )
+            {
+                p->nCutsFilter++;
+                p->nNodeCuts--;
+                // move the head
+                if ( pSuperList->pHead[a] == pTemp )
+                    pSuperList->pHead[a] = pTemp->pNext;
+                // move the tail
+                if ( pSuperList->ppTail[a] == &pTemp->pNext )
+                    pSuperList->ppTail[a] = ppTail;
+                // skip the given cut in the list
+                *ppTail = pTemp->pNext;
+                // recycle pTemp
+                Cut_CutRecycle( p, pTemp );
+            }
+            else
+                ppTail = &pTemp->pNext;
+        }
+        assert( ppTail == pSuperList->ppTail[a] );
+        assert( *ppTail == NULL );
+    }
 
-***********************************************************************/
-void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
-{
-    assert( Cut_NodeReadCuts(p, Node) == NULL );
-    Cut_NodeWriteCuts( p, Node, Cut_CutCreateTriv(p, Node) );
+    return 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Deallocates the cuts at the node.]
+  Synopsis    [Filters cuts using dominance.]
 
   Description []
                
@@ -114,31 +138,79 @@ void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeFreeCuts( Cut_Man_t * p, int Node )
-{
-    Cut_Cut_t * pList, * pCut, * pCut2;
-    pList = Cut_NodeReadCuts( p, Node );
-    if ( pList == NULL )
-        return;
-    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
-        Cut_CutRecycle( p, pCut );
-    Cut_NodeWriteCuts( p, Node, NULL );
+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    []
+  Synopsis    [Processes two cuts.]
 
-  Description []
+  Description [Returns 1 if the limit has been reached.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node )
+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 );
+    else
+        pCut = Cut_CutMergeTwo( p, pCut1, pCut0 );
+    if ( pCut == NULL )
+        return 0;
+    assert( 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;
+    // compute the truth table
+    if ( p->pParams->fTruth )
+        Cut_TruthCompute( p, pCut, pCut0, pCut1 );
+    // add to the list
+    Cut_ListAdd( pSuperList, pCut );
+    // return status (0 if okay; 1 if exceeded the limit)
+    return ++p->nNodeCuts == p->pParams->nKeepMax;
 }
 
 /**Function*************************************************************
@@ -159,6 +231,7 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
     int i, Limit = p->pParams->nVarsMax;
     int clk = clock();
     assert( p->pParams->nVarsMax <= 6 );
+
     // start the new list
     Cut_ListStart( &SuperList );
     // get the cut lists of children
@@ -180,27 +253,37 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
     // start with the elementary cut
     pTemp0 = Cut_CutCreateTriv( p, Node );
     Cut_ListAdd( &SuperList, pTemp0 );
-    p->nCutsNode = 1;
+    p->nNodeCuts = 1;
     // small by small
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
             goto finish;
-    // all by large
-    Cut_ListForEachCut( pList0, pTemp0 )
+    // 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 ) )
             goto finish;
-    // all by large
-    Cut_ListForEachCut( pList1, pTemp1 )
+    }
+    // small by large
+    Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
     Cut_ListForEachCut( pStop0, pTemp0 )
+    {
+        if ( (pTemp0->uSign & pTemp1->uSign) != pTemp1->uSign )
+            continue;
         if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
             goto finish;
+    }
     // large by large
     Cut_ListForEachCut( pStop0, pTemp0 )
     Cut_ListForEachCut( pStop1, pTemp1 )
     {
         assert( pTemp0->nLeaves == (unsigned)Limit && pTemp1->nLeaves == (unsigned)Limit );
+        if ( pTemp0->uSign != pTemp1->uSign )
+            continue;
         for ( i = 0; i < Limit; i++ )
             if ( pTemp0->pLeaves[i] != pTemp1->pLeaves[i] )
                 break;
@@ -210,14 +293,13 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
             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 );
-    // clear the hash table
-    if ( p->pParams->fHash && !p->pParams->fSeq )
-        Cut_TableClear( p->tTable );
     // consider dropping the fanins cuts
     if ( p->pParams->fDrop )
     {
@@ -227,8 +309,8 @@ finish :
 p->timeMerge += clock() - clk;
     // filter the cuts
 clk = clock();
-    if ( p->pParams->fFilter )
-        Cut_CutFilter( p, pList0 );
+//    if ( p->pParams->fFilter )
+//        Cut_CutFilter( p, pList0 );
 p->timeFilter += clock() - clk;
     p->nNodes++;
     return pList0;
@@ -236,46 +318,6 @@ p->timeFilter += clock() - clk;
 
 /**Function*************************************************************
 
-  Synopsis    [Processes two cuts.]
-
-  Description [Returns 1 if the limit has been reached.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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;
-    // merge the cuts
-    if ( pCut0->nLeaves >= pCut1->nLeaves )
-        pCut = Cut_CutMergeTwo( p, pCut0, pCut1 );
-    else
-        pCut = Cut_CutMergeTwo( p, pCut1, pCut0 );
-    if ( pCut == NULL )
-        return 0;
-    assert( pCut->nLeaves > 1 );
-    // add the root if sequential
-    if ( p->pParams->fSeq )
-        pCut->pLeaves[pCut->nLeaves] = Root;
-    // check the lookup table
-    if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq  ) )
-    {
-        Cut_CutRecycle( p, pCut );
-        return 0;
-    }
-    // compute the truth table
-    if ( p->pParams->fTruth )
-        Cut_TruthCompute( p, pCut, pCut0, pCut1 );
-    // add to the list
-    Cut_ListAdd( pSuperList, pCut );
-    // return status (0 if okay; 1 if exceeded the limit)
-    return ++p->nCutsNode == p->pParams->nKeepMax;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Computes the cuts by unioning cuts at a choice node.]
 
   Description []
@@ -299,7 +341,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
 
     // remember the root node to save the resulting cuts
     Root = Vec_IntEntry( vNodes, 0 );
-    p->nCutsNode = 1;
+    p->nNodeCuts = 1;
 
     // collect small cuts first
     Vec_PtrClear( p->vTemp );
@@ -311,6 +353,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
         assert( pList );
         // remember the starting point
         pListStart = pList->pNext;
+        pList->pNext = NULL;
         // save or recycle the elementary cut
         if ( i == 0 )
             Cut_ListAdd( &SuperList, pList ), pTop = pList;
@@ -324,20 +367,19 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
                 Vec_PtrPush( p->vTemp, pCut );
                 break;
             }
-            // check hash tables
-            if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) )
-            {
-                Cut_CutRecycle( p, pCut );
+            // check containment
+            if ( p->pParams->fFilter && Cut_CutFilterOne( p, &SuperList, 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 );
-            if ( ++p->nCutsNode == p->pParams->nKeepMax )
+            if ( ++p->nNodeCuts == p->pParams->nKeepMax )
             {
                 // recycle the rest of the cuts of this node
-                Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
+                Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
                     Cut_CutRecycle( p, pCut );
                 // recycle all cuts of other nodes
                 Vec_IntForEachEntryStart( vNodes, Node, k, i+1 )
@@ -349,25 +391,25 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
                 goto finish;
             }
         }
-    }
+    } 
     // collect larger cuts next
     Vec_PtrForEachEntry( p->vTemp, pList, i )
     {
         Cut_ListForEachCutSafe( pList, pCut, pCut2 )
         {
-            if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq  ) )
-            {
-                Cut_CutRecycle( p, pCut );
+            // check containment
+            if ( p->pParams->fFilter && Cut_CutFilterOne( p, &SuperList, 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 );
-            if ( ++p->nCutsNode == p->pParams->nKeepMax )
+            if ( ++p->nNodeCuts == p->pParams->nKeepMax )
             {
                 // recycle the rest of the cuts
-                Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
+                Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
                     Cut_CutRecycle( p, pCut );
                 // recycle the saved cuts of other nodes
                 Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 )
@@ -382,244 +424,16 @@ finish :
     assert( Cut_NodeReadCuts(p, Root) == NULL );
     pList = Cut_ListFinish( &SuperList );
     Cut_NodeWriteCuts( p, Root, pList );
-    // clear the hash table
-    if ( p->pParams->fHash && !p->pParams->fSeq )
-        Cut_TableClear( p->tTable );
 p->timeUnion += clock() - clk;
     // filter the cuts
 clk = clock();
-    if ( p->pParams->fFilter )
-        Cut_CutFilter( p, pList );
+//    if ( p->pParams->fFilter )
+//        Cut_CutFilter( p, pList );
 p->timeFilter += clock() - clk;
     p->nNodes -= vNodes->nSize - 1;
     return pList;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cut_Cut_t * Cut_CutAlloc( Cut_Man_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->fSeq       = p->pParams->fSeq;
-    pCut->fSimul     = p->fSimul;
-    // statistics
-    p->nCutsAlloc++;
-    p->nCutsCur++;
-    if ( p->nCutsPeak < p->nCutsAlloc - p->nCutsDealloc )
-        p->nCutsPeak = p->nCutsAlloc - p->nCutsDealloc;
-    return pCut;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
-{
-    Cut_Cut_t * pCut;
-    pCut = Cut_CutAlloc( p );
-    pCut->nLeaves = 1;
-    pCut->pLeaves[0] = Node;
-    if ( p->pParams->fTruth )
-        Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
-    p->nCutsTriv++;
-    return pCut;
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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    [Consider dropping cuts if they are useless by now.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node )
-{
-    int nFanouts;
-    assert( p->vFanCounts );
-    nFanouts = Vec_IntEntry( p->vFanCounts, Node );
-    assert( nFanouts > 0 );
-    if ( --nFanouts == 0 )
-        Cut_NodeFreeCuts( p, Node );
-    Vec_IntWriteEntry( p->vFanCounts, Node, nFanouts );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Print the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutPrint( Cut_Cut_t * pCut )
-{
-    int i;
-    assert( pCut->nLeaves > 0 );
-    printf( "%d : {", pCut->nLeaves );
-    for ( i = 0; i < (int)pCut->nLeaves; i++ )
-        printf( " %d", pCut->pLeaves[i] );
-    printf( " }" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Consider dropping cuts if they are useless by now.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
-{
-    printf( "\n" );
-    printf( "%d : %5d %5d %5d %5d %5d\n", 
-        pCut0->nLeaves, 
-        pCut0->nLeaves > 0 ? pCut0->pLeaves[0] : -1, 
-        pCut0->nLeaves > 1 ? pCut0->pLeaves[1] : -1, 
-        pCut0->nLeaves > 2 ? pCut0->pLeaves[2] : -1, 
-        pCut0->nLeaves > 3 ? pCut0->pLeaves[3] : -1, 
-        pCut0->nLeaves > 4 ? pCut0->pLeaves[4] : -1
-        );
-    printf( "%d : %5d %5d %5d %5d %5d\n", 
-        pCut1->nLeaves, 
-        pCut1->nLeaves > 0 ? pCut1->pLeaves[0] : -1, 
-        pCut1->nLeaves > 1 ? pCut1->pLeaves[1] : -1, 
-        pCut1->nLeaves > 2 ? pCut1->pLeaves[2] : -1, 
-        pCut1->nLeaves > 3 ? pCut1->pLeaves[3] : -1, 
-        pCut1->nLeaves > 4 ? pCut1->pLeaves[4] : -1
-        );
-    if ( pCut == NULL )
-        printf( "Cannot merge\n" );
-    else
-        printf( "%d : %5d %5d %5d %5d %5d\n", 
-            pCut->nLeaves, 
-            pCut->nLeaves > 0 ? pCut->pLeaves[0] : -1, 
-            pCut->nLeaves > 1 ? pCut->pLeaves[1] : -1, 
-            pCut->nLeaves > 2 ? pCut->pLeaves[2] : -1, 
-            pCut->nLeaves > 3 ? pCut->pLeaves[3] : -1, 
-            pCut->nLeaves > 4 ? pCut->pLeaves[4] : -1
-            );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Filter the cuts using dominance.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList )
-{ 
-    Cut_Cut_t * pListR, ** ppListR = &pListR;
-    Cut_Cut_t * pCut, * pCut2, * pDom, * pPrev;
-    int i, k;
-    // 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;
-            // check if every node in pDom is contained in pCut
-            for ( i = 0; i < (int)pDom->nLeaves; i++ )
-            {
-                for ( k = 0; k < (int)pCut->nLeaves; k++ )
-                    if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
-                        break;
-                if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
-                    break;
-            }
-            if ( i == (int)pDom->nLeaves ) // every node in pDom is contained in pCut
-                break;
-        }
-        if ( pDom != pCut ) // pDom is contained in pCut - recycle pCut
-        {
-            // make sure cuts are connected after removing
-            pPrev->pNext = pCut->pNext;
-/*
-            // report
-            printf( "Recycling cut:   " );
-            Cut_CutPrint( pCut );
-            printf( "\n" );
-            printf( "As contained in: " );
-            Cut_CutPrint( pDom );
-            printf( "\n" );
-*/
-            // 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;
-}
-
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutTable.c b/src/opt/cut/cutTable.c
deleted file mode 100644
index 5dfaca7b..00000000
--- a/src/opt/cut/cutTable.c
+++ /dev/null
@@ -1,253 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cutTable.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [K-feasible cut computation package.]
-
-  Synopsis    [Hashing cuts to prevent duplication.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cutTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cutInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-struct Cut_HashTableStruct_t_
-{
-    int                  nBins;
-    Cut_Cut_t **         pBins;
-    int                  nEntries;
-    int *                pPlaces;
-    int                  nPlaces;
-    int                  timeLookup;
-};
-
-// iterator through all the cuts of the list
-#define Cut_TableListForEachCut( pList, pCut )               \
-    for ( pCut = pList;                                      \
-          pCut;                                              \
-          pCut = pCut->pData )
-#define Cut_TableListForEachCutSafe( pList, pCut, pCut2 )    \
-    for ( pCut = pList,                                      \
-          pCut2 = pCut? pCut->pData: NULL;                   \
-          pCut;                                              \
-          pCut = pCut2,                                      \
-          pCut2 = pCut? pCut->pData: NULL )
-
-// primes used to compute the hash key
-static int s_HashPrimes[10] = { 109, 499, 557, 619, 631, 709, 797, 881, 907, 991 };
-
-// hashing function
-static inline unsigned Cut_HashKey( Cut_Cut_t * pCut )
-{
-    unsigned i, uRes = pCut->nLeaves * s_HashPrimes[9];
-    for ( i = 0; i < pCut->nLeaves + pCut->fSeq; i++ )
-        uRes += s_HashPrimes[i] * pCut->pLeaves[i];
-    return uRes;
-}
-
-// hashing function
-static inline int Cut_CompareTwo( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 )
-{
-    unsigned i;
-    if ( pCut1->nLeaves != pCut2->nLeaves )
-        return 1;
-    for ( i = 0; i < pCut1->nLeaves; i++ )
-        if ( pCut1->pLeaves[i] != pCut2->pLeaves[i] )
-            return 1;
-    return 0;
-}
-
-static void Cut_TableResize( Cut_HashTable_t * pTable );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cut_HashTable_t * Cut_TableStart( int Size )
-{
-    Cut_HashTable_t * pTable;
-    pTable = ALLOC( Cut_HashTable_t, 1 );
-    memset( pTable, 0, sizeof(Cut_HashTable_t) );
-    // allocate the table
-    pTable->nBins = Cudd_PrimeCopy( Size );
-    pTable->pBins = ALLOC( Cut_Cut_t *, pTable->nBins );
-    memset( pTable->pBins, 0, sizeof(Cut_Cut_t *) * pTable->nBins );
-    pTable->pPlaces = ALLOC( int, pTable->nBins );
-    return pTable;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TableStop( Cut_HashTable_t * pTable )
-{
-    FREE( pTable->pPlaces );
-    free( pTable->pBins );
-    free( pTable );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Check the existence of a cut in the lookup table]
-
-  Description [Returns 1 if the entry is found.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t * pCut, int fStore )
-{
-    Cut_Cut_t * pEnt;
-    unsigned Key;
-    int clk = clock();
-
-    Key = Cut_HashKey(pCut) % pTable->nBins; 
-    Cut_TableListForEachCut( pTable->pBins[Key], pEnt )
-    {
-        if ( !Cut_CompareTwo( pEnt, pCut ) )
-        {
-pTable->timeLookup += clock() - clk;
-            return 1;
-        }
-    }
-    if ( pTable->nEntries > 2 * pTable->nBins )
-    {
-        Cut_TableResize( pTable );
-        Key = Cut_HashKey(pCut) % pTable->nBins; 
-    }
-    // remember the place
-    if ( fStore && pTable->pBins[Key] == NULL )
-        pTable->pPlaces[ pTable->nPlaces++ ] = Key;
-    // add the cut to the table
-    pCut->pData = pTable->pBins[Key];
-    pTable->pBins[Key] = pCut;
-    pTable->nEntries++;
-pTable->timeLookup += clock() - clk;
-    return 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TableClear( Cut_HashTable_t * pTable )
-{
-    int i;
-    assert( pTable->nPlaces <= pTable->nBins );
-    for ( i = 0; i < pTable->nPlaces; i++ )
-    {
-        assert( pTable->pBins[ pTable->pPlaces[i] ] );
-        pTable->pBins[ pTable->pPlaces[i] ] = NULL;
-    }
-    pTable->nPlaces = 0;
-    pTable->nEntries = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_TableResize( Cut_HashTable_t * pTable )
-{
-    Cut_Cut_t ** pBinsNew;
-    Cut_Cut_t * pEnt, * pEnt2;
-    int nBinsNew, Counter, i, clk;
-    unsigned Key;
-
-clk = clock();
-    // get the new table size
-    nBinsNew = Cudd_PrimeCopy( 3 * pTable->nBins ); 
-    // allocate a new array
-    pBinsNew = ALLOC( Cut_Cut_t *, nBinsNew );
-    memset( pBinsNew, 0, sizeof(Cut_Cut_t *) * nBinsNew );
-    // rehash the entries from the old table
-    Counter = 0;
-    for ( i = 0; i < pTable->nBins; i++ )
-        Cut_TableListForEachCutSafe( pTable->pBins[i], pEnt, pEnt2 )
-        {
-            Key = Cut_HashKey(pEnt) % nBinsNew;
-            pEnt->pData   = pBinsNew[Key];
-            pBinsNew[Key] = pEnt;
-            Counter++;
-        }
-    assert( Counter == pTable->nEntries );
-//    printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
-//    PRT( "Time", clock() - clk );
-    // replace the table and the parameters
-    free( pTable->pBins );
-    pTable->pBins = pBinsNew;
-    pTable->nBins = nBinsNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_TableReadTime( Cut_HashTable_t * pTable )
-{
-    if ( pTable == NULL )
-        return 0;
-    return pTable->timeLookup;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c
index efacd456..cc115042 100644
--- a/src/opt/cut/cutTruth.c
+++ b/src/opt/cut/cutTruth.c
@@ -315,6 +315,7 @@ void Cut_TruthComputeOld( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cu
 p->timeTruth += clock() - clk;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/cut/module.make b/src/opt/cut/module.make
index 1175b3f2..2e7519d1 100644
--- a/src/opt/cut/module.make
+++ b/src/opt/cut/module.make
@@ -1,6 +1,7 @@
-SRC +=  src/opt/cut/cutMan.c \
+SRC +=  src/opt/cut/cutApi.c \
+        src/opt/cut/cutCut.c \
+        src/opt/cut/cutMan.c \
         src/opt/cut/cutMerge.c \
         src/opt/cut/cutNode.c \
         src/opt/cut/cutSeq.c \
-        src/opt/cut/cutTable.c \
         src/opt/cut/cutTruth.c 
diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
index f6654476..ed7e94c8 100644
--- a/src/opt/dec/decFactor.c
+++ b/src/opt/dec/decFactor.c
@@ -183,7 +183,7 @@ Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
 ***********************************************************************/
 Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple )
 {
-    Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
     Vec_Int_t * vEdgeLits  = pManDec->vLits;
     Mvc_Cover_t * pDiv, * pQuo, * pRem;
     Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
@@ -228,7 +228,7 @@ Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cov
 ***********************************************************************/
 Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
 {
-    Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
     Vec_Int_t * vEdgeCubes = pManDec->vCubes;
     Vec_Int_t * vEdgeLits  = pManDec->vLits;
     Mvc_Manager_t * pMem = pManDec->pMvcMem;
@@ -323,7 +323,7 @@ Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes
 ***********************************************************************/
 Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
 {
-    Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    Dec_Man_t * pManDec = Abc_FrameReadManDec();
     Mvc_Manager_t * pMem = pManDec->pMvcMem;
     Mvc_Cover_t * pMvc;
     Mvc_Cube_t * pMvcCube;
@@ -365,7 +365,7 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
 ***********************************************************************/
 int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
 {
-    DdManager * dd = Abc_FrameReadManDd( Abc_FrameGetGlobalFrame() );
+    DdManager * dd = Abc_FrameReadManDd();
     DdNode * bFunc1, * bFunc2;
     int RetValue;
     bFunc1 = Abc_ConvertSopToBdd( dd, pSop );    Cudd_Ref( bFunc1 );
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index bfeaa273..6bf1fdbe 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -50,7 +50,7 @@ clk = clock();
     p = ALLOC( Rwr_Man_t, 1 );
     memset( p, 0, sizeof(Rwr_Man_t) );
     p->nFuncs = (1<<16);
-    pManDec   = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    pManDec   = Abc_FrameReadManDec();
     p->puCanons = pManDec->puCanons; 
     p->pPhases  = pManDec->pPhases; 
     p->pPerms   = pManDec->pPerms;