Version abc60803

10 files changed, 171 insertions, 2689 deletions

diff --git a/src/opt/cut/abcCut.c b/src/opt/cut/abcCut.c
deleted file mode 100644
index b4b879a3..00000000
--- a/src/opt/cut/abcCut.c
+++ /dev/null
@@ -1,491 +0,0 @@
-/**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 4c5af98d..dee05dfc 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -65,6 +65,7 @@ struct Cut_ParamsStruct_t_
     int                fLocal;            // compute only local cuts
     int                fRecord;           // record the cut computation flow
     int                fFancy;            // perform fancy computations
+    int                fMap;              // computes delay of FPGA mapping with cuts
     int                fVerbose;          // the verbosiness flag
 };
 
@@ -129,6 +130,7 @@ extern void             Cut_ManIncrementDagNodes( Cut_Man_t * p );
 extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv, int TreeCode ); 
 extern Cut_Cut_t *      Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
 extern Cut_Cut_t *      Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst );
+extern int              Cut_ManMappingArea_rec( Cut_Man_t * p, int Node );
 /*=== cutSeq.c ==========================================================*/
 extern void             Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int nLat0, int nLat1, int fTriv, int CutSetNum );
 extern void             Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node );
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index 2a0139d3..17f268c7 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -71,6 +71,11 @@ struct Cut_ManStruct_t_
     Vec_Int_t *        vNodeCuts;        // the number of cuts for each node
     Vec_Int_t *        vNodeStarts;      // the number of the starting cut of each node
     Vec_Int_t *        vCutPairs;        // the pairs of parent cuts for each cut
+    // minimum delay mapping with the given cuts
+    Vec_Ptr_t *        vCutsMax;
+    Vec_Int_t *        vDelays;
+    Vec_Int_t *        vDelays2;
+    int                nDelayMin;
     // statistics
     int                nCutsCur;
     int                nCutsAlloc;
@@ -88,6 +93,7 @@ struct Cut_ManStruct_t_
     int                timeTruth;
     int                timeFilter;
     int                timeHash;
+    int                timeMap;
 };
 
 // iterator through all the cuts of the list
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index 30e5fa38..ca829471 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -95,6 +95,13 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
         p->vNodeStarts = Vec_IntStart( pParams->nIdsMax );
         p->vCutPairs   = Vec_IntAlloc( 0 );
     }
+    // allocate storage for delays
+    if ( pParams->fMap && !p->pParams->fSeq )
+    {
+        p->vDelays = Vec_IntStart( pParams->nIdsMax );
+        p->vDelays2 = Vec_IntStart( pParams->nIdsMax );
+        p->vCutsMax = Vec_PtrStart( pParams->nIdsMax );
+    }
     // memory for cuts
     p->pMmCuts = Extra_MmFixedStart( p->EntrySize );
     p->vTemp = Vec_PtrAlloc( 100 );
@@ -130,6 +137,9 @@ void Cut_ManStop( Cut_Man_t * p )
     if ( p->vFanCounts )  Vec_IntFree( p->vFanCounts );
     if ( p->vTemp )       Vec_PtrFree( p->vTemp );
 
+    if ( p->vCutsMax )    Vec_PtrFree( p->vCutsMax );
+    if ( p->vDelays )     Vec_IntFree( p->vDelays );
+    if ( p->vDelays2 )    Vec_IntFree( p->vDelays2 );
     if ( p->vNodeCuts )   Vec_IntFree( p->vNodeCuts );
     if ( p->vNodeStarts ) Vec_IntFree( p->vNodeStarts );
     if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
