Version abc50822

10 files changed, 2411 insertions, 0 deletions

diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
new file mode 100644
index 00000000..0b4c4535
--- /dev/null
+++ b/src/opt/cut/cut.h
@@ -0,0 +1,108 @@
+/**CFile****************************************************************
+
+  FileName    [cut.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: .h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CUT_H__
+#define __CUT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cut_ManStruct_t_         Cut_Man_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  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
+    int  fVerbose;      // the verbosiness flag
+};
+
+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           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]
+    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_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];
+}
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== 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 );
+/*=== 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 );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
new file mode 100644
index 00000000..da54a188
--- /dev/null
+++ b/src/opt/cut/cutInt.h
@@ -0,0 +1,107 @@
+/**CFile****************************************************************
+
+  FileName    [cutInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CUT_INT_H__
+#define __CUT_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+#include "vec.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cut_HashTableStruct_t_ Cut_HashTable_t;
+
+struct Cut_ManStruct_t_
+{
+    // user preferences
+    Cut_Params_t *     pParams;          // computation parameters
+    Vec_Int_t *        vFanCounts;       // the array of fanout counters
+    // storage for cuts
+    Vec_Ptr_t *        vCuts;            // cuts by ID
+    Vec_Ptr_t *        vCutsNew;         // cuts by ID
+    Cut_HashTable_t *  tTable;           // cuts by their leaves (and root)
+    // memory management
+    Extra_MmFixed_t *  pMmCuts;
+    int                EntrySize;
+    // temporary variables
+    Cut_Cut_t *        pReady;
+    Vec_Ptr_t *        vTemp;
+    int                fCompl0;
+    int                fCompl1;
+    int                fSimul;
+    // precomputations
+    unsigned           uTruthVars[6][2];
+    unsigned short **  pPerms43;
+    unsigned **        pPerms53;
+    unsigned **        pPerms54;
+    // statistics
+    int                nCutsCur;
+    int                nCutsAlloc;
+    int                nCutsDealloc;
+    int                nCutsPeak;
+    int                nCutsTriv;
+    int                nCutsNode;
+    // runtime
+    int                timeMerge;
+    int                timeUnion;
+    int                timeTruth;
+    int                timeFilter;
+    int                timeHash;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== 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 );
+extern int                 Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t * pCut, int fStore );
+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 );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/cut/cutList.h b/src/opt/cut/cutList.h
new file mode 100644
index 00000000..eb008ef9
--- /dev/null
+++ b/src/opt/cut/cutList.h
@@ -0,0 +1,115 @@
+/**CFile****************************************************************
+
+  FileName    [cutList.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Implementation of layered listed list of cuts.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutList.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __CUT_LIST_H__
+#define __CUT_LIST_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cut_ListStruct_t_         Cut_List_t;
+struct Cut_ListStruct_t_
+{
+    Cut_Cut_t *  pHead[7];
+    Cut_Cut_t ** ppTail[7];
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cut_ListStart( Cut_List_t * p )
+{
+    int i;
+    for ( i = 1; i <= 6; i++ )
+    {
+        p->pHead[i] = 0;
+        p->ppTail[i] = &p->pHead[i];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cut_ListAdd( Cut_List_t * p, Cut_Cut_t * pCut )
+{
+    assert( pCut->nLeaves > 0 && pCut->nLeaves < 7 );
+    *p->ppTail[pCut->nLeaves] = pCut;
+    p->ppTail[pCut->nLeaves] = &pCut->pNext;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Cut_Cut_t * Cut_ListFinish( Cut_List_t * p )
+{
+    int i;
+    for ( i = 1; i < 6; i++ )
+        *p->ppTail[i] = p->pHead[i+1];
+    *p->ppTail[6] = NULL;
+    return p->pHead[1];
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
new file mode 100644
index 00000000..a96f8173
--- /dev/null
+++ b/src/opt/cut/cutMan.c
@@ -0,0 +1,174 @@
+/**CFile****************************************************************
+
+  FileName    [cutMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Cut manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
+{
+    Cut_Man_t * p;
+    int clk = clock();
+    assert( pParams->nVarsMax >= 4 && pParams->nVarsMax <= 6 );
+    p = ALLOC( Cut_Man_t, 1 );
+    memset( p, 0, sizeof(Cut_Man_t) );
+    // set and correct parameters
+    p->pParams = pParams;
+    if ( p->pParams->fSeq )
+        p->pParams->fHash = 1;
+    // space for cuts
+    p->vCuts = Vec_PtrAlloc( pParams->nIdsMax );
+    Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
+    if ( pParams->fSeq )
+    {
+        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);
+    // 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
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the cut manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+    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->tTable )     Cut_TableStop( p->tTable );
+    Extra_MmFixedStop( p->pMmCuts, 0 );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_ManPrintStats( Cut_Man_t * p )
+{
+    printf( "Cut computation statistics:\n" );
+    printf( "Current cuts      = %8d. (Trivial = %d.)\n", p->nCutsCur-p->nCutsTriv, p->nCutsTriv );
+    printf( "Peak cuts         = %8d.\n", p->nCutsPeak );
+    printf( "Total allocated   = %8d.\n", p->nCutsAlloc );
+    printf( "Total deallocated = %8d.\n", p->nCutsDealloc );
+    printf( "The cut size      = %3d bytes.\n", p->EntrySize );
+    printf( "Peak memory       = %.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 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts )
+{
+    p->vFanCounts = vFanCounts;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutMerge.c b/src/opt/cut/cutMerge.c
new file mode 100644
index 00000000..ba1afce4
--- /dev/null
+++ b/src/opt/cut/cutMerge.c
@@ -0,0 +1,656 @@
+/**CFile****************************************************************
+
+  FileName    [cutMerge.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Procedure to merge two cuts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description [This procedure works.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{ 
+    static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}};
+    Cut_Cut_t * pRes;
+    int * pRow;
+    int nLeaves0, nLeaves1, Limit;
+    int i, k, Count, nNodes;
+
+    assert( pCut0->nLeaves >= pCut1->nLeaves );
+
+    // the case of the largest cut sizes
+    Limit = p->pParams->nVarsMax;
+    nLeaves0 = pCut0->nLeaves;
+    nLeaves1 = pCut1->nLeaves;
+    if ( nLeaves0 == Limit && nLeaves1 == Limit )
+    {
+        for ( i = 0; i < nLeaves0; i++ )
+            if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
+                return NULL;
+        pRes = Cut_CutAlloc( p );
+        for ( i = 0; i < nLeaves0; i++ )
+            pRes->pLeaves[i] = pCut0->pLeaves[i];
+        pRes->nLeaves = nLeaves0;
+        return pRes;
+    }
+    // the case when one of the cuts is the largest
+    if ( nLeaves0 == Limit )
+    {
+        for ( i = 0; i < nLeaves1; i++ )
+        {
+            for ( k = nLeaves0 - 1; k >= 0; k-- )
+                if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
+                    break;
+            if ( k == -1 ) // did not find
+                return NULL;
+        }
+        pRes = Cut_CutAlloc( p );
+        for ( i = 0; i < nLeaves0; i++ )
+            pRes->pLeaves[i] = pCut0->pLeaves[i];
+        pRes->nLeaves = nLeaves0;
+        return pRes;
+    }
+    // other cases
+    nNodes = nLeaves0;
+    for ( i = 0; i < nLeaves1; i++ )
+    {
+        for ( k = nLeaves0 - 1; k >= 0; k-- )
+        {
+            if ( pCut0->pLeaves[k] > pCut1->pLeaves[i] )
+                continue;
+            if ( pCut0->pLeaves[k] < pCut1->pLeaves[i] )
+            {
+                pRow = M[k+1];
+                if ( pRow[0] == 0 )
+                    pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
+                else if ( pRow[1] == 0 )
+                    pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
+                else if ( pRow[2] == 0 )
+                    pRow[2] = pCut1->pLeaves[i];
+                else 
+                    assert( 0 );
+                if ( ++nNodes > Limit )
+                {
+                    for ( i = 0; i <= nLeaves0; i++ )
+                        M[i][0] = 0;
+                    return NULL;
+                }
+            }
+            break;
+        }
+        if ( k == -1 )
+        {
+            pRow = M[0];
+            if ( pRow[0] == 0 )
+                pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
+            else if ( pRow[1] == 0 )
+                pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
+            else if ( pRow[2] == 0 )
+                pRow[2] = pCut1->pLeaves[i];
+            else 
+                assert( 0 );
+            if ( ++nNodes > Limit )
+            {
+                for ( i = 0; i <= nLeaves0; i++ )
+                    M[i][0] = 0;
+                return NULL;
+            }
+            continue;
+        }
+    }
+
+    pRes = Cut_CutAlloc( p );
+    for ( Count = 0, i = 0; i <= nLeaves0; i++ )
+    {
+        if ( i > 0 )
+            pRes->pLeaves[Count++] = pCut0->pLeaves[i-1];
+        pRow = M[i];
+        if ( pRow[0] )
+        {
+            pRes->pLeaves[Count++] = pRow[0];
+            if ( pRow[1] )
+            {
+                pRes->pLeaves[Count++] = pRow[1];
+                if ( pRow[2] )
+                    pRes->pLeaves[Count++] = pRow[2];
+            }
+            pRow[0] = 0;
+        }
+    }
+    assert( Count == nNodes );
+    pRes->nLeaves = nNodes;
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeTwo2( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{ 
+    Cut_Cut_t * pRes;
+    int * pLeaves;
+    int Limit, nLeaves0, nLeaves1;
+    int i, k, c;
+
+    assert( pCut0->nLeaves >= pCut1->nLeaves );
+
+    // consider two cuts
+    nLeaves0 = pCut0->nLeaves;
+    nLeaves1 = pCut1->nLeaves;
+
+    // the case of the largest cut sizes
+    Limit = p->pParams->nVarsMax;
+    if ( nLeaves0 == Limit && nLeaves1 == Limit )
+    {
+        for ( i = 0; i < nLeaves0; i++ )
+            if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
+                return NULL;
+        pRes = Cut_CutAlloc( p );
+        for ( i = 0; i < nLeaves0; i++ )
+            pRes->pLeaves[i] = pCut0->pLeaves[i];
+        pRes->nLeaves = pCut0->nLeaves;
+        return pRes;
+    }
+    // the case when one of the cuts is the largest
+    if ( nLeaves0 == Limit )
+    {
+        for ( i = 0; i < nLeaves1; i++ )
+        {
+            for ( k = nLeaves0 - 1; k >= 0; k-- )
+                if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
+                    break;
+            if ( k == -1 ) // did not find
+                return NULL;
+        }
+        pRes = Cut_CutAlloc( p );
+        for ( i = 0; i < nLeaves0; i++ )
+            pRes->pLeaves[i] = pCut0->pLeaves[i];
+        pRes->nLeaves = pCut0->nLeaves;
+        return pRes;
+    }
+
+    // prepare the cut
+    if ( p->pReady == NULL )
+        p->pReady = Cut_CutAlloc( p );
+    pLeaves = p->pReady->pLeaves;
+
+    // compare two cuts with different numbers
+    i = k = 0;
+    for ( c = 0; c < Limit; c++ )
+    {
+        if ( k == nLeaves1 )
+        {
+            if ( i == nLeaves0 )
+            {
+                p->pReady->nLeaves = c;
+                pRes = p->pReady;  p->pReady = NULL;
+                return pRes;
+            }
+            pLeaves[c] = pCut0->pLeaves[i++];
+            continue;
+        }
+        if ( i == nLeaves0 )
+        {
+            if ( k == nLeaves1 )
+            {
+                p->pReady->nLeaves = c;
+                pRes = p->pReady;  p->pReady = NULL;
+                return pRes;
+            }
+            pLeaves[c] = pCut1->pLeaves[k++];
+            continue;
+        }
+        if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] )
+        {
+            pLeaves[c] = pCut0->pLeaves[i++];
+            continue;
+        }
+        if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] )
+        {
+            pLeaves[c] = pCut1->pLeaves[k++];
+            continue;
+        }
+        pLeaves[c] = pCut0->pLeaves[i++]; 
+        k++;
+    }
+    if ( i < nLeaves0 || k < nLeaves1 )
+        return NULL;
+    p->pReady->nLeaves = c;
+    pRes = p->pReady;  p->pReady = NULL;
+    return pRes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeTwo3( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{ 
+    Cut_Cut_t * pRes;
+    int * pLeaves;
+    int Limit, nLeaves0, nLeaves1;
+    int i, k, c;
+
+    assert( pCut0->nLeaves >= pCut1->nLeaves );
+
+    // prepare the cut
+    if ( p->pReady == NULL )
+        p->pReady = Cut_CutAlloc( p );
+    pLeaves = p->pReady->pLeaves;
+
+    // consider two cuts
+    Limit = p->pParams->nVarsMax;
+    nLeaves0 = pCut0->nLeaves;
+    nLeaves1 = pCut1->nLeaves;
+    if ( nLeaves0 == Limit )
+    { // the case when one of the cuts is the largest
+        if ( nLeaves1 == Limit )
+        { // the case when both cuts are the largest
+            for ( i = 0; i < nLeaves0; i++ )
+            {
+                pLeaves[i] = pCut0->pLeaves[i];
+                if ( pLeaves[i] != pCut1->pLeaves[i] )
+                    return NULL;
+            }
+        }
+        else
+        {
+            for ( i = k = 0; i < nLeaves0; i++ )
+            {
+                pLeaves[i] = pCut0->pLeaves[i];
+                if ( k == (int)nLeaves1 )
+                    continue;
+                if ( pLeaves[i] < pCut1->pLeaves[k] )
+                    continue;
+                if ( pLeaves[i] == pCut1->pLeaves[k++] )
+                    continue;
+                return NULL;
+            }
+            if ( k < nLeaves1 )
+                return NULL;
+        }
+        p->pReady->nLeaves = nLeaves0;
+        pRes = p->pReady;  p->pReady = NULL;
+        return pRes;
+    }
+
+    // compare two cuts with different numbers
+    i = k = 0;
+    for ( c = 0; c < Limit; c++ )
+    {
+        if ( k == nLeaves1 )
+        {
+            if ( i == nLeaves0 )
+            {
+                p->pReady->nLeaves = c;
+                pRes = p->pReady;  p->pReady = NULL;
+                return pRes;
+            }
+            pLeaves[c] = pCut0->pLeaves[i++];
+            continue;
+        }
+        if ( i == nLeaves0 )
+        {
+            if ( k == nLeaves1 )
+            {
+                p->pReady->nLeaves = c;
+                pRes = p->pReady;  p->pReady = NULL;
+                return pRes;
+            }
+            pLeaves[c] = pCut1->pLeaves[k++];
+            continue;
+        }
+        if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] )
+        {
+            pLeaves[c] = pCut0->pLeaves[i++];
+            continue;
+        }
+        if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] )
+        {
+            pLeaves[c] = pCut1->pLeaves[k++];
+            continue;
+        }
+        pLeaves[c] = pCut0->pLeaves[i++]; 
+        k++;
+    }
+    if ( i < nLeaves0 || k < nLeaves1 )
+        return NULL;
+    p->pReady->nLeaves = c;
+    pRes = p->pReady;  p->pReady = NULL;
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeTwo4( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{ 
+    Cut_Cut_t * pRes;
+    int * pLeaves;
+    int i, k, min, NodeTemp, Limit, nTotal;
+
+    assert( pCut0->nLeaves >= pCut1->nLeaves );
+
+    // prepare the cut
+    if ( p->pReady == NULL )
+        p->pReady = Cut_CutAlloc( p );
+    pLeaves = p->pReady->pLeaves;
+
+    // consider two cuts
+    Limit = p->pParams->nVarsMax;
+    if ( pCut0->nLeaves == (unsigned)Limit )
+    { // the case when one of the cuts is the largest
+        if ( pCut1->nLeaves == (unsigned)Limit )
+        { // the case when both cuts are the largest
+            for ( i = 0; i < (int)pCut0->nLeaves; i++ )
+            {
+                pLeaves[i] = pCut0->pLeaves[i];
+                if ( pLeaves[i] != pCut1->pLeaves[i] )
+                    return NULL;
+            }
+        }
+        else
+        {
+            for ( i = k = 0; i < (int)pCut0->nLeaves; i++ )
+            {
+                pLeaves[i] = pCut0->pLeaves[i];
+                if ( k == (int)pCut1->nLeaves )
+                    continue;
+                if ( pLeaves[i] < pCut1->pLeaves[k] )
+                    continue;
+                if ( pLeaves[i] == pCut1->pLeaves[k++] )
+                    continue;
+                return NULL;
+            }
+            if ( k < (int)pCut1->nLeaves )
+                return NULL;
+        }
+        p->pReady->nLeaves = pCut0->nLeaves;
+        pRes = p->pReady;  p->pReady = NULL;
+        return pRes;
+    }
+
+    // count the number of unique entries in pCut1
+    nTotal = pCut0->nLeaves;
+    for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+    {
+        // try to find this entry among the leaves of pCut0
+        for ( k = 0; k < (int)pCut0->nLeaves; k++ )
+            if ( pCut1->pLeaves[i] == pCut0->pLeaves[k] )
+                break;
+        if ( k < (int)pCut0->nLeaves ) // found
+            continue;
+        // we found a new entry to add
+        if ( nTotal == Limit )
+            return NULL;
+        pLeaves[nTotal++] = pCut1->pLeaves[i];
+    }
+    // we know that the feasible cut exists
+
+    // add the starting entries
+    for ( k = 0; k < (int)pCut0->nLeaves; k++ )
+        pLeaves[k] = pCut0->pLeaves[k];
+
+    // selection-sort the entries
+    for ( i = 0; i < nTotal - 1; i++ )
+    {
+        min = i;
+        for ( k = i+1; k < nTotal; k++ )
+            if ( pLeaves[k] < pLeaves[min] )
+                min = k;
+        NodeTemp     = pLeaves[i];
+        pLeaves[i]   = pLeaves[min];
+        pLeaves[min] = NodeTemp;
+    }
+    p->pReady->nLeaves = nTotal;
+    pRes = p->pReady;  p->pReady = NULL;
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description [This procedure works.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_CutMergeTwo5( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
+{ 
+    static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}};
+    Cut_Cut_t * pRes;
+    int * pRow;
+    unsigned uSign0, uSign1;
+    int i, k, nNodes, Count;
+    unsigned Limit = p->pParams->nVarsMax;
+
+    assert( pCut0->nLeaves >= pCut1->nLeaves );
+
+    // the case of the largest cut sizes
+    if ( pCut0->nLeaves == Limit && pCut1->nLeaves == Limit )
+    {
+        for ( i = 0; i < (int)pCut0->nLeaves; i++ )
+            if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
+                return NULL;
+        pRes = Cut_CutAlloc( p );
+        for ( i = 0; i < (int)pCut0->nLeaves; i++ )
+            pRes->pLeaves[i] = pCut0->pLeaves[i];
+        pRes->nLeaves = pCut0->nLeaves;
+        return pRes;
+    }
+    // the case when one of the cuts is the largest
+    if ( pCut0->nLeaves == Limit )
+    {
+        if ( !p->pParams->fTruth )
+        {
+            for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+            {
+                for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
+                    if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
+                        break;
+                if ( k == -1 ) // did not find
+                    return NULL;
+            }
+            pRes = Cut_CutAlloc( p );
+        }
+        else
+        {
+            uSign1 = 0;
+            for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+            {
+                for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
+                    if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
+                    {
+                        uSign1 |= (1 << i);
+                        break;
+                    }
+                if ( k == -1 ) // did not find
+                    return NULL;
+            }
+            pRes = Cut_CutAlloc( p );
+            pRes->uTruth = (uSign1 << 8);
+        }
+        for ( i = 0; i < (int)pCut0->nLeaves; i++ )
+            pRes->pLeaves[i] = pCut0->pLeaves[i];
+        pRes->nLeaves = pCut0->nLeaves;
+        return pRes;
+    }
+    // other cases
+    nNodes = pCut0->nLeaves;
+    for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+    {
+        for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
+        {
+            if ( pCut0->pLeaves[k] > pCut1->pLeaves[i] )
+                continue;
+            if ( pCut0->pLeaves[k] < pCut1->pLeaves[i] )
+            {
+                pRow = M[k+1];
+                if ( pRow[0] == 0 )
+                    pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
+                else if ( pRow[1] == 0 )
+                    pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
+                else if ( pRow[2] == 0 )
+                    pRow[2] = pCut1->pLeaves[i];
+                else 
+                    assert( 0 );
+                if ( ++nNodes > (int)Limit )
+                {
+                    for ( i = 0; i <= (int)pCut0->nLeaves; i++ )
+                        M[i][0] = 0;
+                    return NULL;
+                }
+            }
+            break;
+        }
+        if ( k == -1 )
+        {
+            pRow = M[0];
+            if ( pRow[0] == 0 )
+                pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
+            else if ( pRow[1] == 0 )
+                pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
+            else if ( pRow[2] == 0 )
+                pRow[2] = pCut1->pLeaves[i];
+            else 
+                assert( 0 );
+            if ( ++nNodes > (int)Limit )
+            {
+                for ( i = 0; i <= (int)pCut0->nLeaves; i++ )
+                    M[i][0] = 0;
+                return NULL;
+            }
+            continue;
+        }
+    }
+
+    pRes = Cut_CutAlloc( p );
+    if ( !p->pParams->fTruth )
+    {
+        for ( Count = 0, i = 0; i <= (int)pCut0->nLeaves; i++ )
+        {
+            if ( i > 0 )
+                pRes->pLeaves[Count++] = pCut0->pLeaves[i-1];
+            pRow = M[i];
+            if ( pRow[0] )
+            {
+                pRes->pLeaves[Count++] = pRow[0];
+                if ( pRow[1] )
+                {
+                    pRes->pLeaves[Count++] = pRow[1];
+                    if ( pRow[2] )
+                        pRes->pLeaves[Count++] = pRow[2];
+                }
+                pRow[0] = 0;
+            }
+        }
+        assert( Count == nNodes );
+        pRes->nLeaves = nNodes;
+/*
+    // make sure that the cut is correct
+    {
+        for ( i = 1; i < (int)pRes->nLeaves; i++ )
+            if ( pRes->pLeaves[i-1] >= pRes->pLeaves[i] )
+            {
+                int v = 0;
+            }
+    }
+*/
+        return pRes;
+    }
+
+    uSign0 = uSign1 = 0;
+    for ( Count = 0, i = 0; i <= (int)pCut0->nLeaves; i++ )
+    {
+        if ( i > 0 )
+        {
+            uSign0 |= (1 << Count);
+            pRes->pLeaves[Count++] = pCut1->pLeaves[i-1];
+        }
+        pRow = M[i];
+        if ( pRow[0] )
+        {
+            uSign1 |= (1 << Count);
+            pRes->pLeaves[Count++] = pRow[0];
+            if ( pRow[1] )
+            {
+                uSign1 |= (1 << Count);
+                pRes->pLeaves[Count++] = pRow[1];
+                if ( pRow[2] )
+                {
+                    uSign1 |= (1 << Count);
+                    pRes->pLeaves[Count++] = pRow[2];
+                }
+            }
+            pRow[0] = 0;
+        }
+    }
+    assert( Count == nNodes );
+    pRes->nLeaves = nNodes;
+    pRes->uTruth = (uSign1 << 8) | uSign0;
+    return pRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
new file mode 100644
index 00000000..6ce3b983
--- /dev/null
+++ b/src/opt/cut/cutNode.c
@@ -0,0 +1,623 @@
+/**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"
+#include "cutList.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        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.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
+{
+    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    [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 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts by merging cuts at two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 )
+{
+    Cut_List_t SuperList;
+    Cut_Cut_t * pList0, * pList1, * pStop0, * pStop1, * pTemp0, * pTemp1;
+    int i, Limit = p->pParams->nVarsMax;
+    int clk = clock();
+    assert( p->pParams->nVarsMax <= 6 );
+    // start the new list
+    Cut_ListStart( &SuperList );
+    // get the cut lists of children
+    pList0 = Cut_NodeReadCuts( p, Node0 );
+    pList1 = Cut_NodeReadCuts( p, Node1 );
+    assert( pList0 && pList1 );
+    // get the simultation bit of the node
+    p->fSimul = (fCompl0 ^ pList0->fSimul) & (fCompl1 ^ pList1->fSimul);
+    // set temporary variables
+    p->fCompl0 = fCompl0;
+    p->fCompl1 = fCompl1;
+    // find the point in the list where the max-var cuts begin
+    Cut_ListForEachCut( pList0, pStop0 )
+        if ( pStop0->nLeaves == (unsigned)Limit )
+            break;
+    Cut_ListForEachCut( pList1, pStop1 )
+        if ( pStop1->nLeaves == (unsigned)Limit )
+            break;
+    // start with the elementary cut
+    pTemp0 = Cut_CutCreateTriv( p, Node );
+    Cut_ListAdd( &SuperList, pTemp0 );
+    p->nCutsNode = 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 )
+    Cut_ListForEachCut( pStop1, pTemp1 )
+        if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
+            goto finish;
+    // all by large
+    Cut_ListForEachCut( pList1, pTemp1 )
+    Cut_ListForEachCut( pStop0, pTemp0 )
+        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 );
+        for ( i = 0; i < Limit; i++ )
+            if ( pTemp0->pLeaves[i] != pTemp1->pLeaves[i] )
+                break;
+        if ( i < Limit )
+            continue;
+        if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
+            goto finish;
+    }
+finish :
+    // set the list at the node
+    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 )
+    {
+        Cut_NodeTryDroppingCuts( p, Node0 );
+        Cut_NodeTryDroppingCuts( p, Node1 );
+    }
+p->timeMerge += clock() - clk;
+    // filter the cuts
+clk = clock();
+    if ( p->pParams->fFilter )
+        Cut_CutFilter( p, pList0 );
+p->timeFilter += clock() - clk;
+    return pList0;
+}
+
+/**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 []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
+{
+    Cut_List_t SuperList;
+    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 );
+
+    // remember the root node to save the resulting cuts
+    Root = Vec_IntEntry( vNodes, 0 );
+    p->nCutsNode = 1;
+
+    // collect small cuts first
+    Vec_PtrClear( p->vTemp );
+    Vec_IntForEachEntry( vNodes, Node, i )
+    {
+        // get the cuts of this node
+        pList = Cut_NodeReadCuts( p, Node );
+        Cut_NodeWriteCuts( p, Node, NULL );
+        assert( pList );
+        // remember the starting point
+        pListStart = pList->pNext;
+        // save or recycle the elementary cut
+        if ( i == 0 )
+            Cut_ListAdd( &SuperList, pList ), pTop = pList;
+        else
+            Cut_CutRecycle( p, pList );
+        // save all the cuts that are smaller than the limit
+        Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+        {
+            if ( pCut->nLeaves == (unsigned)Limit )
+            {
+                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 );
+                continue;
+            }
+            // set the complemented bit by comparing the first cut with the current cut
+            pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+            // add to the list
+            Cut_ListAdd( &SuperList, pCut );
+            if ( ++p->nCutsNode == p->pParams->nKeepMax )
+            {
+                // recycle the rest of the cuts of this node
+                Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
+                    Cut_CutRecycle( p, pCut );
+                // recycle all cuts of other nodes
+                Vec_IntForEachEntryStart( vNodes, Node, k, i+1 )
+                    Cut_NodeFreeCuts( p, Node );
+                // recycle the saved cuts of other nodes
+                Vec_PtrForEachEntry( p->vTemp, pList, k )
+                    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+                        Cut_CutRecycle( p, pCut );
+                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 );
+                continue;
+            }
+            // set the complemented bit
+            pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+            // add to the list
+            Cut_ListAdd( &SuperList, pCut );
+            if ( ++p->nCutsNode == p->pParams->nKeepMax )
+            {
+                // recycle the rest of the cuts
+                Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
+                    Cut_CutRecycle( p, pCut );
+                // recycle the saved cuts of other nodes
+                Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 )
+                    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+                        Cut_CutRecycle( p, pCut );
+                goto finish;
+            }
+        }
+    }
+finish :
+    // set the cuts at the node
+    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 );
+p->timeFilter += clock() - clk;
+    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 > 1 );
+    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/cutSeq.c b/src/opt/cut/cutSeq.c
new file mode 100644
index 00000000..869bd7b3
--- /dev/null
+++ b/src/opt/cut/cutSeq.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [cutSeq.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Sequential cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutTable.c b/src/opt/cut/cutTable.c
new file mode 100644
index 00000000..5dfaca7b
--- /dev/null
+++ b/src/opt/cut/cutTable.c
@@ -0,0 +1,253 @@
+/**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
new file mode 100644
index 00000000..efacd456
--- /dev/null
+++ b/src/opt/cut/cutTruth.c
@@ -0,0 +1,322 @@
+/**CFile****************************************************************
+
+  FileName    [cutTruth.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Incremental truth table computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutTruth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.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                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
+{
+    unsigned uPhase = 0;
+    int i, k;
+    for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
+    {
+        if ( k == (int)pCut1->nLeaves )
+            break;
+        if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
+            continue;
+        assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
+        uPhase |= (1 << i);
+        k++;
+    }
+    return uPhase;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  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 );
+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 )
+{
+    unsigned * puTruthCut0, * puTruthCut1;
+    unsigned uTruth0[2], uTruth1[2], uPhase;
+
+    puTruthCut0 = Cut_CutReadTruth(pCut0);
+    puTruthCut1 = Cut_CutReadTruth(pCut1);
+
+    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
+    {
+        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 );
+            }
+        }
+    }
+    uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
+
+    // assign the truth table
+    if ( pCut1->nLeaves == pCut->nLeaves )
+        uTruth0 = *Cut_CutReadTruth(pCut1);
+    else
+    {
+        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 );
+            }
+        }
+    }
+    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;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/module.make b/src/opt/cut/module.make
new file mode 100644
index 00000000..1175b3f2
--- /dev/null
+++ b/src/opt/cut/module.make
@@ -0,0 +1,6 @@
+SRC +=  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