Version abc60723

13 files changed, 2779 insertions, 991 deletions

diff --git a/src/opt/cut/Abc_NtkFindCi.c b/src/opt/cut/Abc_NtkFindCi.c
deleted file mode 100644
index 203f9e6f..00000000
--- a/src/opt/cut/Abc_NtkFindCi.c
+++ /dev/null
@@ -1,988 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cutPre22.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Precomputes truth tables for the 2x2 macro cell.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cutPre22.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cutInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define CUT_CELL_MVAR  9
-
-typedef struct Cut_Cell_t_ Cut_Cell_t;
-typedef struct Cut_CMan_t_ Cut_CMan_t;
-
-struct Cut_Cell_t_
-{
-    Cut_Cell_t *       pNext;                        // pointer to the next cell in the table
-    Cut_Cell_t *       pNextVar;                     // pointer to the next cell of this support size
-    Cut_Cell_t *       pParent;                      // pointer to the cell used to derive this one
-    int                nUsed;                        // the number of times the cell is used
-    char               Box[4];                       // functions in the boxes
-    unsigned           nVars          :  4;          // the number of variables
-    unsigned           CrossBar0      :  4;          // the variable set equal
-    unsigned           CrossBar1      :  4;          // the variable set equal
-    unsigned           CrossBarPhase  :  2;          // the phase of the cross bar (0, 1, or 2)
-    unsigned           CanonPhase     : 18;          // the canonical phase
-    char               CanonPerm[CUT_CELL_MVAR+3];   // semicanonical permutation
-    short              Store[2*CUT_CELL_MVAR];       // minterm counts in the cofactors
-    unsigned           uTruth[1<<(CUT_CELL_MVAR-5)]; // the current truth table
-};
-
-struct Cut_CMan_t_
-{
-    // storage for canonical cells
-    Extra_MmFixed_t *  pMem;
-    st_table *         tTable;
-    Cut_Cell_t *       pSameVar[CUT_CELL_MVAR+1];
-    // elementary truth tables
-    unsigned           uInputs[CUT_CELL_MVAR][1<<(CUT_CELL_MVAR-5)];
-    // temporary truth tables
-    unsigned           uTemp1[22][1<<(CUT_CELL_MVAR-5)];
-    unsigned           uTemp2[22][1<<(CUT_CELL_MVAR-5)];
-    unsigned           uTemp3[22][1<<(CUT_CELL_MVAR-5)];
-    unsigned           uFinal[1<<(CUT_CELL_MVAR-5)];
-    unsigned           puAux[1<<(CUT_CELL_MVAR-5)];
-    // statistical variables
-    int                nTotal;
-    int                nGood;
-    int                nVarCounts[CUT_CELL_MVAR+1];
-    int                nSymGroups[CUT_CELL_MVAR+1];
-    int                nSymGroupsE[CUT_CELL_MVAR+1];
-    int                timeCanon;
-    int                timeSupp;
-    int                timeTable;
-    int                nCellFound;
-    int                nCellNotFound;
-};
-
-// NP-classes of functions of 3 variables (22)
-static char * s_NP3[22] = {
-    " 0\n",                          // 00    const 0            // 0 vars 
-    " 1\n",                          // 01    const 1            // 0 vars  
-    "1 1\n",                         // 02    a                  // 1 vars  
-    "11 1\n",                        // 03    ab                 // 2 vars  
-    "11 0\n",                        // 04    (ab)'              // 2 vars  
-    "10 1\n01 1\n",                  // 05    a<+>b              // 2 vars  
-    "111 1\n",                       // 06 0s abc                // 3 vars  
-    "111 0\n",                       // 07    (abc)'             // 
-    "11- 1\n1-1 1\n",                // 08 1p a(b+c)             // 
-    "11- 0\n1-1 0\n",                // 09    (a(b+c))'          // 
-    "111 1\n100 1\n010 1\n001 1\n",  // 10 2s a<+>b<+>c          // 
-    "10- 0\n1-0 0\n011 0\n",         // 11 3p a<+>bc             // 
-    "101 1\n110 1\n",                // 12 4p a(b<+>c)           // 
-    "101 0\n110 0\n",                // 13    (a(b<+>c))'        // 
-    "11- 1\n1-1 1\n-11 1\n",         // 14 5s ab+bc+ac           // 
-    "111 1\n000 1\n",                // 15 6s abc+a'b'c'         // 
-    "111 0\n000 0\n",                // 16    (abc+a'b'c')'      // 
-    "11- 1\n-11 1\n0-1 1\n",         // 17 7  ab+bc+a'c          // 
-    "011 1\n101 1\n110 1\n",         // 18 8s a'bc+ab'c+abc'     // 
-    "011 0\n101 0\n110 0\n",         // 19    (a'bc+ab'c+abc')'  // 
-    "100 1\n-11 1\n",                // 20 9p ab'c'+bc           // 
-    "100 0\n-11 0\n"                 // 21    (ab'c'+bc)'        // 
-};
-
-// NP-classes of functions of 3 variables (22)
-static char * s_NP3Names[22] = {
-    "   const 0            ",
-    "   const 1            ",
-    "   a                  ",
-    "   ab                 ",
-    "   (ab)'              ",
-    "   a<+>b              ",
-    "0s abc                ",
-    "   (abc)'             ",
-    "1p a(b+c)             ",
-    "   (a(b+c))'          ",
-    "2s a<+>b<+>c          ",
-    "3p a<+>bc             ",
-    "4p a(b<+>c)           ",
-    "   (a(b<+>c))'        ",
-    "5s ab+bc+ac           ",
-    "6s abc+a'b'c'         ",
-    "   (abc+a'b'c')'      ",
-    "7  ab+bc+a'c          ",
-    "8s a'bc+ab'c+abc'     ",
-    "   (a'bc+ab'c+abc')'  ",
-    "9p ab'c'+bc           ",
-    "   (ab'c'+bc)'        "
-};
-
-// the number of variables in each function
-static int s_NP3VarNums[22] = { 0, 0, 1, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3 };
-
-// NPN classes of functions of exactly 3 inputs (10)
-static int s_NPNe3[10] = { 6, 8, 10, 11, 12, 14, 15, 17, 18, 20 };
-
-// NPN classes of functions of exactly 3 inputs that are symmetric (5)
-static int s_NPNe3s[10] = { 6, 10, 14, 15, 18 };
-
-// NPN classes of functions of exactly 3 inputs (4)
-static int s_NPNe3p[10] = { 8, 11, 12, 20 };
-
-static Cut_CMan_t * Cut_CManStart();
-static void Cut_CManStop( Cut_CMan_t * p );
-static void Cut_CellTruthElem( unsigned * InA, unsigned * InB, unsigned * InC, unsigned * pOut, int nVars, int Type );
-static void Cut_CellCanonicize( Cut_CMan_t * p, Cut_Cell_t * pCell );
-static int  Cut_CellTableLookup( Cut_CMan_t * p, Cut_Cell_t * pCell );
-static void Cut_CellSuppMin( Cut_Cell_t * pCell );
-static void Cut_CellCrossBar( Cut_Cell_t * pCell );
-
-
-static Cut_CMan_t * s_pCMan = NULL;
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Start the precomputation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CellLoad()
-{
-    FILE * pFile;
-    char * pFileName = "cells22_daomap_iwls.txt";
-    char pString[1000];
-    Cut_CMan_t * p;
-    Cut_Cell_t * pCell;
-    int Length; //, i;
-    pFile = fopen( pFileName, "r" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open file \"%s\".\n", pFileName );
-        return;
-    }
-   // start the manager
-    p = Cut_CManStart();
-    // load truth tables
-    while ( fgets(pString, 1000, pFile) )
-    {
-        Length = strlen(pString);
-        pString[Length--] = 0;
-        if ( Length == 0 )
-            continue;
-        // derive the cell
-        pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
-        memset( pCell, 0, sizeof(Cut_Cell_t) );
-        pCell->nVars = Extra_Base2Log(Length*4);
-        pCell->nUsed = 1;
-//        Extra_TruthCopy( pCell->uTruth, pTruth, nVars );
-        Extra_ReadHexadecimal( pCell->uTruth, pString, pCell->nVars );
-        Cut_CellSuppMin( pCell );
-/*
-        // set the elementary permutation
-        for ( i = 0; i < (int)pCell->nVars; i++ )
-            pCell->CanonPerm[i] = i;
-        // canonicize
-        pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
-*/
-        // add to the table
-        p->nTotal++;
-
-//        Extra_PrintHexadecimal( stdout, pCell->uTruth, pCell->nVars ); printf( "\n" );
-//        if ( p->nTotal == 500 )
-//            break;
-
-        if ( !Cut_CellTableLookup( p, pCell ) ) // new cell
-            p->nGood++;
-    }
-    printf( "Read %d cells from file \"%s\". Added %d cells to the table.\n", p->nTotal, pFileName, p->nGood );
-    fclose( pFile );
-//    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Precomputes truth tables for the 2x2 macro cell.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CellPrecompute()
-{
-    Cut_CMan_t * p;
-    Cut_Cell_t * pCell, * pTemp;
-    int i1, i2, i3, i, j, k, c, clk = clock(), clk2 = clock();
-
-    p = Cut_CManStart();
-
-    // precompute truth tables
-    for ( i = 0; i < 22; i++ )
-        Cut_CellTruthElem( p->uInputs[0], p->uInputs[1], p->uInputs[2], p->uTemp1[i], 9, i );
-    for ( i = 0; i < 22; i++ )
-        Cut_CellTruthElem( p->uInputs[3], p->uInputs[4], p->uInputs[5], p->uTemp2[i], 9, i );
-    for ( i = 0; i < 22; i++ )
-        Cut_CellTruthElem( p->uInputs[6], p->uInputs[7], p->uInputs[8], p->uTemp3[i], 9, i );
-/*
-        if ( k == 8 && ((i1 == 6 && i2 == 14 && i3 == 20) || (i1 == 20 && i2 == 6 && i3 == 14)) )
-        {
-            Extra_PrintBinary( stdout, &pCell->CanonPhase, pCell->nVars+1 ); printf( " : " );
-            for ( i = 0; i < pCell->nVars; i++ )
-                printf( "%d=%d/%d  ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
-            Extra_PrintHexadecimal( stdout, pCell->uTruth, pCell->nVars );
-            printf( "\n" );
-        }
-*/
-/*
-    // go through symmetric roots
-    for ( k = 0; k < 5; k++ )
-    for ( i1 =  0; i1 < 22; i1++ )
-    for ( i2 = i1; i2 < 22; i2++ )
-    for ( i3 = i2; i3 < 22; i3++ )
-    {
-        // derive the cell
-        pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
-        memset( pCell, 0, sizeof(Cut_Cell_t) );
-        pCell->nVars  = 9;
-        pCell->Box[0] = s_NPNe3s[k];
-        pCell->Box[1] = i1;
-        pCell->Box[2] = i2;
-        pCell->Box[3] = i3;
-        // fill in the truth table
-        Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3s[k] );
-        // canonicize
-        Cut_CellCanonicize( pCell );
-
-        // add to the table
-        p->nTotal++;
-        if ( Cut_CellTableLookup( p, pCell ) ) // already exists
-            Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
-        else
-            p->nGood++;
-    }
-
-    // go through partially symmetric roots
-    for ( k = 0; k < 4; k++ )
-    for ( i1 = 0;  i1 < 22; i1++ )
-    for ( i2 = 0;  i2 < 22; i2++ )
-    for ( i3 = i2; i3 < 22; i3++ )
-    {
-        // derive the cell
-        pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
-        memset( pCell, 0, sizeof(Cut_Cell_t) );
-        pCell->nVars  = 9;
-        pCell->Box[0] = s_NPNe3p[k];
-        pCell->Box[1] = i1;
-        pCell->Box[2] = i2;
-        pCell->Box[3] = i3;
-        // fill in the truth table
-        Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3p[k] );
-        // canonicize
-        Cut_CellCanonicize( pCell );
-
-        // add to the table
-        p->nTotal++;
-        if ( Cut_CellTableLookup( p, pCell ) ) // already exists
-            Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
-        else
-            p->nGood++;
-    }
-
-    // go through non-symmetric functions
-    for ( i1 = 0; i1 < 22; i1++ )
-    for ( i2 = 0; i2 < 22; i2++ )
-    for ( i3 = 0; i3 < 22; i3++ )
-    {
-        // derive the cell
-        pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
-        memset( pCell, 0, sizeof(Cut_Cell_t) );
-        pCell->nVars  = 9;
-        pCell->Box[0] = 17;
-        pCell->Box[1] = i1;
-        pCell->Box[2] = i2;
-        pCell->Box[3] = i3;
-        // fill in the truth table
-        Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, 17 );
-        // canonicize
-        Cut_CellCanonicize( pCell );
-
-        // add to the table
-        p->nTotal++;
-        if ( Cut_CellTableLookup( p, pCell ) ) // already exists
-            Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
-        else
-            p->nGood++;
-    }
-*/
-
-    // go through non-symmetric functions
-    for ( k = 0; k < 10; k++ )
-    for ( i1 = 0; i1 < 22; i1++ )
-    for ( i2 = 0; i2 < 22; i2++ )
-    for ( i3 = 0; i3 < 22; i3++ )
-    {
-        // derive the cell
-        pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
-        memset( pCell, 0, sizeof(Cut_Cell_t) );
-        pCell->nVars  = 9;
-        pCell->Box[0] = s_NPNe3[k];
-        pCell->Box[1] = i1;
-        pCell->Box[2] = i2;
-        pCell->Box[3] = i3;
-        // set the elementary permutation
-        for ( i = 0; i < (int)pCell->nVars; i++ )
-            pCell->CanonPerm[i] = i;
-        // fill in the truth table
-        Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3[k] );
-        // minimize the support
-        Cut_CellSuppMin( pCell );
-
-        // canonicize
-        pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
-
-        // add to the table
-        p->nTotal++;
-        if ( Cut_CellTableLookup( p, pCell ) ) // already exists
-            Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
-        else
-        {
-            p->nGood++;
-            p->nVarCounts[pCell->nVars]++;
-
-            if ( pCell->nVars )
-            for ( i = 0; i < (int)pCell->nVars-1; i++ )
-            {
-                if ( pCell->Store[2*i] != pCell->Store[2*(i+1)] ) // i and i+1 cannot be symmetric
-                    continue;
-                // i and i+1 can be symmetric
-                // find the end of this group
-                for ( j = i+1; j < (int)pCell->nVars; j++ )
-                    if ( pCell->Store[2*i] != pCell->Store[2*j] ) 
-                        break;
-
-                if ( pCell->Store[2*i] == pCell->Store[2*i+1] )
-                    p->nSymGroupsE[j-i]++;
-                else
-                    p->nSymGroups[j-i]++;
-                i = j - 1;
-            }
-/*
-            if ( pCell->nVars == 3 )
-            {
-                Extra_PrintBinary( stdout, pCell->uTruth, 32 ); printf( "\n" );
-                for ( i = 0; i < (int)pCell->nVars; i++ )
-                    printf( "%d=%d/%d  ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
-                printf( "\n" );
-            }
-*/
-        }
-    }
-
-    printf( "BASIC: Total = %d. Good = %d. Entry = %d. ", p->nTotal, p->nGood, sizeof(Cut_Cell_t) );
-    PRT( "Time", clock() - clk );
-    printf( "Cells:  " );
-    for ( i = 0; i <= 9; i++ )
-        printf( "%d=%d ", i, p->nVarCounts[i] );
-    printf( "\nDiffs:  " );
-    for ( i = 0; i <= 9; i++ )
-        printf( "%d=%d ", i, p->nSymGroups[i] );
-    printf( "\nEquals: " );
-    for ( i = 0; i <= 9; i++ )
-        printf( "%d=%d ", i, p->nSymGroupsE[i] );
-    printf( "\n" );
-
-    // continue adding new cells using support
-    for ( k = CUT_CELL_MVAR; k > 3; k-- )
-    {
-        for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
-        for ( i1 = 0; i1 < k; i1++ )
-        for ( i2 = i1+1; i2 < k; i2++ )
-        for ( c = 0; c < 3; c++ )
-        {
-            // derive the cell
-            pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
-            memset( pCell, 0, sizeof(Cut_Cell_t) );
-            pCell->nVars   = pTemp->nVars;
-            pCell->pParent = pTemp;
-            // set the elementary permutation
-            for ( i = 0; i < (int)pCell->nVars; i++ )
-                pCell->CanonPerm[i] = i;
-            // fill in the truth table
-            Extra_TruthCopy( pCell->uTruth, pTemp->uTruth, pTemp->nVars );
-            // create the cross-bar
-            pCell->CrossBar0 = i1;
-            pCell->CrossBar1 = i2;
-            pCell->CrossBarPhase = c;
-            Cut_CellCrossBar( pCell );
-            // minimize the support
-//clk2 = clock();
-            Cut_CellSuppMin( pCell );
-//p->timeSupp += clock() - clk2;
-            // canonicize
-//clk2 = clock();
-            pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
-//p->timeCanon += clock() - clk2;
-
-            // add to the table
-//clk2 = clock();
-            p->nTotal++;
-            if ( Cut_CellTableLookup( p, pCell ) ) // already exists
-                Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
-            else
-            {
-                p->nGood++;
-                p->nVarCounts[pCell->nVars]++;
-
-                for ( i = 0; i < (int)pCell->nVars-1; i++ )
-                {
-                    if ( pCell->Store[2*i] != pCell->Store[2*(i+1)] ) // i and i+1 cannot be symmetric
-                        continue;
-                    // i and i+1 can be symmetric
-                    // find the end of this group
-                    for ( j = i+1; j < (int)pCell->nVars; j++ )
-                        if ( pCell->Store[2*i] != pCell->Store[2*j] ) 
-                            break;
-
-                    if ( pCell->Store[2*i] == pCell->Store[2*i+1] )
-                        p->nSymGroupsE[j-i]++;
-                    else
-                        p->nSymGroups[j-i]++;
-                    i = j - 1;
-                }
-/*
-                if ( pCell->nVars == 3 )
-                {
-                    Extra_PrintBinary( stdout, pCell->uTruth, 32 ); printf( "\n" );
-                    for ( i = 0; i < (int)pCell->nVars; i++ )
-                        printf( "%d=%d/%d  ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
-                    printf( "\n" );
-                }
-*/
-            }
-//p->timeTable += clock() - clk2;
-        }
-
-        printf( "VAR %d: Total = %d. Good = %d. Entry = %d. ", k, p->nTotal, p->nGood, sizeof(Cut_Cell_t) );
-        PRT( "Time", clock() - clk );
-        printf( "Cells:  " );
-        for ( i = 0; i <= 9; i++ )
-            printf( "%d=%d ", i, p->nVarCounts[i] );
-        printf( "\nDiffs:  " );
-        for ( i = 0; i <= 9; i++ )
-            printf( "%d=%d ", i, p->nSymGroups[i] );
-        printf( "\nEquals: " );
-        for ( i = 0; i <= 9; i++ )
-            printf( "%d=%d ", i, p->nSymGroupsE[i] );
-        printf( "\n" );
-    }
-//    printf( "\n" );
-    PRT( "Supp ", p->timeSupp );
-    PRT( "Canon", p->timeCanon );
-    PRT( "Table", p->timeTable );
-//    Cut_CManStop( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Check the table.]
-
-  Description [Returns 1 if such a truth table already exists.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_CellTableLookup( Cut_CMan_t * p, Cut_Cell_t * pCell )
-{
-    Cut_Cell_t ** pSlot, * pTemp;
-    unsigned Hash;
-    Hash = Extra_TruthHash( pCell->uTruth, Extra_TruthWordNum( pCell->nVars ) );
-    if ( !st_find_or_add( p->tTable, (char *)Hash, (char ***)&pSlot ) )
-        *pSlot = NULL;
-    for ( pTemp = *pSlot; pTemp; pTemp = pTemp->pNext )
-    {
-        if ( pTemp->nVars != pCell->nVars )
-            continue;
-        if ( Extra_TruthIsEqual(pTemp->uTruth, pCell->uTruth, pCell->nVars) )
-            return 1;
-    }
-    // the entry is new
-    pCell->pNext = *pSlot;
-    *pSlot = pCell;
-    // add it to the variable support list
-    pCell->pNextVar = p->pSameVar[pCell->nVars];
-    p->pSameVar[pCell->nVars] = pCell;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CellSuppMin( Cut_Cell_t * pCell )
-{
-    static unsigned uTemp[1<<(CUT_CELL_MVAR-5)];
-    unsigned * pIn, * pOut, * pTemp;
-    int i, k, Counter, Temp;
-
-    // go backward through the support variables and remove redundant
-    for ( k = pCell->nVars - 1; k >= 0; k-- )
-        if ( !Extra_TruthVarInSupport(pCell->uTruth, pCell->nVars, k) )
-        {
-            // shift all the variables above this one
-            Counter = 0;
-            pIn = pCell->uTruth; pOut = uTemp;
-            for ( i = k; i < (int)pCell->nVars - 1; i++ )
-            {
-                Extra_TruthSwapAdjacentVars( pOut, pIn, pCell->nVars, i );
-                pTemp = pIn; pIn = pOut; pOut = pTemp;
-                // swap the support vars
-                Temp = pCell->CanonPerm[i]; 
-                pCell->CanonPerm[i] = pCell->CanonPerm[i+1];
-                pCell->CanonPerm[i+1] = Temp;
-                Counter++;
-            }
-            // return the function back into its place
-            if ( Counter & 1 )
-                Extra_TruthCopy( pOut, pIn, pCell->nVars );
-            // remove one variable
-            pCell->nVars--;
-//            Extra_PrintBinary( stdout, pCell->uTruth, (1<<pCell->nVars) ); printf( "\n" );
-        }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CellCrossBar( Cut_Cell_t * pCell )
-{
-    static unsigned uTemp0[1<<(CUT_CELL_MVAR-5)];
-    static unsigned uTemp1[1<<(CUT_CELL_MVAR-5)];
-    Extra_TruthCopy( uTemp0, pCell->uTruth, pCell->nVars );
-    Extra_TruthCopy( uTemp1, pCell->uTruth, pCell->nVars );
-    if ( pCell->CanonPhase == 0 )
-    {
-        Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar0 );
-        Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar1 );
-        Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar0 );
-        Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar1 );
-    }
-    else if ( pCell->CanonPhase == 1 )
-    {
-        Extra_TruthCofactor1( uTemp0, pCell->nVars, pCell->CrossBar0 );
-        Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar1 );
-        Extra_TruthCofactor0( uTemp1, pCell->nVars, pCell->CrossBar0 );
-        Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar1 );
-    }
-    else if ( pCell->CanonPhase == 2 )
-    {
-        Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar0 );
-        Extra_TruthCofactor1( uTemp0, pCell->nVars, pCell->CrossBar1 );
-        Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar0 );
-        Extra_TruthCofactor0( uTemp1, pCell->nVars, pCell->CrossBar1 );
-    }
-    else assert( 0 );
-    Extra_TruthCombine( pCell->uTruth, uTemp0, uTemp1, pCell->nVars, pCell->CrossBar0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CellTruthElem( unsigned * InA, unsigned * InB, unsigned * InC, unsigned * pOut, int nVars, int Type )
-{
-    int nWords = Extra_TruthWordNum( nVars );
-    int i;
-
-    assert( Type < 22 );
-    switch ( Type )
-    {
-    // " 0\n",                         // 00   const 0
-    case 0:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = 0;
-        return;
-    // " 1\n",                         // 01   const 1
-    case 1:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = 0xFFFFFFFF;
-        return;
-    // "1 1\n",                        // 02   a
-    case 2:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = InA[i];
-        return;
-    // "11 1\n",                       // 03   ab
-    case 3:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = InA[i] & InB[i];
-        return;
-    // "11 0\n",                       // 04   (ab)'
-    case 4:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = ~(InA[i] & InB[i]);
-        return;
-    // "10 1\n01 1\n",                 // 05   a<+>b
-    case 5:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = InA[i] ^ InB[i];
-        return;
-    // "111 1\n",                      // 06 + abc
-    case 6:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = InA[i] & InB[i] & InC[i];
-        return;
-    // "111 0\n",                      // 07   (abc)'
-    case 7:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = ~(InA[i] & InB[i] & InC[i]);
-        return;
-    // "11- 1\n1-1 1\n",               // 08 + a(b+c)
-    case 8:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = InA[i] & (InB[i] | InC[i]);
-        return;
-    // "11- 0\n1-1 0\n",               // 09   (a(b+c))'
-    case 9:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = ~(InA[i] & (InB[i] | InC[i]));
-        return;
-    // "111 1\n100 1\n010 1\n001 1\n", // 10 + a<+>b<+>c
-    case 10:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = InA[i] ^ InB[i] ^ InC[i];
-        return;
-    // "10- 0\n1-0 0\n011 0\n",        // 11 + a<+>bc
-    case 11:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = InA[i] ^ (InB[i] & InC[i]);
-        return;
-    // "101 1\n110 1\n",               // 12 + a(b<+>c)
-    case 12:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = InA[i] & (InB[i] ^ InC[i]);
-        return;
-    // "101 0\n110 0\n",               // 13   (a(b<+>c))'
-    case 13:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = ~(InA[i] & (InB[i] ^ InC[i]));
-        return;
-    // "11- 1\n1-1 1\n-11 1\n",        // 14 + ab+bc+ac
-    case 14:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = (InA[i] & InB[i]) | (InB[i] & InC[i]) | (InA[i] & InC[i]);
-        return;
-    // "111 1\n000 1\n",               // 15 + abc+a'b'c'
-    case 15:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = (InA[i] & InB[i] & InC[i]) | (~InA[i] & ~InB[i] & ~InC[i]);
-        return;
-    // "111 0\n000 0\n",               // 16   (abc+a'b'c')'
-    case 16:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = ~((InA[i] & InB[i] & InC[i]) | (~InA[i] & ~InB[i] & ~InC[i]));
-        return;
-    // "11- 1\n-11 1\n0-1 1\n",        // 17 + ab+bc+a'c
-    case 17:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = (InA[i] & InB[i]) | (InB[i] & InC[i]) | (~InA[i] & InC[i]);
-        return;
-    // "011 1\n101 1\n110 1\n",        // 18 + a'bc+ab'c+abc'
-    case 18:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = (~InA[i] & InB[i] & InC[i]) | (InA[i] & ~InB[i] & InC[i]) | (InA[i] & InB[i] & ~InC[i]);
-        return;
-    // "011 0\n101 0\n110 0\n",        // 19   (a'bc+ab'c+abc')'
-    case 19:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = ~((~InA[i] & InB[i] & InC[i]) | (InA[i] & ~InB[i] & InC[i]) | (InA[i] & InB[i] & ~InC[i]));
-        return;
-    // "100 1\n-11 1\n",               // 20 + ab'c'+bc
-    case 20:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = (InA[i] & ~InB[i] & ~InC[i]) | (InB[i] & InC[i]);
-        return;
-    // "100 0\n-11 0\n"                // 21   (ab'c'+bc)'
-    case 21:
-        for ( i = 0; i < nWords; i++ )
-            pOut[i] = ~((InA[i] & ~InB[i] & ~InC[i]) | (InB[i] & InC[i]));
-        return;
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Start the precomputation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cut_CMan_t * Cut_CManStart()
-{
-    Cut_CMan_t * p;
-    int i, k;
-    // start the manager
-    assert( sizeof(unsigned) == 4 );
-    p = ALLOC( Cut_CMan_t, 1 );
-    memset( p, 0, sizeof(Cut_CMan_t) );
-    // start the table and the memory manager
-    p->tTable = st_init_table(st_ptrcmp,st_ptrhash);
-    p->pMem = Extra_MmFixedStart( sizeof(Cut_Cell_t) );
-    // set elementary truth tables
-    for ( k = 0; k < CUT_CELL_MVAR; k++ )
-        for ( i = 0; i < (1<<CUT_CELL_MVAR); i++ )
-            if ( i & (1 << k) )
-                p->uInputs[k][i>>5] |= (1 << (i&31));
-    s_pCMan = p;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CManStop( Cut_CMan_t * p )
-{
-    st_free_table( p->tTable );
-    Extra_MmFixedStop( p->pMem, 0 );
-    free( p );
-}
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_CellIsRunning()
-{
-    return s_pCMan != NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cut_CellDumpToFile()
-{
-    FILE * pFile;
-    Cut_CMan_t * p = s_pCMan;
-    Cut_Cell_t * pTemp;
-    char * pFileName = "celllib22.txt";
-    int NumUsed[10][5] = {{0}};
-    int BoxUsed[22][5] = {{0}};
-    int i, k, Counter;
-    int clk = clock();
-
-    if ( p == NULL )
-    {
-        printf( "Cut_CellDumpToFile: Cell manager is not defined.\n" );
-        return;
-    }
-
-    // count the number of cells used
-    for ( k = CUT_CELL_MVAR; k >= 0; k-- )
-    {
-        for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
-        {
-            if ( pTemp->nUsed == 0 )
-                NumUsed[k][0]++;
-            else if ( pTemp->nUsed < 10 )
-                NumUsed[k][1]++;
-            else if ( pTemp->nUsed < 100 )
-                NumUsed[k][2]++;
-            else if ( pTemp->nUsed < 1000 )
-                NumUsed[k][3]++;
-            else 
-                NumUsed[k][4]++;
-
-            for ( i = 0; i < 4; i++ )
-                if ( pTemp->nUsed == 0 )
-                    BoxUsed[ pTemp->Box[i] ][0]++;
-                else if ( pTemp->nUsed < 10 )
-                    BoxUsed[ pTemp->Box[i] ][1]++;
-                else if ( pTemp->nUsed < 100 )
-                    BoxUsed[ pTemp->Box[i] ][2]++;
-                else if ( pTemp->nUsed < 1000 )
-                    BoxUsed[ pTemp->Box[i] ][3]++;
-                else 
-                    BoxUsed[ pTemp->Box[i] ][4]++;
-        }
-    }
-
-    printf( "Functions found = %10d.  Functions not found = %10d.\n", p->nCellFound, p->nCellNotFound );
-    for ( k = 0; k <= CUT_CELL_MVAR; k++ )
-    {
-        printf( "%3d  : ", k );
-        for ( i = 0; i < 5; i++ ) 
-            printf( "%8d ", NumUsed[k][i] );
-        printf( "\n" );
-    }
-    printf( "Box usage:\n" );
-    for ( k = 0; k < 22; k++ )
-    {
-        printf( "%3d  : ", k );
-        for ( i = 0; i < 5; i++ ) 
-            printf( "%8d ", BoxUsed[k][i] );
-        printf( "  %s", s_NP3Names[k] );
-        printf( "\n" );
-    }
-
-    pFile = fopen( pFileName, "w" );
-    if ( pFile == NULL )
-    {
-        printf( "Cut_CellDumpToFile: Cannout open output file.\n" );
-        return;
-    }
-
-    Counter = 0;
-    for ( k = 0; k <= CUT_CELL_MVAR; k++ )
-    {
-        for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
-            if ( pTemp->nUsed > 0 )
-            {
-                Extra_PrintHexadecimal( pFile, pTemp->uTruth, (k <= 5? 5 : k) );
-                fprintf( pFile, "\n" );
-                Counter++;
-            }
-        fprintf( pFile, "\n" );
-    }
-    fclose( pFile );
-
-    printf( "Library composed of %d functions is written into file \"%s\".  ", Counter, pFileName );
-
-    PRT( "Time", clock() - clk );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Looks up if the given function exists in the hash table.]
-
-  Description [If the function exists, returns 1, meaning that it can be
-  implemented using two levels of 3-input LUTs. If the function does not 
-  exist, return 0.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cut_CellTruthLookup( unsigned * pTruth, int nVars )
-{
-    Cut_CMan_t * p = s_pCMan;
-    Cut_Cell_t * pTemp;
-    Cut_Cell_t Cell, * pCell = &Cell;
-    unsigned Hash;
-    int i;
-
-    // cell manager is not defined
-    if ( p == NULL )
-    {
-        printf( "Cut_CellTruthLookup: Cell manager is not defined.\n" );
-        return 0;
-    }
-
-    // canonicize
-    memset( pCell, 0, sizeof(Cut_Cell_t) );
-    pCell->nVars = nVars;
-    Extra_TruthCopy( pCell->uTruth, pTruth, nVars );
-    Cut_CellSuppMin( pCell );
-    // set the elementary permutation
-    for ( i = 0; i < (int)pCell->nVars; i++ )
-        pCell->CanonPerm[i] = i;
-    // canonicize
-    pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
-
-
-    // check if the cell exists
-    Hash = Extra_TruthHash( pCell->uTruth, Extra_TruthWordNum(pCell->nVars) );
-    if ( st_lookup( p->tTable, (char *)Hash, (char **)&pTemp ) )
-    {
-        for ( ; pTemp; pTemp = pTemp->pNext )
-        {
-            if ( pTemp->nVars != pCell->nVars )
-                continue;
-            if ( Extra_TruthIsEqual(pTemp->uTruth, pCell->uTruth, pCell->nVars) )
-            {
-                pTemp->nUsed++;
-                p->nCellFound++;
-                return 1;
-            }
-        }
-    }
-    p->nCellNotFound++;
-    return 0;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/cut/abcCut.c b/src/opt/cut/abcCut.c
new file mode 100644
index 00000000..b4b879a3
--- /dev/null
+++ b/src/opt/cut/abcCut.c
@@ -0,0 +1,491 @@
+/**CFile****************************************************************
+
+  FileName    [abcCut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface to cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "cut.h"
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq );
+static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq );
+
+
+extern int nTotal, nGood, nEqual;
+
+// temporary
+//Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) { return NULL; }
+Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) 
+{
+    Vec_Int_t * vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 );
+    int i;
+    Abc_Obj_t * pObj;
+
+//    Abc_NtkForEachCi( pNtk, pObj, i )
+//        Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+//        if ( Abc_ObjIsNode(pObj) && (rand() % 4 == 0) )
+        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj) && (rand() % 3 == 0) )
+            Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+    }
+    return vAttrs; 
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
+{
+    ProgressBar * pProgress;
+    Cut_Man_t *  p;
+    Abc_Obj_t * pObj, * pNode;
+    Vec_Ptr_t * vNodes;
+    Vec_Int_t * vChoices;
+    int i;
+    int clk = clock();
+
+    extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
+
+    nTotal = nGood = nEqual = 0;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    // start the manager
+    pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
+    p = Cut_ManStart( pParams );
+    // compute node attributes if local or global cuts are requested
+    if ( pParams->fGlobal || pParams->fLocal )
+    {
+        extern Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk );
+        Cut_ManSetNodeAttrs( p, Abc_NtkGetNodeAttributes(pNtk) );
+    }
+    // prepare for cut dropping
+    if ( pParams->fDrop )
+        Cut_ManSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) );
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_NodeSetTriv( p, pObj->Id );
+    // compute cuts for internal nodes
+    vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs
+    vChoices = Vec_IntAlloc( 100 );
+    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // when we reached a CO, it is time to deallocate the cuts
+        if ( Abc_ObjIsCo(pObj) )
+        {
+            if ( pParams->fDrop )
+                Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            continue;
+        }
+        // skip constant node, it has no cuts
+        if ( Abc_NodeIsConst(pObj) )
+            continue;
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // compute the cuts to the internal node
+        Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree );  
+        // consider dropping the fanins cuts
+        if ( pParams->fDrop )
+        {
+            Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId1(pObj) );
+        }
+        // add cuts due to choices
+        if ( Abc_NodeIsAigChoice(pObj) )
+        {
+            Vec_IntClear( vChoices );
+            for ( pNode = pObj; pNode; pNode = pNode->pData )
+                Vec_IntPush( vChoices, pNode->Id );
+            Cut_NodeUnionCuts( p, vChoices );
+        }
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
+    Vec_IntFree( vChoices );
+PRT( "Total", clock() - clk );
+//Abc_NtkPrintCuts( p, pNtk, 0 );
+//    Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
+
+    // temporary printout of stats
+    if ( nTotal )
+    printf( "Total cuts = %d. Good cuts = %d.  Ratio = %5.2f\n", nTotal, nGood, ((double)nGood)/nTotal );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cut computation using the oracle.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
+{
+    Abc_Obj_t * pObj;
+    Vec_Ptr_t * vNodes;
+    int i, clk = clock();
+    int fDrop = Cut_OracleReadDrop(p);
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // prepare cut droppping
+    if ( fDrop )
+        Cut_OracleSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) );
+
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_OracleNodeSetTriv( p, pObj->Id );
+
+    // compute cuts for internal nodes
+    vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // when we reached a CO, it is time to deallocate the cuts
+        if ( Abc_ObjIsCo(pObj) )
+        {
+            if ( fDrop )
+                Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            continue;
+        }
+        // skip constant node, it has no cuts
+        if ( Abc_NodeIsConst(pObj) )
+            continue;
+        // compute the cuts to the internal node
+        Cut_OracleComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
+                Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        // consider dropping the fanins cuts
+        if ( fDrop )
+        {
+            Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId1(pObj) );
+        }
+    }
+    Vec_PtrFree( vNodes );
+//PRT( "Total", clock() - clk );
+//Abc_NtkPrintCuts_( p, pNtk, 0 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
+{
+    Cut_Man_t *  p;
+    Abc_Obj_t * pObj, * pNode;
+    int i, nIters, fStatus;
+    Vec_Int_t * vChoices;
+    int clk = clock();
+
+    assert( Abc_NtkIsSeq(pNtk) );
+    assert( pParams->fSeq );
+//    assert( Abc_NtkIsDfsOrdered(pNtk) );
+
+    // start the manager
+    pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
+    pParams->nCutSet = Abc_NtkCutSetNodeNum( pNtk );
+    p = Cut_ManStart( pParams );
+
+    // set cuts for the constant node and the PIs
+    pObj = Abc_NtkConst1(pNtk);
+    if ( Abc_ObjFanoutNum(pObj) > 0 )
+        Cut_NodeSetTriv( p, pObj->Id );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+//printf( "Setting trivial cut %d.\n", pObj->Id );
+        Cut_NodeSetTriv( p, pObj->Id );
+    }
+    // label the cutset nodes and set their number in the array
+    // assign the elementary cuts to the cutset nodes
+    Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+    {
+        assert( pObj->fMarkC == 0 );
+        pObj->fMarkC = 1;
+        pObj->pCopy = (Abc_Obj_t *)i;
+        Cut_NodeSetTriv( p, pObj->Id );
+//printf( "Setting trivial cut %d.\n", pObj->Id );
+    }
+
+    // process the nodes
+    vChoices = Vec_IntAlloc( 100 );
+    for ( nIters = 0; nIters < 10; nIters++ )
+    {
+//printf( "ITERATION %d:\n", nIters );
+        // compute the cuts for the internal nodes
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            Abc_NodeGetCutsSeq( p, pObj, nIters==0 );
+            // add cuts due to choices
+            if ( Abc_NodeIsAigChoice(pObj) )
+            {
+                Vec_IntClear( vChoices );
+                for ( pNode = pObj; pNode; pNode = pNode->pData )
+                    Vec_IntPush( vChoices, pNode->Id );
+                Cut_NodeUnionCutsSeq( p, vChoices, (pObj->fMarkC ? (int)pObj->pCopy : -1), nIters==0 );
+            }
+        }
+        // merge the new cuts with the old cuts
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Cut_NodeNewMergeWithOld( p, pObj->Id );
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            Cut_NodeNewMergeWithOld( p, pObj->Id );
+        // for the cutset, transfer temp cuts to new cuts
+        fStatus = 0;
+        Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+            fStatus |= Cut_NodeTempTransferToNew( p, pObj->Id, i );
+        if ( fStatus == 0 )
+            break;
+    }
+    Vec_IntFree( vChoices );
+
+    // if the status is not finished, transfer new to old for the cutset
+    Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+        Cut_NodeNewMergeWithOld( p, pObj->Id );
+
+    // transfer the old cuts to the new positions
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        Cut_NodeOldTransferToNew( p, pObj->Id );
+
+    // unlabel the cutset nodes
+    Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+        pObj->fMarkC = 0;
+if ( pParams->fVerbose )
+{
+PRT( "Total", clock() - clk );
+printf( "Converged after %d iterations.\n", nIters );
+}
+//Abc_NtkPrintCuts( p, pNtk, 1 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
+{
+    void * pList;
+    if ( pList = Abc_NodeReadCuts( p, pObj ) )
+        return pList;
+    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fDag, fTree );
+    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fDag, fTree );
+    return Abc_NodeGetCuts( p, pObj, fDag, fTree );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
+{
+    Abc_Obj_t * pFanin;
+    int fDagNode, fTriv, TreeCode = 0;
+//    assert( Abc_NtkIsStrash(pObj->pNtk) );
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+
+
+    // check if the node is a DAG node
+    fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj));
+    // increment the counter of DAG nodes
+    if ( fDagNode ) Cut_ManIncrementDagNodes( p );
+    // add the trivial cut if the node is a DAG node, or if we compute all cuts
+    fTriv = fDagNode || !fDag;
+    // check if fanins are DAG nodes
+    if ( fTree )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        TreeCode |=  (Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin));
+        pFanin = Abc_ObjFanin1(pObj);
+        TreeCode |= ((Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin)) << 1);
+    }
+
+
+    // changes due to the global/local cut computation
+    {
+        Cut_Params_t * pParams = Cut_ManReadParams(p);
+        if ( pParams->fLocal )
+        {
+            Vec_Int_t * vNodeAttrs = Cut_ManReadNodeAttrs(p);
+            fDagNode = Vec_IntEntry( vNodeAttrs, pObj->Id );
+            if ( fDagNode ) Cut_ManIncrementDagNodes( p );
+//            fTriv = fDagNode || !pParams->fGlobal;
+            fTriv = !Vec_IntEntry( vNodeAttrs, pObj->Id );
+            TreeCode = 0;
+            pFanin = Abc_ObjFanin0(pObj);
+            TreeCode |=  Vec_IntEntry( vNodeAttrs, pFanin->Id );
+            pFanin = Abc_ObjFanin1(pObj);
+            TreeCode |= (Vec_IntEntry( vNodeAttrs, pFanin->Id ) << 1);
+        }
+    }
+    return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv, TreeCode );  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv )
+{
+    int CutSetNum;
+    assert( Abc_NtkIsSeq(pObj->pNtk) );
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    fTriv     = pObj->fMarkC ? 0 : fTriv;
+    CutSetNum = pObj->fMarkC ? (int)pObj->pCopy : -1;
+    Cut_NodeComputeCutsSeq( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj), fTriv, CutSetNum );  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj )
+{
+    return Cut_NodeReadCutsNew( p, pObj->Id );  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj )
+{
+    Cut_NodeFreeCuts( p, pObj->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq )
+{
+    Cut_Man_t * pMan = p;
+    Cut_Cut_t * pList;
+    Abc_Obj_t * pObj;
+    int i;
+    printf( "Cuts of the network:\n" );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        pList = Abc_NodeReadCuts( p, pObj );
+        printf( "Node %s:\n", Abc_ObjName(pObj) );
+        Cut_CutPrintList( pList, fSeq );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq )
+{
+    Cut_Man_t * pMan = p;
+    Cut_Cut_t * pList;
+    Abc_Obj_t * pObj;
+    pObj = Abc_NtkObj( pNtk, 2 * Abc_NtkObjNum(pNtk) / 3 );
+    pList = Abc_NodeReadCuts( p, pObj );
+    printf( "Node %s:\n", Abc_ObjName(pObj) );
+    Cut_CutPrintList( pList, fSeq );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index c2142c4f..4c5af98d 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -61,6 +61,8 @@ struct Cut_ParamsStruct_t_
     int                fDrop;             // drop cuts on the fly
     int                fDag;              // compute only DAG cuts
     int                fTree;             // compute only tree cuts
+    int                fGlobal;           // compute only global cuts
+    int                fLocal;            // compute only local cuts
     int                fRecord;           // record the cut computation flow
     int                fFancy;            // perform fancy computations
     int                fVerbose;          // the verbosiness flag
@@ -118,7 +120,10 @@ extern void             Cut_ManStop( Cut_Man_t * p );
 extern void             Cut_ManPrintStats( Cut_Man_t * p );
 extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, int TimeTotal );
 extern void             Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
+extern void             Cut_ManSetNodeAttrs( Cut_Man_t * p, Vec_Int_t * vFanCounts );
 extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
+extern Cut_Params_t *   Cut_ManReadParams( Cut_Man_t * p );
+extern Vec_Int_t *      Cut_ManReadNodeAttrs( Cut_Man_t * p );
 extern void             Cut_ManIncrementDagNodes( Cut_Man_t * p );
 /*=== cutNode.c ==========================================================*/
 extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv, int TreeCode ); 
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index c6246ad7..2a0139d3 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -46,6 +46,7 @@ struct Cut_ManStruct_t_
     // user preferences
     Cut_Params_t *     pParams;          // computation parameters
     Vec_Int_t *        vFanCounts;       // the array of fanout counters
+    Vec_Int_t *        vNodeAttrs;       // node attributes (1 = global; 0 = local)
     // storage for cuts
     Vec_Ptr_t *        vCutsNew;         // new cuts by node ID
     Vec_Ptr_t *        vCutsOld;         // old cuts by node ID
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index 22ea1cb6..30e5fa38 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -233,6 +233,22 @@ void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts )
   SeeAlso     []
 
 ***********************************************************************/
+void Cut_ManSetNodeAttrs( Cut_Man_t * p, Vec_Int_t * vNodeAttrs )
+{
+    p->vNodeAttrs = vNodeAttrs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Cut_ManReadVarsMax( Cut_Man_t * p )
 {
     return p->pParams->nVarsMax;
@@ -249,6 +265,38 @@ int Cut_ManReadVarsMax( Cut_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Cut_Params_t * Cut_ManReadParams( Cut_Man_t * p )
+{
+    return p->pParams;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cut_ManReadNodeAttrs( Cut_Man_t * p )
+{
+    return p->vNodeAttrs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Cut_ManIncrementDagNodes( Cut_Man_t * p )
 {
     p->nNodesDag++;
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 6f7777ad..fafa89f7 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -206,6 +206,32 @@ static inline int Cut_CutFilterOne( Cut_Man_t * p, Cut_List_t * pSuperList, Cut_
 
 /**Function*************************************************************
 
+  Synopsis    [Checks if the cut is local and can be removed.]
+
+  Description [Returns 1 if the cut is removed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cut_CutFilterGlobal( Cut_Man_t * p, Cut_Cut_t * pCut )
+{
+    int a;
+    if ( pCut->nLeaves == 1 )
+        return 0;
+    for ( a = 0; a < (int)pCut->nLeaves; a++ )
+        if ( Vec_IntEntry( p->vNodeAttrs, pCut->pLeaves[a] ) ) // global
+            return 0;
+    // there is no global nodes, the cut should be removed
+    p->nCutsFilter++;
+    Cut_CutRecycle( p, pCut );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Checks containment for one cut.]
 
   Description [Returns 1 if the cut is removed.]
@@ -306,6 +332,14 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t
                 return 0;
         }
     }
+
+    if ( p->pParams->fGlobal )
+    {
+        assert( p->vNodeAttrs != NULL );
+        if ( Cut_CutFilterGlobal( p, pCut ) )
+            return 0;
+    }
+
     // compute the truth table
     if ( p->pParams->fTruth )
         Cut_TruthCompute( p, pCut, pCut0, pCut1, p->fCompl0, p->fCompl1 );
@@ -395,7 +429,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
         p->nNodeCuts++;
     }
     // get the cut lists of children
-    if ( pList0 == NULL || pList1 == NULL )
+    if ( pList0 == NULL || pList1 == NULL || (p->pParams->fLocal && TreeCode)  )
         return;
 
     // remember the old number of cuts
diff --git a/src/opt/cut/cutPre22.c b/src/opt/cut/cutPre22.c
index 203f9e6f..20c93c5f 100644
--- a/src/opt/cut/cutPre22.c
+++ b/src/opt/cut/cutPre22.c
@@ -617,7 +617,7 @@ void Cut_CellCrossBar( Cut_Cell_t * pCell )
         Extra_TruthCofactor0( uTemp1, pCell->nVars, pCell->CrossBar1 );
     }
     else assert( 0 );
-    Extra_TruthCombine( pCell->uTruth, uTemp0, uTemp1, pCell->nVars, pCell->CrossBar0 );
+    Extra_TruthMux( pCell->uTruth, uTemp0, uTemp1, pCell->nVars, pCell->CrossBar0 );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/cut/vec.h b/src/opt/cut/vec.h
new file mode 100644
index 00000000..6ab23298
--- /dev/null
+++ b/src/opt/cut/vec.h
@@ -0,0 +1,66 @@
+/**CFile****************************************************************
+
+  FileName    [vec.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_H__
+#define __VEC_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#include "vecInt.h"
+#include "vecStr.h"
+#include "vecPtr.h"
+#include "vecVec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/cut/vecInt.h b/src/opt/cut/vecInt.h
new file mode 100644
index 00000000..4f193cf2
--- /dev/null
+++ b/src/opt/cut/vecInt.h
@@ -0,0 +1,753 @@
+/**CFile****************************************************************
+
+  FileName    [vecInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable arrays of integers.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_INT_H__
+#define __VEC_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Int_t_       Vec_Int_t;
+struct Vec_Int_t_ 
+{
+    int              nCap;
+    int              nSize;
+    int *            pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define Vec_IntForEachEntry( vVec, Entry, i )                                               \
+    for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
+#define Vec_IntForEachEntryStart( vVec, Entry, i, Start )                                   \
+    for ( i = Start; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
+#define Vec_IntForEachEntryStartStop( vVec, Entry, i, Start, Stop )                         \
+    for ( i = Start; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
+#define Vec_IntForEachEntryReverse( vVec, pEntry, i )                                       \
+    for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntAlloc( int nCap )
+{
+    Vec_Int_t * p;
+    p = ALLOC( Vec_Int_t, 1 );
+    if ( nCap > 0 && nCap < 16 )
+        nCap = 16;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given size and cleans it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntStart( int nSize )
+{
+    Vec_Int_t * p;
+    p = Vec_IntAlloc( nSize );
+    p->nSize = nSize;
+    memset( p->pArray, 0, sizeof(int) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntAllocArray( int * pArray, int nSize )
+{
+    Vec_Int_t * p;
+    p = ALLOC( Vec_Int_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = pArray;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntAllocArrayCopy( int * pArray, int nSize )
+{
+    Vec_Int_t * p;
+    p = ALLOC( Vec_Int_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = ALLOC( int, nSize );
+    memcpy( p->pArray, pArray, sizeof(int) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntDup( Vec_Int_t * pVec )
+{
+    Vec_Int_t * p;
+    p = ALLOC( Vec_Int_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
+    memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the array into another vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_IntDupArray( Vec_Int_t * pVec )
+{
+    Vec_Int_t * p;
+    p = ALLOC( Vec_Int_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = pVec->pArray;
+    pVec->nSize  = 0;
+    pVec->nCap   = 0;
+    pVec->pArray = NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntFree( Vec_Int_t * p )
+{
+    FREE( p->pArray );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int * Vec_IntReleaseArray( Vec_Int_t * p )
+{
+    int * pArray = p->pArray;
+    p->nCap = 0;
+    p->nSize = 0;
+    p->pArray = NULL;
+    return pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int * Vec_IntArray( Vec_Int_t * p )
+{
+    return p->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntSize( Vec_Int_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntEntry( Vec_Int_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntAddToEntry( Vec_Int_t * p, int i, int Addition )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] += Addition;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntEntryLast( Vec_Int_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[p->nSize-1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the vector to the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = REALLOC( int, p->pArray, nCapMin ); 
+    assert( p->pArray );
+    p->nCap   = nCapMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Entry )
+{
+    int i;
+    Vec_IntGrow( p, nSize );
+    for ( i = 0; i < nSize; i++ )
+        p->pArray[i] = Entry;
+    p->nSize = nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry )
+{
+    int i;
+    if ( p->nSize >= nSize )
+        return;
+    Vec_IntGrow( p, nSize );
+    for ( i = p->nSize; i < nSize; i++ )
+        p->pArray[i] = Entry;
+    p->nSize = nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntShrink( Vec_Int_t * p, int nSizeNew )
+{
+    assert( p->nSize >= nSizeNew );
+    p->nSize = nSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntClear( Vec_Int_t * p )
+{
+    p->nSize = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntPush( Vec_Int_t * p, int Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_IntGrow( p, 16 );
+        else
+            Vec_IntGrow( p, 2 * p->nCap );
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntPushFirst( Vec_Int_t * p, int Entry )
+{
+    int i;
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_IntGrow( p, 16 );
+        else
+            Vec_IntGrow( p, 2 * p->nCap );
+    }
+    p->nSize++;
+    for ( i = p->nSize - 1; i >= 1; i-- )
+        p->pArray[i] = p->pArray[i-1];
+    p->pArray[0] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        int * pArray;
+        int i;
+
+        if ( p->nSize == 0 )
+            p->nCap = 1;
+        pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
+//        pArray = ALLOC( int, p->nCap * 2 );
+        if ( p->pArray )
+        {
+            for ( i = 0; i < p->nSize; i++ )
+                pArray[i] = p->pArray[i];
+            Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
+//            free( p->pArray );
+        }
+        p->nCap *= 2;
+        p->pArray = pArray;
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the entry while preserving the increasing order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry )
+{
+    int i;
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_IntGrow( p, 16 );
+        else
+            Vec_IntGrow( p, 2 * p->nCap );
+    }
+    p->nSize++;
+    for ( i = p->nSize-2; i >= 0; i-- )
+        if ( p->pArray[i] > Entry )
+            p->pArray[i+1] = p->pArray[i];
+        else
+            break;
+    p->pArray[i+1] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the entry while preserving the increasing order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntPushUniqueOrder( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return 1;
+    Vec_IntPushOrder( p, Entry );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return 1;
+    Vec_IntPush( p, Entry );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the last entry and removes it from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntPop( Vec_Int_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[--p->nSize];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntFind( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntRemove( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            break;
+    if ( i == p->nSize )
+        return 0;
+    assert( i < p->nSize );
+    for ( i++; i < p->nSize; i++ )
+        p->pArray[i-1] = p->pArray[i];
+    p->nSize--;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntSortCompare1( int * pp1, int * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntSortCompare2( int * pp1, int * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 > *pp2 )
+        return -1;
+    if ( *pp1 < *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntSort( Vec_Int_t * p, int fReverse )
+{
+    if ( fReverse ) 
+        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+                (int (*)(const void *, const void *)) Vec_IntSortCompare2 );
+    else
+        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+                (int (*)(const void *, const void *)) Vec_IntSortCompare1 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntSortCompareUnsigned( unsigned * pp1, unsigned * pp2 )
+{
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntSortUnsigned( Vec_Int_t * p )
+{
+    qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+            (int (*)(const void *, const void *)) Vec_IntSortCompareUnsigned );
+}
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/cut/vecPtr.h b/src/opt/cut/vecPtr.h
new file mode 100644
index 00000000..f2413703
--- /dev/null
+++ b/src/opt/cut/vecPtr.h
@@ -0,0 +1,579 @@
+/**CFile****************************************************************
+
+  FileName    [vecPtr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable arrays of generic pointers.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecPtr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_PTR_H__
+#define __VEC_PTR_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Ptr_t_       Vec_Ptr_t;
+struct Vec_Ptr_t_ 
+{
+    int              nCap;
+    int              nSize;
+    void **          pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+// iterators through entries
+#define Vec_PtrForEachEntry( vVec, pEntry, i )                                               \
+    for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
+#define Vec_PtrForEachEntryStart( vVec, pEntry, i, Start )                                   \
+    for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
+#define Vec_PtrForEachEntryStop( vVec, pEntry, i, Stop )                                     \
+    for ( i = 0; (i < Stop) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
+#define Vec_PtrForEachEntryStartStop( vVec, pEntry, i, Start, Stop )                         \
+    for ( i = Start; (i < Stop) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
+#define Vec_PtrForEachEntryReverse( vVec, pEntry, i )                                        \
+    for ( i = Vec_PtrSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i-- )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrAlloc( int nCap )
+{
+    Vec_Ptr_t * p;
+    p = ALLOC( Vec_Ptr_t, 1 );
+    if ( nCap > 0 && nCap < 8 )
+        nCap = 8;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given size and cleans it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrStart( int nSize )
+{
+    Vec_Ptr_t * p;
+    p = Vec_PtrAlloc( nSize );
+    p->nSize = nSize;
+    memset( p->pArray, 0, sizeof(void *) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrAllocArray( void ** pArray, int nSize )
+{
+    Vec_Ptr_t * p;
+    p = ALLOC( Vec_Ptr_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = pArray;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrAllocArrayCopy( void ** pArray, int nSize )
+{
+    Vec_Ptr_t * p;
+    p = ALLOC( Vec_Ptr_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = ALLOC( void *, nSize );
+    memcpy( p->pArray, pArray, sizeof(void *) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrDup( Vec_Ptr_t * pVec )
+{
+    Vec_Ptr_t * p;
+    p = ALLOC( Vec_Ptr_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
+    memcpy( p->pArray, pVec->pArray, sizeof(void *) * pVec->nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the array into another vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrDupArray( Vec_Ptr_t * pVec )
+{
+    Vec_Ptr_t * p;
+    p = ALLOC( Vec_Ptr_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = pVec->pArray;
+    pVec->nSize  = 0;
+    pVec->nCap   = 0;
+    pVec->pArray = NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrFree( Vec_Ptr_t * p )
+{
+    FREE( p->pArray );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void ** Vec_PtrReleaseArray( Vec_Ptr_t * p )
+{
+    void ** pArray = p->pArray;
+    p->nCap = 0;
+    p->nSize = 0;
+    p->pArray = NULL;
+    return pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void ** Vec_PtrArray( Vec_Ptr_t * p )
+{
+    return p->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_PtrSize( Vec_Ptr_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void ** Vec_PtrEntryP( Vec_Ptr_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray + i;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrWriteEntry( Vec_Ptr_t * p, int i, void * Entry )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void * Vec_PtrEntryLast( Vec_Ptr_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[p->nSize-1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the vector to the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrGrow( Vec_Ptr_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = REALLOC( void *, p->pArray, nCapMin ); 
+    p->nCap   = nCapMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrFill( Vec_Ptr_t * p, int nSize, void * Entry )
+{
+    int i;
+    Vec_PtrGrow( p, nSize );
+    for ( i = 0; i < nSize; i++ )
+        p->pArray[i] = Entry;
+    p->nSize = nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
+{
+    int i;
+    if ( p->nSize >= nSize )
+        return;
+    if ( p->nSize < 2 * nSize )
+        Vec_PtrGrow( p, 2 * nSize );
+    else
+        Vec_PtrGrow( p, p->nSize );
+    for ( i = p->nSize; i < nSize; i++ )
+        p->pArray[i] = Entry;
+    p->nSize = nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrShrink( Vec_Ptr_t * p, int nSizeNew )
+{
+    assert( p->nSize >= nSizeNew );
+    p->nSize = nSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrClear( Vec_Ptr_t * p )
+{
+    p->nSize = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrPush( Vec_Ptr_t * p, void * Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_PtrGrow( p, 16 );
+        else
+            Vec_PtrGrow( p, 2 * p->nCap );
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_PtrPushUnique( Vec_Ptr_t * p, void * Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return 1;
+    Vec_PtrPush( p, Entry );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the last entry and removes it from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void * Vec_PtrPop( Vec_Ptr_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[--p->nSize];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_PtrFind( Vec_Ptr_t * p, void * Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrRemove( Vec_Ptr_t * p, void * Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            break;
+    assert( i < p->nSize );
+    for ( i++; i < p->nSize; i++ )
+        p->pArray[i-1] = p->pArray[i];
+    p->nSize--;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Moves the first nItems to the end.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrReorder( Vec_Ptr_t * p, int nItems )
+{
+    assert( nItems < p->nSize );
+    Vec_PtrGrow( p, nItems + p->nSize );
+    memmove( (char **)p->pArray + p->nSize, p->pArray, nItems * sizeof(void*) );
+    memmove( p->pArray, (char **)p->pArray + nItems, p->nSize * sizeof(void*) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
+{
+    qsort( (void *)p->pArray, p->nSize, sizeof(void *), 
+            (int (*)(const void *, const void *)) Vec_PtrSortCompare );
+}
+
+#endif
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/cut/vecStr.h b/src/opt/cut/vecStr.h
new file mode 100644
index 00000000..eb6aa41d
--- /dev/null
+++ b/src/opt/cut/vecStr.h
@@ -0,0 +1,510 @@
+/**CFile****************************************************************
+
+  FileName    [vecStr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable arrays of characters.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecStr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_STR_H__
+#define __VEC_STR_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Str_t_       Vec_Str_t;
+struct Vec_Str_t_ 
+{
+    int              nCap;
+    int              nSize;
+    char *           pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define Vec_StrForEachEntry( vVec, Entry, i )                                               \
+    for ( i = 0; (i < Vec_StrSize(vVec)) && (((Entry) = Vec_StrEntry(vVec, i)), 1); i++ )   
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrAlloc( int nCap )
+{
+    Vec_Str_t * p;
+    p = ALLOC( Vec_Str_t, 1 );
+    if ( nCap > 0 && nCap < 16 )
+        nCap = 16;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( char, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given size and cleans it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrStart( int nSize )
+{
+    Vec_Str_t * p;
+    p = Vec_StrAlloc( nSize );
+    p->nSize = nSize;
+    memset( p->pArray, 0, sizeof(char) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrAllocArray( char * pArray, int nSize )
+{
+    Vec_Str_t * p;
+    p = ALLOC( Vec_Str_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = pArray;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrAllocArrayCopy( char * pArray, int nSize )
+{
+    Vec_Str_t * p;
+    p = ALLOC( Vec_Str_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = ALLOC( char, nSize );
+    memcpy( p->pArray, pArray, sizeof(char) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrDup( Vec_Str_t * pVec )
+{
+    Vec_Str_t * p;
+    p = ALLOC( Vec_Str_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = p->nCap? ALLOC( char, p->nCap ) : NULL;
+    memcpy( p->pArray, pVec->pArray, sizeof(char) * pVec->nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the array into another vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Str_t * Vec_StrDupArray( Vec_Str_t * pVec )
+{
+    Vec_Str_t * p;
+    p = ALLOC( Vec_Str_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = pVec->pArray;
+    pVec->nSize  = 0;
+    pVec->nCap   = 0;
+    pVec->pArray = NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrFree( Vec_Str_t * p )
+{
+    FREE( p->pArray );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char * Vec_StrReleaseArray( Vec_Str_t * p )
+{
+    char * pArray = p->pArray;
+    p->nCap = 0;
+    p->nSize = 0;
+    p->pArray = NULL;
+    return pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char * Vec_StrArray( Vec_Str_t * p )
+{
+    return p->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_StrSize( Vec_Str_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char Vec_StrEntry( Vec_Str_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrWriteEntry( Vec_Str_t * p, int i, char Entry )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char Vec_StrEntryLast( Vec_Str_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[p->nSize-1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the vector to the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrGrow( Vec_Str_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = REALLOC( char, p->pArray, 2 * nCapMin ); 
+    p->nCap   = 2 * nCapMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrFill( Vec_Str_t * p, int nSize, char Entry )
+{
+    int i;
+    Vec_StrGrow( p, nSize );
+    p->nSize = nSize;
+    for ( i = 0; i < p->nSize; i++ )
+        p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrShrink( Vec_Str_t * p, int nSizeNew )
+{
+    assert( p->nSize >= nSizeNew );
+    p->nSize = nSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrClear( Vec_Str_t * p )
+{
+    p->nSize = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_StrGrow( p, 16 );
+        else
+            Vec_StrGrow( p, 2 * p->nCap );
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Appends the string to the char vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrAppend( Vec_Str_t * p, char * pString )
+{
+    int i, nLength = strlen(pString);
+    Vec_StrGrow( p, p->nSize + nLength );
+    for ( i = 0; i < nLength; i++ )
+        p->pArray[p->nSize + i] = pString[i];
+    p->nSize += nLength;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the last entry and removes it from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char Vec_StrPop( Vec_Str_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[--p->nSize];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_StrSortCompare1( char * pp1, char * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_StrSortCompare2( char * pp1, char * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 > *pp2 )
+        return -1;
+    if ( *pp1 < *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrSort( Vec_Str_t * p, int fReverse )
+{
+    if ( fReverse ) 
+        qsort( (void *)p->pArray, p->nSize, sizeof(char), 
+                (int (*)(const void *, const void *)) Vec_StrSortCompare2 );
+    else
+        qsort( (void *)p->pArray, p->nSize, sizeof(char), 
+                (int (*)(const void *, const void *)) Vec_StrSortCompare1 );
+}
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/cut/vecVec.h b/src/opt/cut/vecVec.h
new file mode 100644
index 00000000..5b725354
--- /dev/null
+++ b/src/opt/cut/vecVec.h
@@ -0,0 +1,289 @@
+/**CFile****************************************************************
+
+  FileName    [vecVec.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable vector of resizable vectors.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecVec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_VEC_H__
+#define __VEC_VEC_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Vec_t_       Vec_Vec_t;
+struct Vec_Vec_t_ 
+{
+    int              nCap;
+    int              nSize;
+    void **          pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+// iterators through levels 
+#define Vec_VecForEachLevel( vGlob, vVec, i )                                                 \
+    for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
+#define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart )                                \
+    for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
+#define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop )                 \
+    for ( i = LevelStart; (i <= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
+#define Vec_VecForEachLevelReverse( vGlob, vVec, i )                                          \
+    for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
+
+// iteratores through entries
+#define Vec_VecForEachEntry( vGlob, pEntry, i, k )                                            \
+    for ( i = 0; i < Vec_VecSize(vGlob); i++ )                                                \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryStart( vGlob, pEntry, i, k, LevelStart )                           \
+    for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ )                                       \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryStartStop( vGlob, pEntry, i, k, LevelStart, LevelStop )            \
+    for ( i = LevelStart; i <= LevelStop; i++ )                                               \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryReverse( vGlob, pEntry, i, k )                                     \
+    for ( i = 0; i < Vec_VecSize(vGlob); i++ )                                                \
+        Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryReverseReverse( vGlob, pEntry, i, k )                              \
+    for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- )                                           \
+        Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k ) 
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Vec_t * Vec_VecAlloc( int nCap )
+{
+    Vec_Vec_t * p;
+    p = ALLOC( Vec_Vec_t, 1 );
+    if ( nCap > 0 && nCap < 8 )
+        nCap = 8;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Vec_t * Vec_VecStart( int nSize )
+{
+    Vec_Vec_t * p;
+    int i;
+    p = Vec_VecAlloc( nSize );
+    for ( i = 0; i < nSize; i++ )
+        p->pArray[i] = Vec_PtrAlloc( 0 );
+    p->nSize = nSize;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecExpand( Vec_Vec_t * p, int Level )
+{
+    int i;
+    if ( p->nSize >= Level + 1 )
+        return;
+    Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
+    for ( i = p->nSize; i <= Level; i++ )
+        p->pArray[i] = Vec_PtrAlloc( 0 );
+    p->nSize = Level + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_VecSize( Vec_Vec_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void * Vec_VecEntry( Vec_Vec_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecFree( Vec_Vec_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i;
+    Vec_VecForEachLevel( p, vVec, i )
+        Vec_PtrFree( vVec );
+    Vec_PtrFree( (Vec_Ptr_t *)p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the vector of vectors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_VecSizeSize( Vec_Vec_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i, Counter = 0;
+    Vec_VecForEachLevel( p, vVec, i )
+        Counter += vVec->nSize;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecClear( Vec_Vec_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i;
+    Vec_VecForEachLevel( p, vVec, i )
+        Vec_PtrClear( vVec );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry )
+{
+    if ( p->nSize < Level + 1 )
+    {
+        int i;
+        Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
+        for ( i = p->nSize; i < Level + 1; i++ )
+            p->pArray[i] = Vec_PtrAlloc( 0 );
+        p->nSize = Level + 1;
+    }
+    Vec_PtrPush( (Vec_Ptr_t*)p->pArray[Level], Entry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
+{
+    if ( p->nSize < Level + 1 )
+        Vec_VecPush( p, Level, Entry );
+    else
+        Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry );
+}
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index 1b23bb53..5311cec6 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -267,7 +267,7 @@ Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
     {
         pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
         pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
-        pNode->pFunc = Ivy_And( pAnd0, pAnd1 );
+        pNode->pFunc = Ivy_And( pMan, pAnd0, pAnd1 );
     }
     // complement the result if necessary
     return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );