Version abc70930

1 files changed, 0 insertions, 1496 deletions

diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
deleted file mode 100644
index 326d1543..00000000
--- a/src/base/abci/abcRestruct.c
+++ /dev/null
@@ -1,1496 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [abcRestruct.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: abcRestruct.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "dec.h"
-#include "dsd.h"
-#include "cut.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-  
-#define RST_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
-
-typedef struct Abc_ManRst_t_   Abc_ManRst_t;
-struct Abc_ManRst_t_
-{
-    // the network
-    Abc_Ntk_t *      pNtk;              // the network for restructuring
-    // user specified parameters
-    int              nCutMax;           // the limit on the size of the supernode
-    int              fUpdateLevel;      // turns on watching the number of levels
-    int              fUseZeros;         // turns on zero-cost replacements
-    int              fVerbose;          // the verbosity flag
-    // internal data structures
-    DdManager *      dd;                // the BDD manager
-    Dsd_Manager_t *  pManDsd;           // the DSD manager
-    Vec_Ptr_t *      vVisited;          // temporary
-    Vec_Ptr_t *      vLeaves;           // temporary
-    Vec_Ptr_t *      vDecs;             // temporary
-    Vec_Ptr_t *      vTemp;             // temporary
-    Vec_Int_t *      vSims;             // temporary
-    Vec_Int_t *      vRands;            // temporary
-    Vec_Int_t *      vOnes;             // temporary
-    Vec_Int_t *      vBinate;           // temporary
-    Vec_Int_t *      vTwos;             // temporary
-    // node statistics
-    int              nLastGain;
-    int              nCutsConsidered;
-    int              nCutsExplored;
-    int              nNodesConsidered;
-    int              nNodesRestructured;
-    int              nNodesGained;
-    // runtime statistics
-    int              timeCut;
-    int              timeBdd;
-    int              timeDsd;
-    int              timeEval;
-    int              timeRes;
-    int              timeNtk;
-    int              timeTotal;
-};
-
-static Dec_Graph_t * Abc_NodeResubstitute( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList );
-
-static Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList );
-static Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCut );
-static Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, Abc_Obj_t * pRoot, int Required, int nNodesSaved, int * pnNodesAdded );
-
-static Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fDag );
-static Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose );
-static void Abc_NtkManRstStop( Abc_ManRst_t * p );
-static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Implements AIG restructuring.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose )
-{
-    ProgressBar * pProgress;
-    Abc_ManRst_t * pManRst;
-    Cut_Man_t * pManCut;
-    Cut_Cut_t * pCutList;
-    Dec_Graph_t * pGraph;
-    Abc_Obj_t * pNode;
-    int clk, clkStart = clock();
-    int fMulti = 1;
-    int fResub = 0;
-    int i, nNodes;
-
-    assert( Abc_NtkIsStrash(pNtk) );
-    // cleanup the AIG
-    Abc_AigCleanup(pNtk->pManFunc);
-    Abc_NtkCleanCopy(pNtk);
-
-    // compute the reverse levels if level update is requested
-    if ( fUpdateLevel )
-        Abc_NtkStartReverseLevels( pNtk, 0 );
-
-    // start the restructuring manager
-    pManRst = Abc_NtkManRstStart( nCutMax, fUpdateLevel, fUseZeros, fVerbose );
-    pManRst->pNtk = pNtk;
-    // start the cut manager
-clk = clock();
-    pManCut = Abc_NtkStartCutManForRestruct( pNtk, nCutMax, fMulti );
-pManRst->timeCut += clock() - clk;
-//    pNtk->pManCut = pManCut;
-
-    // resynthesize each node once
-    nNodes = Abc_NtkObjNumMax(pNtk);
-    pProgress = Extra_ProgressBarStart( stdout, nNodes );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        // skip the constant node
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        // skip persistant nodes
-        if ( Abc_NodeIsPersistant(pNode) )
-            continue;
-        // skip the node if it is inside the tree
-//        if ( Abc_ObjFanoutNum(pNode) < 2 )
-//            continue;
-        // skip the nodes with too many fanouts
-        if ( Abc_ObjFanoutNum(pNode) > 1000 )
-            continue;
-        // stop if all nodes have been tried once
-        if ( i >= nNodes )
-            break;
-        // get the cuts for the given node
-clk = clock();
-        pCutList = Abc_NodeGetCutsRecursive( pManCut, pNode, fMulti, 0 ); 
-pManRst->timeCut += clock() - clk;
-
-        // perform restructuring
-clk = clock();
-        if ( fResub )
-            pGraph = Abc_NodeResubstitute( pManRst, pNode, pCutList );
-        else
-            pGraph = Abc_NodeRestructure( pManRst, pNode, pCutList );
-pManRst->timeRes += clock() - clk;
-        if ( pGraph == NULL )
-            continue;
-
-        // acceptable replacement found, update the graph
-clk = clock();
-        Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, pManRst->nLastGain );
-pManRst->timeNtk += clock() - clk;
-        Dec_GraphFree( pGraph );
-    }
-    Extra_ProgressBarStop( pProgress );
-pManRst->timeTotal = clock() - clkStart;
-
-    // print statistics of the manager
-//    if ( fVerbose )
-        Abc_NtkManRstPrintStats( pManRst );
-    // delete the managers
-    Cut_ManStop( pManCut );
-    Abc_NtkManRstStop( pManRst );
-    // put the nodes into the DFS order and reassign their IDs
-    Abc_NtkReassignIds( pNtk );
-//    Abc_AigCheckFaninOrder( pNtk->pManFunc );
-    // fix the levels
-    if ( fUpdateLevel )
-        Abc_NtkStopReverseLevels( pNtk );
-    else
-        Abc_NtkLevel( pNtk );
-    // check
-    if ( !Abc_NtkCheck( pNtk ) )
-    {
-        printf( "Abc_NtkRefactor: The network check has failed.\n" );
-        return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_RestructNodeDivisors( Abc_ManRst_t * p, Abc_Obj_t * pRoot, int nNodesSaved )
-{
-    Abc_Obj_t * pNode, * pFanout;//, * pFanin;
-    int i, k;
-    // start with the leaves
-    Vec_PtrClear( p->vDecs );
-    Vec_PtrForEachEntry( p->vLeaves, pNode, i )
-    {
-        Vec_PtrPush( p->vDecs, pNode );
-        assert( pNode->fMarkC == 0 );
-        pNode->fMarkC = 1;
-    }
-    // explore the fanouts
-    Vec_PtrForEachEntry( p->vDecs, pNode, i )
-    {
-        // if the fanout has both fanins in the set, add it
-        Abc_ObjForEachFanout( pNode, pFanout, k )
-        {
-            if ( pFanout->fMarkC || Abc_ObjIsPo(pFanout) )
-                continue;
-            if ( Abc_ObjFanin0(pFanout)->fMarkC && Abc_ObjFanin1(pFanout)->fMarkC )
-            {
-                Vec_PtrPush( p->vDecs, pFanout );
-                pFanout->fMarkC = 1;
-            }
-        }
-    }
-    // unmark the nodes
-    Vec_PtrForEachEntry( p->vDecs, pNode, i )
-        pNode->fMarkC = 0;
-/*
-    // print the nodes
-    Vec_PtrForEachEntryStart( p->vDecs, pNode, i, Vec_PtrSize(p->vLeaves) )
-    {
-        printf( "%2d %s = ", i, Abc_NodeIsTravIdCurrent(pNode)? "*" : " " );
-        // find the first fanin
-        Vec_PtrForEachEntry( p->vDecs, pFanin, k )
-            if ( Abc_ObjFanin0(pNode) == pFanin )
-                break;
-        if ( k < Vec_PtrSize(p->vLeaves) )
-            printf( "%c", 'a' + k );
-        else
-            printf( "%d", k );
-        printf( "%s ", Abc_ObjFaninC0(pNode)? "\'" : "" );
-        // find the second fanin
-        Vec_PtrForEachEntry( p->vDecs, pFanin, k )
-            if ( Abc_ObjFanin1(pNode) == pFanin )
-                break;
-        if ( k < Vec_PtrSize(p->vLeaves) )
-            printf( "%c", 'a' + k );
-        else
-            printf( "%d", k );
-        printf( "%s ", Abc_ObjFaninC1(pNode)? "\'" : "" );
-        printf( "\n" );
-    }
-*/
-    printf( "%d\n", Vec_PtrSize(p->vDecs)-nNodesSaved-Vec_PtrSize(p->vLeaves) );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the cut manager for rewriting.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList )
-{
-    Dec_Graph_t * pGraph;
-    Cut_Cut_t * pCut;
-//    int nCuts;
-    p->nNodesConsidered++;
-/*
-    // count the number of cuts with four inputs or more
-    nCuts = 0;
-    for ( pCut = pCutList; pCut; pCut = pCut->pNext )
-        nCuts += (int)(pCut->nLeaves > 3);
-    printf( "-----------------------------------\n" );
-    printf( "Node %6d : Factor-cuts = %5d.\n", pNode->Id, nCuts );
-*/
-    // go through the interesting cuts
-    for ( pCut = pCutList; pCut; pCut = pCut->pNext )
-    {
-        if ( pCut->nLeaves < 4 )
-            continue;
-        if ( pGraph = Abc_NodeRestructureCut( p, pNode, pCut ) )
-            return pGraph;
-    }
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the cut manager for rewriting.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut )
-{
-    Dec_Graph_t * pGraph;
-    Dsd_Node_t * pNodeDsd;
-    Abc_Obj_t * pLeaf;
-    DdNode * bFunc;
-    int nNodesSaved, nNodesAdded;
-    int Required, nMaxSize, clk, i;
-    int fVeryVerbose = 0;
-
-    p->nCutsConsidered++;
-
-    // get the required time for the node
-    Required = p->fUpdateLevel? Abc_ObjRequiredLevel(pRoot) : ABC_INFINITY;
-
-    // collect the leaves of the cut
-    Vec_PtrClear( p->vLeaves );
-    for ( i = 0; i < (int)pCut->nLeaves; i++ )
-    {
-        pLeaf = Abc_NtkObj(pRoot->pNtk, pCut->pLeaves[i]);
-        if ( pLeaf == NULL )  // the so-called "bad cut phenomenon" is due to removed nodes
-            return NULL;
-        Vec_PtrPush( p->vLeaves, pLeaf );
-    }
-
-    if ( pRoot->Id == 29 )
-    {
-        int x = 0;
-    }
-
-clk = clock();
-    // collect the internal nodes of the cut
-//    Abc_NodeConeCollect( &pRoot, 1, p->vLeaves, p->vVisited, 0 );
-    // derive the BDD of the cut
-    bFunc = Abc_NodeConeBdd( p->dd, p->dd->vars, pRoot, p->vLeaves, p->vVisited );  Cudd_Ref( bFunc );
-p->timeBdd += clock() - clk;
-
-    // consider the special case, when the function is a constant
-    if ( Cudd_IsConstant(bFunc) )
-    {
-        p->nLastGain = Abc_NodeMffcSize( pRoot );
-        p->nNodesGained += p->nLastGain;
-        p->nNodesRestructured++;
-        Cudd_RecursiveDeref( p->dd, bFunc );
-        if ( Cudd_IsComplement(bFunc) )
-            return Dec_GraphCreateConst0();
-        return Dec_GraphCreateConst1();
-    }
-
-clk = clock();
-    // try disjoint support decomposition
-    pNodeDsd = Dsd_DecomposeOne( p->pManDsd, bFunc );
-p->timeDsd += clock() - clk;
-
-    // skip nodes with non-decomposable blocks
-    Dsd_TreeNodeGetInfoOne( pNodeDsd, NULL, &nMaxSize );
-    if ( nMaxSize > 3 )
-    {
-        Cudd_RecursiveDeref( p->dd, bFunc );
-        return NULL;
-    }
-
-
-/*
-    // skip nodes that cannot be improved
-    if ( Vec_PtrSize(p->vVisited) <= Dsd_TreeGetAigCost(pNodeDsd) )
-    {
-        Cudd_RecursiveDeref( p->dd, bFunc );
-        return NULL;
-    }
-*/
-
-    p->nCutsExplored++;
-
-    // mark the fanin boundary 
-    // (can mark only essential fanins, belonging to bNodeFunc!)
-    Vec_PtrForEachEntry( p->vLeaves, pLeaf, i )
-        pLeaf->vFanouts.nSize++;
-    // label MFFC with current traversal ID
-    Abc_NtkIncrementTravId( pRoot->pNtk );
-    nNodesSaved = Abc_NodeMffcLabelAig( pRoot );
-    // unmark the fanin boundary and set the fanins as leaves in the form
-    Vec_PtrForEachEntry( p->vLeaves, pLeaf, i )
-        pLeaf->vFanouts.nSize--;
-/*
-    if ( nNodesSaved < 3 )
-    {
-        Cudd_RecursiveDeref( p->dd, bFunc );
-        return NULL;
-    }
-*/
-
-/* 
-    printf( "%5d : Cut-size = %d.  Old AIG = %2d.  New AIG = %2d.  Old MFFC = %2d.\n",
-        pRoot->Id, pCut->nLeaves, Vec_PtrSize(p->vVisited), Dsd_TreeGetAigCost(pNodeDsd), 
-        nNodesSaved );
-    Dsd_NodePrint( stdout, pNodeDsd );
-
-    Abc_RestructNodeDivisors( p, pRoot );
-
-    if ( pRoot->Id == 433 )
-    {
-        int x = 0;
-    }
-*/
-//    Abc_RestructNodeDivisors( p, pRoot, nNodesSaved );
-
-
-    // detect how many new nodes will be added (while taking into account reused nodes)
-clk = clock();
-    if ( nMaxSize > 3 )
-        pGraph = NULL;
-    else
-        pGraph = Abc_NodeEvaluateDsd( p, pNodeDsd, pRoot, Required, nNodesSaved, &nNodesAdded );
-//    pGraph = NULL;
-p->timeEval += clock() - clk;
-
-    // quit if there is no improvement
-    if ( pGraph == NULL || nNodesAdded == -1 || nNodesAdded == nNodesSaved && !p->fUseZeros )
-    {
-        Cudd_RecursiveDeref( p->dd, bFunc );
-        if ( pGraph ) Dec_GraphFree( pGraph );
-        return NULL;
-    }
-
-/*
-    // print stats
-    printf( "%5d : Cut-size = %d.  Old AIG = %2d.  New AIG = %2d.  Old MFFC = %2d.  New MFFC = %2d. Gain = %d.\n",
-        pRoot->Id, pCut->nLeaves, Vec_PtrSize(p->vVisited), Dsd_TreeGetAigCost(pNodeDsd), 
-        nNodesSaved, nNodesAdded, (nNodesAdded == -1)? 0 : nNodesSaved-nNodesAdded );
-//    Dsd_NodePrint( stdout, pNodeDsd );
-//    Dec_GraphPrint( stdout, pGraph, NULL, NULL );
-*/
-
-    // compute the total gain in the number of nodes
-    p->nLastGain = nNodesSaved - nNodesAdded;
-    p->nNodesGained += p->nLastGain;
-    p->nNodesRestructured++;
-
-    // report the progress
-    if ( fVeryVerbose )
-    {
-        printf( "Node %6s : ",  Abc_ObjName(pRoot) );
-        printf( "Cone = %2d. ", p->vLeaves->nSize );
-        printf( "BDD = %2d. ",  Cudd_DagSize(bFunc) );
-        printf( "FF = %2d. ",   1 + Dec_GraphNodeNum(pGraph) );
-        printf( "MFFC = %2d. ", nNodesSaved );
-        printf( "Add = %2d. ",  nNodesAdded );
-        printf( "GAIN = %2d. ", p->nLastGain );
-        printf( "\n" );
-    }
-    Cudd_RecursiveDeref( p->dd, bFunc );
-    return pGraph;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Moves closer to the end the node that is best for sharing.]
-
-  Description [If the flag is set, tries to find an EXOR, otherwise, tries
-  to find an OR.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeEdgeDsdPermute( Dec_Graph_t * pGraph, Abc_ManRst_t * pManRst, Vec_Int_t * vEdges, int fExor )
-{
-    Dec_Edge_t eNode1, eNode2, eNode3;
-    Abc_Obj_t * pNode1, * pNode2, * pNode3, * pTemp;
-    int LeftBound = 0, RightBound, i;
-    // get the right bound
-    RightBound = Vec_IntSize(vEdges) - 2;
-    assert( LeftBound <= RightBound );
-    if ( LeftBound == RightBound )
-        return;
-    // get the two last nodes
-    eNode1 = Dec_IntToEdge( Vec_IntEntry(vEdges, RightBound + 1) );
-    eNode2 = Dec_IntToEdge( Vec_IntEntry(vEdges, RightBound    ) );
-    pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc;
-    pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc;
-    pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl );
-    pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl );
-    // quit if the last node does not exist
-    if ( pNode1 == NULL )
-        return;
-    // find the first node that can be shared
-    for ( i = RightBound; i >= LeftBound; i-- )
-    {
-        // get the third node
-        eNode3 = Dec_IntToEdge( Vec_IntEntry(vEdges, i) );
-        pNode3 = Dec_GraphNode( pGraph, eNode3.Node )->pFunc;
-        pNode3 = !pNode3? NULL : Abc_ObjNotCond( pNode3, eNode3.fCompl );
-        if ( pNode3 == NULL )
-            continue;
-        // check if the node exists
-        if ( fExor )
-        {
-            if ( pNode1 && pNode3 )
-            {
-                pTemp = Abc_AigXorLookup( pManRst->pNtk->pManFunc, pNode1, pNode3, NULL );
-                if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
-                    continue;
-
-                if ( pNode3 == pNode2 )
-                    return;
-                Vec_IntWriteEntry( vEdges, i,          Dec_EdgeToInt(eNode2) );
-                Vec_IntWriteEntry( vEdges, RightBound, Dec_EdgeToInt(eNode3) );
-                return;
-            }
-        }
-        else
-        {
-            if ( pNode1 && pNode3 )
-            {
-                pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode3) );
-                if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
-                    continue;
-
-                if ( eNode3.Node == eNode2.Node )
-                    return;
-                Vec_IntWriteEntry( vEdges, i,          Dec_EdgeToInt(eNode2) );
-                Vec_IntWriteEntry( vEdges, RightBound, Dec_EdgeToInt(eNode3) );
-                return;
-            }
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the new edge in the given order.]
-
-  Description [Similar to Vec_IntPushOrder, except in decreasing order.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeEdgeDsdPushOrdered( Dec_Graph_t * pGraph, Vec_Int_t * vEdges, int Edge )
-{
-    int i, NodeOld, NodeNew;
-    vEdges->nSize++;
-    for ( i = vEdges->nSize-2; i >= 0; i-- )
-    {
-        NodeOld = Dec_IntToEdge(vEdges->pArray[i]).Node;
-        NodeNew = Dec_IntToEdge(Edge).Node;
-        // use <= because we are trying to push the new (non-existent) nodes as far as possible
-        if ( Dec_GraphNode(pGraph, NodeOld)->Level <= Dec_GraphNode(pGraph, NodeNew)->Level )
-            vEdges->pArray[i+1] = vEdges->pArray[i];
-        else
-            break;
-    }
-    vEdges->pArray[i+1] = Edge;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Evaluation one DSD.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Edge_t Abc_NodeEvaluateDsd_rec( Dec_Graph_t * pGraph, Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, int Required, int nNodesSaved, int * pnNodesAdded )
-{
-    Dec_Edge_t eNode1, eNode2, eNode3, eResult, eQuit = { 0, 2006 };
-    Abc_Obj_t * pNode1, * pNode2, * pNode3, * pNode4, * pTemp;
-    Dsd_Node_t * pChildDsd;
-    Dsd_Type_t DecType;
-    Vec_Int_t * vEdges;
-    int Level1, Level2, Level3, Level4;
-    int i, Index, fCompl, Type;
-
-    // remove the complemented attribute
-    fCompl   = Dsd_IsComplement( pNodeDsd );
-    pNodeDsd = Dsd_Regular( pNodeDsd );
-
-    // consider the trivial case
-    DecType = Dsd_NodeReadType( pNodeDsd );
-    if ( DecType == DSD_NODE_BUF )
-    {
-        Index = Dsd_NodeReadFunc(pNodeDsd)->index;
-        assert( Index < Dec_GraphLeaveNum(pGraph) );
-        eResult = Dec_EdgeCreate( Index, fCompl );
-        return eResult;
-    }
-    assert( DecType == DSD_NODE_OR || DecType == DSD_NODE_EXOR || DecType == DSD_NODE_PRIME );
-
-    // solve the problem for the children
-    vEdges = Vec_IntAlloc( Dsd_NodeReadDecsNum(pNodeDsd) );
-    Dsd_NodeForEachChild( pNodeDsd, i, pChildDsd )
-    {
-        eResult = Abc_NodeEvaluateDsd_rec( pGraph, pManRst, pChildDsd, Required, nNodesSaved, pnNodesAdded );
-        if ( eResult.Node == eQuit.Node ) // infeasible
-        {
-            Vec_IntFree( vEdges );
-            return eQuit;
-        }
-        // order the inputs only if this is OR or EXOR
-        if ( DecType == DSD_NODE_PRIME )
-            Vec_IntPush( vEdges, Dec_EdgeToInt(eResult) );
-        else
-            Abc_NodeEdgeDsdPushOrdered( pGraph, vEdges, Dec_EdgeToInt(eResult) );
-    }
-    // the edges are sorted by the level of their nodes in decreasing order
-
-
-    // consider special cases
-    if ( DecType == DSD_NODE_OR )
-    {
-        // try to balance the nodes by delay
-        assert( Vec_IntSize(vEdges) > 1 );
-        while ( Vec_IntSize(vEdges) > 1 )
-        {
-            // permute the last two entries
-            if ( Vec_IntSize(vEdges) > 2 )
-                Abc_NodeEdgeDsdPermute( pGraph, pManRst, vEdges, 0 );
-            // get the two last nodes
-            eNode1 = Dec_IntToEdge( Vec_IntPop(vEdges) );
-            eNode2 = Dec_IntToEdge( Vec_IntPop(vEdges) );
-            pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc;
-            pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc;
-            pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl );
-            pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl );
-            // check if the new node exists
-            pNode3 = NULL;
-            if ( pNode1 && pNode2 )
-            {
-                pNode3 = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) ); 
-                pNode3 = !pNode3? NULL : Abc_ObjNot(pNode3);
-            }
-            // create the new node
-            eNode3 = Dec_GraphAddNodeOr( pGraph, eNode1, eNode2 );
-            // set level
-            Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level;
-            Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level;
-            Dec_GraphNode( pGraph, eNode3.Node )->Level = 1 + ABC_MAX(Level1, Level2);
-            // get the new node if possible
-            if ( pNode3 )
-            {
-                Dec_GraphNode( pGraph, eNode3.Node )->pFunc = Abc_ObjNotCond(pNode3, eNode3.fCompl);
-                Level3 = Dec_GraphNode( pGraph, eNode3.Node )->Level;
-                assert( Required == ABC_INFINITY || Level3 == (int)Abc_ObjRegular(pNode3)->Level );
-            }
-            if ( !pNode3 || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pNode3)) )
-            {
-                (*pnNodesAdded)++;
-                if ( *pnNodesAdded > nNodesSaved )
-                {
-                    Vec_IntFree( vEdges );
-                    return eQuit;
-                }
-            }
-            // add the resulting node to the form
-            Abc_NodeEdgeDsdPushOrdered( pGraph, vEdges, Dec_EdgeToInt(eNode3) );
-        }
-        // get the last node
-        eResult = Dec_IntToEdge( Vec_IntPop(vEdges) );
-        Vec_IntFree( vEdges );
-        // complement the graph if the node was complemented
-        eResult.fCompl ^= fCompl;
-        return eResult;
-    }
-    if ( DecType == DSD_NODE_EXOR )
-    {
-        // try to balance the nodes by delay
-        assert( Vec_IntSize(vEdges) > 1 );
-        while ( Vec_IntSize(vEdges) > 1 )
-        {
-            // permute the last two entries
-            if ( Vec_IntSize(vEdges) > 2 )
-                Abc_NodeEdgeDsdPermute( pGraph, pManRst, vEdges, 1 );
-            // get the two last nodes
-            eNode1 = Dec_IntToEdge( Vec_IntPop(vEdges) );
-            eNode2 = Dec_IntToEdge( Vec_IntPop(vEdges) );
-            pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc;
-            pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc;
-            pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl );
-            pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl );
-            // check if the new node exists
-            Type = 0;
-            pNode3 = NULL;
-            if ( pNode1 && pNode2 )
-                pNode3 = Abc_AigXorLookup( pManRst->pNtk->pManFunc, pNode1, pNode2, &Type ); 
-            // create the new node
-            eNode3 = Dec_GraphAddNodeXor( pGraph, eNode1, eNode2, Type ); // should have the same structure as in AIG
-            // set level
-            Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level;
-            Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level;
-            Dec_GraphNode( pGraph, eNode3.Node )->Level = 2 + ABC_MAX(Level1, Level2);
-            // get the new node if possible
-            if ( pNode3 )
-            {
-                Dec_GraphNode( pGraph, eNode3.Node )->pFunc = Abc_ObjNotCond(pNode3, eNode3.fCompl);
-                Level3 = Dec_GraphNode( pGraph, eNode3.Node )->Level;
-                assert( Required == ABC_INFINITY || Level3 == (int)Abc_ObjRegular(pNode3)->Level );
-            }
-            if ( !pNode3 || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pNode3)) )
-            {
-                (*pnNodesAdded)++;
-                if ( !pNode1 || !pNode2 )
-                    (*pnNodesAdded) += 2;
-                else if ( Type == 0 )
-                {
-                    pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, Abc_ObjNot(pNode2) );
-                    if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
-                        (*pnNodesAdded)++;
-                    pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), pNode2 );
-                    if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
-                        (*pnNodesAdded)++;
-                }
-                else
-                {
-                    pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) );
-                    if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
-                        (*pnNodesAdded)++;
-                    pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, pNode2 );
-                    if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
-                        (*pnNodesAdded)++;
-                }
-                if ( *pnNodesAdded > nNodesSaved )
-                {
-                    Vec_IntFree( vEdges );
-                    return eQuit;
-                }
-            }
-            // add the resulting node to the form
-            Abc_NodeEdgeDsdPushOrdered( pGraph, vEdges, Dec_EdgeToInt(eNode3) );
-        }
-        // get the last node
-        eResult = Dec_IntToEdge( Vec_IntPop(vEdges) );
-        Vec_IntFree( vEdges );
-        // complement the graph if the node is complemented
-        eResult.fCompl ^= fCompl;
-        return eResult;
-    }
-    if ( DecType == DSD_NODE_PRIME )
-    {
-        DdNode * bLocal, * bVar, * bCofT, * bCofE;
-        bLocal = Dsd_TreeGetPrimeFunction( pManRst->dd, pNodeDsd );  Cudd_Ref( bLocal );
-//Extra_bddPrint( pManRst->dd, bLocal );
-
-        bVar  = pManRst->dd->vars[0];
-        bCofE = Cudd_Cofactor( pManRst->dd, bLocal, Cudd_Not(bVar) );  Cudd_Ref( bCofE );
-        bCofT = Cudd_Cofactor( pManRst->dd, bLocal, bVar );            Cudd_Ref( bCofT );
-        if ( !Extra_bddIsVar(bCofE) || !Extra_bddIsVar(bCofT) )
-        {
-            Cudd_RecursiveDeref( pManRst->dd, bCofE );
-            Cudd_RecursiveDeref( pManRst->dd, bCofT );
-            bVar  = pManRst->dd->vars[1];
-            bCofE = Cudd_Cofactor( pManRst->dd, bLocal, Cudd_Not(bVar) );  Cudd_Ref( bCofE );
-            bCofT = Cudd_Cofactor( pManRst->dd, bLocal, bVar );            Cudd_Ref( bCofT );
-            if ( !Extra_bddIsVar(bCofE) || !Extra_bddIsVar(bCofT) )
-            {
-                Cudd_RecursiveDeref( pManRst->dd, bCofE );
-                Cudd_RecursiveDeref( pManRst->dd, bCofT );
-                bVar  = pManRst->dd->vars[2];
-                bCofE = Cudd_Cofactor( pManRst->dd, bLocal, Cudd_Not(bVar) );  Cudd_Ref( bCofE );
-                bCofT = Cudd_Cofactor( pManRst->dd, bLocal, bVar );            Cudd_Ref( bCofT );
-                if ( !Extra_bddIsVar(bCofE) || !Extra_bddIsVar(bCofT) )
-                {
-                    Cudd_RecursiveDeref( pManRst->dd, bCofE );
-                    Cudd_RecursiveDeref( pManRst->dd, bCofT );
-                    Cudd_RecursiveDeref( pManRst->dd, bLocal );
-                    Vec_IntFree( vEdges );
-                    return eQuit;
-                }
-            }
-        }
-        Cudd_RecursiveDeref( pManRst->dd, bLocal );
-        // we found the control variable (bVar) and the var-cofactors (bCofT, bCofE)
-
-        // find the graph nodes
-        eNode1 = Dec_IntToEdge( Vec_IntEntry(vEdges, bVar->index) );
-        eNode2 = Dec_IntToEdge( Vec_IntEntry(vEdges, Cudd_Regular(bCofT)->index) );
-        eNode3 = Dec_IntToEdge( Vec_IntEntry(vEdges, Cudd_Regular(bCofE)->index) );
-        // add the complements to the graph nodes
-        eNode2.fCompl ^= Cudd_IsComplement(bCofT);
-        eNode3.fCompl ^= Cudd_IsComplement(bCofE);
-
-        // because the cofactors are vars, we can just as well deref them here
-        Cudd_RecursiveDeref( pManRst->dd, bCofE );
-        Cudd_RecursiveDeref( pManRst->dd, bCofT );
-
-        // find the ABC nodes
-        pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc;
-        pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc;
-        pNode3 = Dec_GraphNode( pGraph, eNode3.Node )->pFunc;
-        pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl );
-        pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl );
-        pNode3 = !pNode3? NULL : Abc_ObjNotCond( pNode3, eNode3.fCompl );
-
-        // check if the new node exists
-        Type = 0;
-        pNode4 = NULL;
-        if ( pNode1 && pNode2 && pNode3 )
-            pNode4 = Abc_AigMuxLookup( pManRst->pNtk->pManFunc, pNode1, pNode2, pNode3, &Type ); 
-
-        // create the new node
-        eResult = Dec_GraphAddNodeMux( pGraph, eNode1, eNode2, eNode3, Type ); // should have the same structure as AIG
-
-        // set level
-        Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level;
-        Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level;
-        Level3 = Dec_GraphNode( pGraph, eNode3.Node )->Level;
-        Dec_GraphNode( pGraph, eResult.Node )->Level = 2 + ABC_MAX( ABC_MAX(Level1, Level2), Level3 );
-        // get the new node if possible
-        if ( pNode4 )
-        {
-            Dec_GraphNode( pGraph, eResult.Node )->pFunc = Abc_ObjNotCond(pNode4, eResult.fCompl);
-            Level4 = Dec_GraphNode( pGraph, eResult.Node )->Level;
-            assert( Required == ABC_INFINITY || Level4 == (int)Abc_ObjRegular(pNode4)->Level );
-        }
-        if ( !pNode4 || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pNode4)) )
-        {
-            (*pnNodesAdded)++;
-            if ( Type == 0 ) 
-            {
-                if ( !pNode1 || !pNode2 )
-                    (*pnNodesAdded)++;
-                else
-                {
-                    pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, pNode2 );
-                    if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
-                        (*pnNodesAdded)++;
-                }
-                if ( !pNode1 || !pNode3 )
-                    (*pnNodesAdded)++;
-                else
-                {
-                    pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), pNode3 );
-                    if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
-                        (*pnNodesAdded)++;
-                }
-            }
-            else
-            {
-                if ( !pNode1 || !pNode2 )
-                    (*pnNodesAdded)++;
-                else
-                {
-                    pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, Abc_ObjNot(pNode2) );
-                    if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
-                        (*pnNodesAdded)++;
-                }
-                if ( !pNode1 || !pNode3 )
-                    (*pnNodesAdded)++;
-                else
-                {
-                    pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode3) );
-                    if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
-                        (*pnNodesAdded)++;
-                }
-            }
-            if ( *pnNodesAdded > nNodesSaved )
-            {
-                Vec_IntFree( vEdges );
-                return eQuit;
-            }
-        }
-
-        Vec_IntFree( vEdges );
-        // complement the graph if the node was complemented
-        eResult.fCompl ^= fCompl;
-        return eResult;
-    }
-    Vec_IntFree( vEdges );
-    return eQuit;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Evaluation one DSD.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, Abc_Obj_t * pRoot, int Required, int nNodesSaved, int * pnNodesAdded )
-{
-    Dec_Graph_t * pGraph;
-    Dec_Edge_t gEdge;
-    Abc_Obj_t * pLeaf;
-    Dec_Node_t * pNode;
-    int i;
-
-    // create the graph and set the leaves
-    pGraph = Dec_GraphCreate( Vec_PtrSize(pManRst->vLeaves) );
-    Dec_GraphForEachLeaf( pGraph, pNode, i )
-    {
-        pLeaf = Vec_PtrEntry( pManRst->vLeaves, i );
-        pNode->pFunc = pLeaf;
-        pNode->Level = pLeaf->Level;
-    }
-
-    // create the decomposition structure from the DSD
-    *pnNodesAdded = 0;
-    gEdge = Abc_NodeEvaluateDsd_rec( pGraph, pManRst, pNodeDsd, Required, nNodesSaved, pnNodesAdded );
-    if ( gEdge.Node > 1000 ) // infeasible
-    {
-        *pnNodesAdded = -1;
-        Dec_GraphFree( pGraph );
-        return NULL;
-    }
-
-    // quit if the root node is the same
-    pLeaf = Dec_GraphNode( pGraph, gEdge.Node )->pFunc;
-    if ( Abc_ObjRegular(pLeaf) == pRoot )
-    {
-        *pnNodesAdded = -1;
-        Dec_GraphFree( pGraph );
-        return NULL;
-    }
-
-    Dec_GraphSetRoot( pGraph, gEdge );
-    return pGraph;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the cut manager for rewriting.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fDag )
-{
-    static Cut_Params_t Params, * pParams = &Params;
-    Cut_Man_t * pManCut;
-    Abc_Obj_t * pObj;
-    int i;
-    // start the cut manager
-    memset( pParams, 0, sizeof(Cut_Params_t) );
-    pParams->nVarsMax  = nCutMax; // the max cut size ("k" of the k-feasible cuts)
-    pParams->nKeepMax  = 250;     // the max number of cuts kept at a node
-    pParams->fTruth    = 0;       // compute truth tables
-    pParams->fFilter   = 1;       // filter dominated cuts
-    pParams->fSeq      = 0;       // compute sequential cuts
-    pParams->fDrop     = 0;       // drop cuts on the fly
-    pParams->fDag      = fDag;    // compute DAG cuts
-    pParams->fTree     = 0;       // compute tree cuts
-    pParams->fVerbose  = 0;       // the verbosiness flag
-    pParams->nIdsMax   = Abc_NtkObjNumMax( pNtk );
-    pManCut = Cut_ManStart( pParams );
-    if ( pParams->fDrop )
-        Cut_ManSetFanoutCounts( pManCut, Abc_NtkFanoutCounts(pNtk) );
-    // set cuts for PIs
-    Abc_NtkForEachCi( pNtk, pObj, i )
-        if ( Abc_ObjFanoutNum(pObj) > 0 )
-            Cut_NodeSetTriv( pManCut, pObj->Id );
-    return pManCut;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the resynthesis manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose )
-{
-    Abc_ManRst_t * p;
-    p = ALLOC( Abc_ManRst_t, 1 );
-    memset( p, 0, sizeof(Abc_ManRst_t) );
-    // set the parameters
-    p->nCutMax      = nCutMax;
-    p->fUpdateLevel = fUpdateLevel;
-    p->fUseZeros    = fUseZeros;
-    p->fVerbose     = fVerbose;
-    // start the BDD manager
-    p->dd = Cudd_Init( p->nCutMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    Cudd_zddVarsFromBddVars( p->dd, 2 );
-    // start the DSD manager
-    p->pManDsd = Dsd_ManagerStart( p->dd, p->dd->size, 0 );
-    // other temp datastructures
-    p->vVisited     = Vec_PtrAlloc( 100 );
-    p->vLeaves      = Vec_PtrAlloc( 100 );
-    p->vDecs        = Vec_PtrAlloc( 100 );
-    p->vTemp        = Vec_PtrAlloc( 100 );
-    p->vSims        = Vec_IntAlloc( 100 );
-    p->vOnes        = Vec_IntAlloc( 100 );
-    p->vBinate      = Vec_IntAlloc( 100 );
-    p->vTwos        = Vec_IntAlloc( 100 );
-    p->vRands       = Vec_IntAlloc( 20 );
-    
-    {
-        int i;
-        for ( i = 0; i < 20; i++ )
-            Vec_IntPush( p->vRands, (int)RST_RANDOM_UNSIGNED );
-    }
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the resynthesis manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkManRstStop( Abc_ManRst_t * p )
-{
-    Dsd_ManagerStop( p->pManDsd );
-    Extra_StopManager( p->dd );
-    Vec_PtrFree( p->vDecs );
-    Vec_PtrFree( p->vLeaves );
-    Vec_PtrFree( p->vVisited );
-    Vec_PtrFree( p->vTemp );
-    Vec_IntFree( p->vSims );
-    Vec_IntFree( p->vOnes );
-    Vec_IntFree( p->vBinate );
-    Vec_IntFree( p->vTwos );
-    Vec_IntFree( p->vRands );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the resynthesis manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkManRstPrintStats( Abc_ManRst_t * p )
-{
-    printf( "Refactoring statistics:\n" );
-    printf( "Nodes considered   = %8d.\n", p->nNodesConsidered   );
-    printf( "Cuts considered    = %8d.\n", p->nCutsConsidered    );
-    printf( "Cuts explored      = %8d.\n", p->nCutsExplored      );
-    printf( "Nodes restructured = %8d.\n", p->nNodesRestructured );
-    printf( "Calculated gain    = %8d.\n", p->nNodesGained       );
-    PRT( "Cuts       ", p->timeCut );
-    PRT( "Resynthesis", p->timeRes );
-    PRT( "    BDD    ", p->timeBdd );
-    PRT( "    DSD    ", p->timeDsd );
-    PRT( "    Eval   ", p->timeEval );
-    PRT( "AIG update ", p->timeNtk );
-    PRT( "TOTAL      ", p->timeTotal );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_Abc_NodeResubCollectDivs( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut )
-{
-    Abc_Obj_t * pNode, * pFanout;
-    int i, k;
-    // collect the leaves of the cut
-    Vec_PtrClear( p->vDecs );
-    Abc_NtkIncrementTravId( pRoot->pNtk );
-    for ( i = 0; i < (int)pCut->nLeaves; i++ )
-    {
-        pNode = Abc_NtkObj(pRoot->pNtk, pCut->pLeaves[i]);
-        if ( pNode == NULL )  // the so-called "bad cut phenomenon" is due to removed nodes
-            return 0;
-        Vec_PtrPush( p->vDecs, pNode );
-        Abc_NodeSetTravIdCurrent( pNode );        
-    }
-    // explore the fanouts
-    Vec_PtrForEachEntry( p->vDecs, pNode, i )
-    {
-        // if the fanout has both fanins in the set, add it
-        Abc_ObjForEachFanout( pNode, pFanout, k )
-        {
-            if ( Abc_NodeIsTravIdCurrent(pFanout) || Abc_ObjIsPo(pFanout) )
-                continue;
-            if ( Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pFanout)) && Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pFanout)) )
-            {
-                Vec_PtrPush( p->vDecs, pFanout );
-                Abc_NodeSetTravIdCurrent( pFanout );     
-            }
-        }
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeResubMffc_rec( Abc_Obj_t * pNode )
-{
-    if ( Abc_NodeIsTravIdCurrent(pNode) )
-        return 0;
-    Abc_NodeSetTravIdCurrent( pNode ); 
-    return 1 + Abc_NodeResubMffc_rec( Abc_ObjFanin0(pNode) ) +
-        Abc_NodeResubMffc_rec( Abc_ObjFanin1(pNode) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeResubMffc( Abc_ManRst_t * p, Vec_Ptr_t * vDecs, int nLeaves, Abc_Obj_t * pRoot )
-{
-    Abc_Obj_t * pObj;
-    int Counter, i, k;
-    // increment the traversal ID for the leaves
-    Abc_NtkIncrementTravId( pRoot->pNtk );
-    // label the leaves
-    Vec_PtrForEachEntryStop( vDecs, pObj, i, nLeaves )
-        Abc_NodeSetTravIdCurrent( pObj ); 
-    // make sure the node is in the cone and is no one of the leaves
-    assert( Abc_NodeIsTravIdPrevious(pRoot) );
-    Counter = Abc_NodeResubMffc_rec( pRoot );
-    // move the labeled nodes to the end 
-    Vec_PtrClear( p->vTemp );
-    k = 0;
-    Vec_PtrForEachEntryStart( vDecs, pObj, i, nLeaves )
-        if ( Abc_NodeIsTravIdCurrent(pObj) )
-            Vec_PtrPush( p->vTemp, pObj );
-        else
-            Vec_PtrWriteEntry( vDecs, k++, pObj );
-    // add the labeled nodes
-    Vec_PtrForEachEntry( p->vTemp, pObj, i )
-        Vec_PtrWriteEntry( vDecs, k++, pObj );
-    assert( k == Vec_PtrSize(p->vDecs) );
-    assert( pRoot == Vec_PtrEntryLast(p->vDecs) );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs simulation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeMffcSimulate( Vec_Ptr_t * vDecs, int nLeaves, Vec_Int_t * vRands, Vec_Int_t * vSims )
-{
-    Abc_Obj_t * pObj;
-    unsigned uData0, uData1, uData;
-    int i;
-    // initialize random simulation data
-    Vec_IntClear( vSims );
-    Vec_PtrForEachEntryStop( vDecs, pObj, i, nLeaves )
-    {
-        uData = (unsigned)Vec_IntEntry( vRands, i );
-        pObj->pData = (void *)uData;
-        Vec_IntPush( vSims, uData );
-    }
-    // simulate
-    Vec_PtrForEachEntryStart( vDecs, pObj, i, nLeaves )
-    {
-        uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
-        uData1 = (unsigned)Abc_ObjFanin1(pObj)->pData;
-        uData = (Abc_ObjFaninC0(pObj)? ~uData0 : uData0) & (Abc_ObjFaninC1(pObj)? ~uData1 : uData1);
-        pObj->pData = (void *)uData;
-        Vec_IntPush( vSims, uData );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Full equality check.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeCheckFull( Abc_ManRst_t * p, Dec_Graph_t * pGraph )
-{
-    return 1;
-}
-/**Function*************************************************************
-
-  Synopsis    [Detect contants.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Graph_t * Abc_NodeMffcConstants( Abc_ManRst_t * p, Vec_Int_t * vSims )
-{
-    Dec_Graph_t * pGraph;
-    unsigned uRoot;
-    // get the root node
-    uRoot = (unsigned)Vec_IntEntryLast( vSims );
-    // get the graph if the node looks constant
-    if ( uRoot == 0 )
-        pGraph = Dec_GraphCreateConst0();
-    else if ( uRoot == ~(unsigned)0 )
-        pGraph = Dec_GraphCreateConst1();
-    // check the graph
-    if ( Abc_NodeCheckFull( p, pGraph ) )
-        return pGraph;
-    Dec_GraphFree( pGraph );
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Detect single non-overlaps.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Graph_t * Abc_NodeMffcSingleVar( Abc_ManRst_t * p, Vec_Int_t * vSims, int nNodes, Vec_Int_t * vOnes )
-{
-    Dec_Graph_t * pGraph;
-    unsigned uRoot, uNode;
-    int i;
-
-    Vec_IntClear( vOnes );
-    Vec_IntClear( p->vBinate );
-    uRoot = (unsigned)Vec_IntEntryLast( vSims );
-    for ( i = 0; i < nNodes; i++ )
-    {
-        uNode = (unsigned)Vec_IntEntry( vSims, i );
-        if ( uRoot == uNode || uRoot == ~uNode )
-        {
-            pGraph = Dec_GraphCreate( 1 );
-            Dec_GraphNode( pGraph, 0 )->pFunc = Vec_PtrEntry( p->vDecs, i );
-            Dec_GraphSetRoot( pGraph, Dec_IntToEdge( (int)(uRoot == ~uNode) ) );
-            // check the graph
-            if ( Abc_NodeCheckFull( p, pGraph ) )
-                return pGraph;
-            Dec_GraphFree( pGraph );
-        }
-        if ( (uRoot & uNode) == 0 )
-            Vec_IntPush( vOnes, i << 1 );
-        else if ( (uRoot & ~uNode) == 0 )
-            Vec_IntPush( vOnes, (i << 1) + 1 );
-        else
-            Vec_IntPush( p->vBinate, i );
-    }    
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Detect single non-overlaps.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Graph_t * Abc_NodeMffcSingleNode( Abc_ManRst_t * p, Vec_Int_t * vSims, int nNodes, Vec_Int_t * vOnes )
-{
-    Dec_Graph_t * pGraph;
-    Dec_Edge_t eNode0, eNode1, eRoot;
-    unsigned uRoot;
-    int i, k;
-    uRoot = (unsigned)Vec_IntEntryLast( vSims );
-    for ( i = 0; i < vOnes->nSize; i++ )
-        for ( k = i+1; k < vOnes->nSize; k++ )
-            if ( ~uRoot == ((unsigned)vOnes->pArray[i] | (unsigned)vOnes->pArray[k]) )
-            {
-                eNode0 = Dec_IntToEdge( vOnes->pArray[i] ^ 1 );
-                eNode1 = Dec_IntToEdge( vOnes->pArray[k] ^ 1 );
-                pGraph = Dec_GraphCreate( 2 );
-                Dec_GraphNode( pGraph, 0 )->pFunc = Vec_PtrEntry( p->vDecs, eNode0.Node );
-                Dec_GraphNode( pGraph, 1 )->pFunc = Vec_PtrEntry( p->vDecs, eNode1.Node );
-                eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
-                Dec_GraphSetRoot( pGraph, eRoot );
-                if ( Abc_NodeCheckFull( p, pGraph ) )
-                    return pGraph;
-                Dec_GraphFree( pGraph );
-            }
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Detect single non-overlaps.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Graph_t * Abc_NodeMffcDoubleNode( Abc_ManRst_t * p, Vec_Int_t * vSims, int nNodes, Vec_Int_t * vOnes )
-{
-//    Dec_Graph_t * pGraph;
-//    unsigned uRoot, uNode;
-//    int i;
-
-
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Evaluates resubstution of one cut.]
-
-  Description [Returns the graph to add if any.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Graph_t * Abc_NodeResubEval( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut )
-{
-    Dec_Graph_t * pGraph;
-    int nNodesSaved;
-
-    // collect the nodes in the cut
-    if ( !Abc_Abc_NodeResubCollectDivs( p, pRoot, pCut ) )
-        return NULL;
-
-    // label MFFC and count its size
-    nNodesSaved = Abc_NodeResubMffc( p, p->vDecs, pCut->nLeaves, pRoot );
-    assert( nNodesSaved > 0 );
-
-    // simulate MFFC
-    Abc_NodeMffcSimulate( p->vDecs, pCut->nLeaves, p->vRands, p->vSims );
-
-    // check for constant output
-    pGraph = Abc_NodeMffcConstants( p, p->vSims );
-    if ( pGraph )
-    {
-        p->nNodesGained += nNodesSaved;
-        p->nNodesRestructured++;
-        return pGraph;
-    }
-
-    // check for one literal (fill up the ones array)
-    pGraph = Abc_NodeMffcSingleVar( p, p->vSims, Vec_IntSize(p->vSims) - nNodesSaved, p->vOnes );
-    if ( pGraph )
-    {
-        p->nNodesGained += nNodesSaved;
-        p->nNodesRestructured++;
-        return pGraph;
-    }
-    if ( nNodesSaved == 1 )
-        return NULL;
-
-    // look for one node
-    pGraph = Abc_NodeMffcSingleNode( p, p->vSims, Vec_IntSize(p->vSims) - nNodesSaved, p->vOnes );
-    if ( pGraph )
-    {
-        p->nNodesGained += nNodesSaved - 1;
-        p->nNodesRestructured++;
-        return pGraph;
-    }
-    if ( nNodesSaved == 2 )
-        return NULL;
-
-    // look for two nodes
-    pGraph = Abc_NodeMffcDoubleNode( p, p->vSims, Vec_IntSize(p->vSims) - nNodesSaved, p->vOnes );
-    if ( pGraph )
-    {
-        p->nNodesGained += nNodesSaved - 2;
-        p->nNodesRestructured++;
-        return pGraph;
-    }
-    if ( nNodesSaved == 3 )
-        return NULL;
-/*
-    // look for MUX/EXOR
-    pGraph = Abc_NodeMffcMuxNode( p, p->vSims, Vec_IntSize(p->vSims) - nNodesSaved );
-    if ( pGraph )
-    {
-        p->nNodesGained += nNodesSaved - 1;
-        p->nNodesRestructured++;
-        return pGraph;
-    }
-*/
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resubstution.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dec_Graph_t * Abc_NodeResubstitute( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList )
-{
-    Dec_Graph_t * pGraph, * pGraphBest = NULL;
-    Cut_Cut_t * pCut;
-    int nCuts;
-    p->nNodesConsidered++;
-
-    // count the number of cuts with four inputs or more
-    nCuts = 0;
-    for ( pCut = pCutList; pCut; pCut = pCut->pNext )
-        nCuts += (int)(pCut->nLeaves > 3);
-    printf( "-----------------------------------\n" );
-    printf( "Node %6d : Factor-cuts = %5d.\n", pNode->Id, nCuts );
-
-    // go through the interesting cuts
-    for ( pCut = pCutList; pCut; pCut = pCut->pNext )
-    {
-        if ( pCut->nLeaves < 4 )
-            continue;
-        pGraph = Abc_NodeResubEval( p, pNode, pCut );
-        if ( pGraph == NULL )
-            continue;
-        if ( !pGraphBest || Dec_GraphNodeNum(pGraph) < Dec_GraphNodeNum(pGraphBest) )
-        {
-            if ( pGraphBest ) 
-                Dec_GraphFree(pGraphBest);
-            pGraphBest = pGraph;
-        }
-        else
-            Dec_GraphFree(pGraph);
-    }
-    return pGraphBest;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-