path: root/src/base/abci/abcRestruct.c

/**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                              ///
////////////////////////////////////////////////////////////////////////
  
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
    // 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_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 fMulti );
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 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 );

    // 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 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 ); 
pManRst->timeCut += clock() - clk;
        // evaluate these cuts
clk = clock();
        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_NtkGetLevelNum( 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 )
{
    Abc_Obj_t * pNode, * pFanin, * pFanout;
    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" );
    }
}


/**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_NodeReadRequiredLevel(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 );
    }
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_NodeMffcLabel( pRoot );
    // unmark the fanin boundary and set the fanins as leaves in the form
    Vec_PtrForEachEntry( p->vLeaves, pLeaf, i )
        pLeaf->vFanouts.nSize--;


    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;
    }

    // detect how many new nodes will be added (while taking into account reused nodes)
clk = clock();
    pGraph = Abc_NodeEvaluateDsd( p, pNodeDsd, pRoot, Required, nNodesSaved, &nNodesAdded );
//    pGraph = NULL;
p->timeEval += clock() - clk;

    // quit if there is no improvement
    if ( 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 fMulti )
{
    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->fMulti    = fMulti;  // compute factor-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 );
    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 );
    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 );
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////