@@ -168,13 +178,20 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     printf( "The cut size      = %8d bytes.\n", p->EntrySize );
     printf( "Peak memory       = %8.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
     printf( "Total nodes       = %8d.\n", p->nNodes );
+    if ( p->pParams->fDag || p->pParams->fTree )
+    {
     printf( "DAG nodes         = %8d.\n", p->nNodesDag );
     printf( "Tree nodes        = %8d.\n", p->nNodes - p->nNodesDag );
+    }
     printf( "Nodes w/o cuts    = %8d.\n", p->nNodesNoCuts );
+    if ( p->pParams->fMap && !p->pParams->fSeq )
+    printf( "Mapping delay     = %8d.\n", p->nDelayMin );
+
     PRT( "Merge ", p->timeMerge );
     PRT( "Union ", p->timeUnion );
     PRT( "Filter", p->timeFilter );
     PRT( "Truth ", p->timeTruth );
+    PRT( "Map   ", p->timeMap );
 //    printf( "Nodes = %d. Multi = %d.  Cuts = %d. Multi = %d.\n", 
 //        p->nNodes, p->nNodesMulti, p->nCutsCur-p->nCutsTriv, p->nCutsMulti );
 //    printf( "Count0 = %d. Count1 = %d. Count2 = %d.\n\n", p->Count0, p->Count1, p->Count2 );
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index fafa89f7..adff525f 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -24,6 +24,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static int Cut_NodeMapping( Cut_Man_t * p, Cut_Cut_t * pCuts, int Node, int Node0, int Node1 );
+static int Cut_NodeMapping2( Cut_Man_t * p, Cut_Cut_t * pCuts, int Node, int Node0, int Node1 );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -396,15 +399,157 @@ p->timeMerge += clock() - clk;
     // set the list at the node
     Vec_PtrFillExtra( p->vCutsNew, Node + 1, NULL );
     assert( Cut_NodeReadCutsNew(p, Node) == NULL );
+
+    /////
+    pList->pNext = NULL;
+    /////
+
     Cut_NodeWriteCutsNew( p, Node, pList );
     // filter the cuts
 //clk = clock();
 //    if ( p->pParams->fFilter )
 //        Cut_CutFilter( p, pList0 );
 //p->timeFilter += clock() - clk;
+    // perform mapping of this node with these cuts
+clk = clock();
+    if ( p->pParams->fMap && !p->pParams->fSeq )
+    {
+//        int Delay1, Delay2;
+//        Delay1 = Cut_NodeMapping( p, pList, Node, Node0, Node1 );    
+//        Delay2 = Cut_NodeMapping2( p, pList, Node, Node0, Node1 );   
+//        assert( Delay1 >= Delay2 );
+        Cut_NodeMapping( p, pList, Node, Node0, Node1 );
+    }
+p->timeMap += clock() - clk;
     return pList;
 }
- 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns optimum delay mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_NodeMapping2( Cut_Man_t * p, Cut_Cut_t * pCuts, int Node, int Node0, int Node1 )
+{
+    Cut_Cut_t * pCut;
+    int DelayMin, DelayCur, i;
+    if ( pCuts == NULL )
+        p->nDelayMin = -1;
+    if ( p->nDelayMin == -1 )
+        return -1;
+    DelayMin = 1000000;
+    Cut_ListForEachCut( pCuts, pCut )
+    {
+        if ( pCut->nLeaves == 1 )
+            continue;
+        DelayCur = 0;
+        for ( i = 0; i < (int)pCut->nLeaves; i++ )
+            if ( DelayCur < Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) )
+                DelayCur = Vec_IntEntry(p->vDelays, pCut->pLeaves[i]);
+        if ( DelayMin > DelayCur )
+            DelayMin = DelayCur;
+    }
+    if ( DelayMin == 1000000 )
+    {
+         p->nDelayMin = -1;
+         return -1;
+    }
+    DelayMin++;
+    Vec_IntWriteEntry( p->vDelays, Node, DelayMin );
+    if ( p->nDelayMin < DelayMin )
+        p->nDelayMin = DelayMin;
+    return DelayMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns optimum delay mapping using the largest cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_NodeMapping( Cut_Man_t * p, Cut_Cut_t * pCuts, int Node, int Node0, int Node1 )
+{
+    Cut_Cut_t * pCut0, * pCut1, * pCut;
+    int Delay0, Delay1, Delay;
+    // get the fanin cuts
+    Delay0 = Vec_IntEntry( p->vDelays2, Node0 );
+    Delay1 = Vec_IntEntry( p->vDelays2, Node1 );
+    pCut0 = (Delay0 == 0) ? Vec_PtrEntry( p->vCutsNew, Node0 ) : Vec_PtrEntry( p->vCutsMax, Node0 );
+    pCut1 = (Delay1 == 0) ? Vec_PtrEntry( p->vCutsNew, Node1 ) : Vec_PtrEntry( p->vCutsMax, Node1 );
+    if ( Delay0 == Delay1 )
+        Delay = (Delay0 == 0) ? Delay0 + 1: Delay0;
+    else if ( Delay0 > Delay1 )
+    {
+        Delay = Delay0;
+        pCut1 = Vec_PtrEntry( p->vCutsNew, Node1 );
+        assert( pCut1->nLeaves == 1 );
+    }
+    else // if ( Delay0 < Delay1 )
+    {
+        Delay = Delay1;
+        pCut0 = Vec_PtrEntry( p->vCutsNew, Node0 );
+        assert( pCut0->nLeaves == 1 );
+    }
+    // merge the cuts
+    if ( pCut0->nLeaves < pCut1->nLeaves )
+        pCut  = Cut_CutMergeTwo( p, pCut1, pCut0 );
+    else
+        pCut  = Cut_CutMergeTwo( p, pCut0, pCut1 );
+    if ( pCut == NULL )
+    {
+        Delay++;
+        pCut = Cut_CutAlloc( p );
+        pCut->nLeaves = 2;
+        pCut->pLeaves[0] = Node0 < Node1 ? Node0 : Node1;
+        pCut->pLeaves[1] = Node0 < Node1 ? Node1 : Node0;
+    }
+    assert( Delay > 0 );
+    Vec_IntWriteEntry( p->vDelays2, Node, Delay );
+    Vec_PtrWriteEntry( p->vCutsMax, Node, pCut );
+    if ( p->nDelayMin < Delay )
+        p->nDelayMin = Delay;
+    return Delay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area after mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cut_ManMappingArea_rec( Cut_Man_t * p, int Node )
+{
+    Cut_Cut_t * pCut;
+    int i, Counter;
+    if ( p->vCutsMax == NULL )
+        return 0;
+    pCut = Vec_PtrEntry( p->vCutsMax, Node );
+    if ( pCut == NULL || pCut->nLeaves == 1 )
+        return 0;
+    Counter = 0;
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        Counter += Cut_ManMappingArea_rec( p, pCut->pLeaves[i] );
+    Vec_PtrWriteEntry( p->vCutsMax, Node, NULL );
+    return 1 + Counter;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Computes the cuts by merging cuts at two nodes.]
diff --git a/src/opt/cut/vec.h b/src/opt/cut/vec.h
deleted file mode 100644
index 6ab23298..00000000
--- a/src/opt/cut/vec.h
+++ /dev/null
@@ -1,66 +0,0 @@
-/**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
deleted file mode 100644
index 4f193cf2..00000000
--- a/src/opt/cut/vecInt.h
+++ /dev/null
@@ -1,753 +0,0 @@
-/**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
deleted file mode 100644
index f2413703..00000000
--- a/src/opt/cut/vecPtr.h
+++ /dev/null
@@ -1,579 +0,0 @@
-/**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
deleted file mode 100644
index eb6aa41d..00000000
--- a/src/opt/cut/vecStr.h
+++ /dev/null
@@ -1,510 +0,0 @@
-/**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
deleted file mode 100644
index 5b725354..00000000
--- a/src/opt/cut/vecVec.h
+++ /dev/null
@@ -1,289 +0,0 @@
-/**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                                ///
-////////////////////////////////////////////////////////////////////////
-