src/aig/ivy/ivySeq.c

Go to the documentation of this file.

#include "ivy.h"
#include "deco.h"
#include "rwt.h"


static int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUseZeroCost );
static void Ivy_GraphPrepare( Dec_Graph_t * pGraph, Ivy_Cut_t * pCut, Vec_Ptr_t * vFanins, char * pPerm );
static unsigned Ivy_CutGetTruth( Ivy_Man_t * p, Ivy_Obj_t * pObj, int * pNums, int nNums );
static Dec_Graph_t * Rwt_CutEvaluateSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, char * pPerm, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int * pGainBest, unsigned uTruth );
static int Ivy_GraphToNetworkSeqCountSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax );
static Ivy_Obj_t * Ivy_GraphToNetworkSeq( Ivy_Man_t * p, Dec_Graph_t * pGraph );
static void Ivy_GraphUpdateNetworkSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain );
static Ivy_Store_t * Ivy_CutComputeForNode( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves );

static inline int Ivy_CutHashValue( int NodeId )  { return 1 << (NodeId % 31); }


//int nMoves;
//int nMovesS;
//int nClauses;
//int timeInv;

int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
{ 
    Rwt_Man_t * pManRwt;
    Ivy_Obj_t * pNode;
    int i, nNodes, nGain;
    int clk, clkStart = clock();

    // set the DC latch values
    Ivy_ManForEachLatch( p, pNode, i )
        pNode->Init = IVY_INIT_DC;
    // start the rewriting manager
    pManRwt = Rwt_ManStart( 0 );
    p->pData = pManRwt;
    if ( pManRwt == NULL )
        return 0; 
    // create fanouts
    if ( p->fFanout == 0 )
        Ivy_ManStartFanout( p );
    // resynthesize each node once
    nNodes = Ivy_ManObjIdMax(p);
    Ivy_ManForEachNode( p, pNode, i )
    {
        assert( !Ivy_ObjIsBuf(pNode) );
        assert( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) );
        assert( !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) );
        // fix the fanin buffer problem
//        Ivy_NodeFixBufferFanins( p, pNode );
//        if ( Ivy_ObjIsBuf(pNode) )
//            continue;
        // stop if all nodes have been tried once
        if ( i > nNodes ) 
            break;
        // for each cut, try to resynthesize it
        nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost );
        if ( nGain > 0 || nGain == 0 && fUseZeroCost )
        {
            Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt);
            int fCompl           = Rwt_ManReadCompl(pManRwt);
            // complement the FF if needed
clk = clock();
            if ( fCompl ) Dec_GraphComplement( pGraph );
            Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain );
            if ( fCompl ) Dec_GraphComplement( pGraph );
Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
        }
    }
Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
    // print stats
    if ( fVerbose )
        Rwt_ManPrintStats( pManRwt );
    // delete the managers
    Rwt_ManStop( pManRwt );
    p->pData = NULL;
    // fix the levels
    Ivy_ManResetLevels( p );
//    if ( Ivy_ManCheckFanoutNums(p) )
//        printf( "Ivy_ManRewritePre(): The check has failed.\n" );
    // check
    if ( !Ivy_ManCheck(p) )
        printf( "Ivy_ManRewritePre(): The check has failed.\n" );
    return 1;
}


int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUseZeroCost )
{
    int fVeryVerbose = 0;
    Dec_Graph_t * pGraph;
    Ivy_Store_t * pStore;
    Ivy_Cut_t * pCut;
    Ivy_Obj_t * pFanin;//, * pFanout;
    Vec_Ptr_t * vFanout;
    unsigned uPhase, uTruthBest, uTruth;//, nNewClauses;
    char * pPerm;
    int nNodesSaved, nNodesSaveCur;
    int i, c, GainCur, GainBest = -1;
    int clk, clk2;//, clk3;

    p->nNodesConsidered++;
    // get the node's cuts
clk = clock();
    pStore = Ivy_CutComputeForNode( pMan, pNode, 5 );
p->timeCut += clock() - clk;

    // go through the cuts
clk = clock();
    vFanout = Vec_PtrAlloc( 100 );
    for ( c = 1; c < pStore->nCuts; c++ )
    {
        pCut = pStore->pCuts + c;
        // consider only 4-input cuts
        if ( pCut->nSize != 4 )
            continue;
        // skip the cuts with buffers
        for ( i = 0; i < (int)pCut->nSize; i++ )
            if ( Ivy_ObjIsBuf( Ivy_ManObj(pMan, Ivy_LeafId(pCut->pArray[i])) ) )
                break;
        if ( i != pCut->nSize )
        {
            p->nCutsBad++;
            continue;
        }
        p->nCutsGood++;
        // get the fanin permutation
clk2 = clock();
        uTruth = 0xFFFF & Ivy_CutGetTruth( pMan, pNode, pCut->pArray, pCut->nSize );  // truth table
p->timeTruth += clock() - clk2;
        pPerm = p->pPerms4[ p->pPerms[uTruth] ];
        uPhase = p->pPhases[uTruth];
        // collect fanins with the corresponding permutation/phase
        Vec_PtrClear( p->vFaninsCur );
        Vec_PtrFill( p->vFaninsCur, (int)pCut->nSize, 0 );
        for ( i = 0; i < (int)pCut->nSize; i++ )
        {
            pFanin = Ivy_ManObj( pMan, Ivy_LeafId( pCut->pArray[pPerm[i]] ) );
            assert( Ivy_ObjIsNode(pFanin) || Ivy_ObjIsCi(pFanin) || Ivy_ObjIsConst1(pFanin) );
            pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
            Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
        }
clk2 = clock();
        // mark the fanin boundary 
        Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
            Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
        // label MFFC with current ID
        Ivy_ManIncrementTravId( pMan );
        nNodesSaved = Ivy_ObjMffcLabel( pMan, pNode );
        // label fanouts with the current ID
//        Ivy_ObjForEachFanout( pMan, pNode, vFanout, pFanout, i )
//            Ivy_ObjSetTravIdCurrent( pMan, pFanout );
        // unmark the fanin boundary
        Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
            Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
p->timeMffc += clock() - clk2;

        // evaluate the cut
clk2 = clock();
        pGraph = Rwt_CutEvaluateSeq( pMan, p, pNode, pCut, pPerm, p->vFaninsCur, nNodesSaved, &GainCur, uTruth );
p->timeEval += clock() - clk2;


        // check if the cut is better than the current best one
        if ( pGraph != NULL && GainBest < GainCur )
        {
            // save this form
            nNodesSaveCur = nNodesSaved;
            GainBest   = GainCur;
            p->pGraph  = pGraph;
            p->pCut    = pCut;
            p->pPerm   = pPerm;
            p->fCompl  = ((uPhase & (1<<4)) > 0);
            uTruthBest = uTruth;
            // collect fanins in the
            Vec_PtrClear( p->vFanins );
            Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
                Vec_PtrPush( p->vFanins, pFanin );
        }
    }
    Vec_PtrFree( vFanout );
p->timeRes += clock() - clk;

    if ( GainBest == -1 )
        return -1;
/*
    {
    Ivy_Cut_t * pCut = p->pCut;
    printf( "Node %5d. Using cut : {", Ivy_ObjId(pNode) );
    for ( i = 0; i < pCut->nSize; i++ )
        printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
    printf( " }\n" );
    }
*/

//clk3 = clock();
//nNewClauses = Ivy_CutTruthPrint( pMan, p->pCut, uTruth );
//timeInv += clock() - clk;

//    nClauses += nNewClauses;
//    nMoves++;
//    if ( nNewClauses > 0 )
//        nMovesS++;

    // copy the leaves
    Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm );

    p->nScores[p->pMap[uTruthBest]]++;
    p->nNodesGained += GainBest;
    if ( fUseZeroCost || GainBest > 0 )
        p->nNodesRewritten++;

/*
    if ( GainBest > 0 )
    {
        Ivy_Cut_t * pCut = p->pCut;
        printf( "Node %5d. Using cut : {", Ivy_ObjId(pNode) );
        for ( i = 0; i < pCut->nSize; i++ )
            printf( " %5d(%2d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
        printf( " }\n" );
    }
*/

    // report the progress
    if ( fVeryVerbose && GainBest > 0 )
    {
        printf( "Node %6d :   ", Ivy_ObjId(pNode) );
        printf( "Fanins = %d. ", p->vFanins->nSize );
        printf( "Save = %d.  ", nNodesSaveCur );
        printf( "Add = %d.  ",  nNodesSaveCur-GainBest );
        printf( "GAIN = %d.  ", GainBest );
        printf( "Cone = %d.  ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 );
        printf( "Class = %d.  ", p->pMap[uTruthBest] );
        printf( "\n" );
    }
    return GainBest;
}


Dec_Graph_t * Rwt_CutEvaluateSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, char * pPerm, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int * pGainBest, unsigned uTruth )
{
    Vec_Ptr_t * vSubgraphs;
    Dec_Graph_t * pGraphBest, * pGraphCur;
    Rwt_Node_t * pNode;
    int nNodesAdded, GainBest, i;
    // find the matching class of subgraphs
    vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] );
    p->nSubgraphs += vSubgraphs->nSize;
    // determine the best subgraph
    GainBest = -1;
    Vec_PtrForEachEntry( vSubgraphs, pNode, i )
    {
        // get the current graph
        pGraphCur = (Dec_Graph_t *)pNode->pNext;

//        if ( pRoot->Id == 8648 )
//        Dec_GraphPrint( stdout, pGraphCur, NULL, NULL );
        // copy the leaves
//        Vec_PtrForEachEntry( vFaninsCur, pFanin, k )
//            Dec_GraphNode(pGraphCur, k)->pFunc = pFanin;
        Ivy_GraphPrepare( pGraphCur, pCut, vFaninsCur, pPerm );

        // detect how many unlabeled nodes will be reused
        nNodesAdded = Ivy_GraphToNetworkSeqCountSeq( pMan, pRoot, pGraphCur, nNodesSaved );
        if ( nNodesAdded == -1 )
            continue;
        assert( nNodesSaved >= nNodesAdded );
        // count the gain at this node
        if ( GainBest < nNodesSaved - nNodesAdded )
        {
            GainBest   = nNodesSaved - nNodesAdded;
            pGraphBest = pGraphCur;
        }
    }
    if ( GainBest == -1 )
        return NULL;
    *pGainBest = GainBest;
    return pGraphBest;
}

void Ivy_GraphPrepare( Dec_Graph_t * pGraph, Ivy_Cut_t * pCut, Vec_Ptr_t * vFanins, char * pPerm )
{
    Dec_Node_t * pNode, * pNode0, * pNode1;
    int i;
    assert( Dec_GraphLeaveNum(pGraph) == pCut->nSize );
    assert( Vec_PtrSize(vFanins) == pCut->nSize );
    // label the leaves with latch numbers
    Dec_GraphForEachLeaf( pGraph, pNode, i )
    {
        pNode->pFunc = Vec_PtrEntry( vFanins, i );
        pNode->nLat2 = Ivy_LeafLat( pCut->pArray[pPerm[i]] );
    }
    // propagate latches through the nodes
    Dec_GraphForEachNode( pGraph, pNode, i )
    {
        // get the children of this node
        pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
        pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
        // distribute the latches
        pNode->nLat2 = IVY_MIN( pNode0->nLat2, pNode1->nLat2 );
        pNode->nLat0 = pNode0->nLat2 - pNode->nLat2;
        pNode->nLat1 = pNode1->nLat2 - pNode->nLat2;
    }
}

int Ivy_GraphToNetworkSeqCountSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax )
{
    Dec_Node_t * pNode, * pNode0, * pNode1;
    Ivy_Obj_t * pAnd, * pAnd0, * pAnd1;
    int i, k, Counter, fCompl;
    // check for constant function or a literal
    if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) )
        return 0;
    // compute the AIG size after adding the internal nodes
    Counter = 0;
    Dec_GraphForEachNode( pGraph, pNode, i )
    {
        // get the children of this node
        pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
        pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
        // get the AIG nodes corresponding to the children 
        pAnd0 = pNode0->pFunc; 
        pAnd1 = pNode1->pFunc; 
        // skip the latches
        for ( k = 0; pAnd0 && k < (int)pNode->nLat0; k++ )
        {
            fCompl = Ivy_IsComplement(pAnd0);
            pAnd0 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Regular(pAnd0), NULL, IVY_LATCH, IVY_INIT_DC) );
            if ( pAnd0 )
                pAnd0 = Ivy_NotCond( pAnd0, fCompl );
        }
        for ( k = 0; pAnd1 && k < (int)pNode->nLat1; k++ )
        {
            fCompl = Ivy_IsComplement(pAnd1);
            pAnd1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Regular(pAnd1), NULL, IVY_LATCH, IVY_INIT_DC) );
            if ( pAnd1 )
                pAnd1 = Ivy_NotCond( pAnd1, fCompl );
        }
        // get the new node
        if ( pAnd0 && pAnd1 )
        {
            // if they are both present, find the resulting node
            pAnd0 = Ivy_NotCond( pAnd0, pNode->eEdge0.fCompl );
            pAnd1 = Ivy_NotCond( pAnd1, pNode->eEdge1.fCompl );
            assert( !Ivy_ObjIsLatch(Ivy_Regular(pAnd0)) || !Ivy_ObjIsLatch(Ivy_Regular(pAnd1)) );
            if ( Ivy_Regular(pAnd0) == Ivy_Regular(pAnd1) || Ivy_ObjIsConst1(Ivy_Regular(pAnd0)) || Ivy_ObjIsConst1(Ivy_Regular(pAnd1)) )
                pAnd = Ivy_And( p, pAnd0, pAnd1 );
            else
                pAnd = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) );
            // return -1 if the node is the same as the original root
            if ( Ivy_Regular(pAnd) == pRoot )
                return -1;
        }
        else
            pAnd = NULL;
        // count the number of added nodes
        if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(p, Ivy_Regular(pAnd)) )
        {
            if ( ++Counter > NodeMax )
                return -1;
        }
        pNode->pFunc = pAnd;
    }
    return Counter;
}


Ivy_Obj_t * Ivy_GraphToNetworkSeq( Ivy_Man_t * p, Dec_Graph_t * pGraph )
{
    Ivy_Obj_t * pAnd0, * pAnd1;
    Dec_Node_t * pNode;
    int i, k;
    // check for constant function
    if ( Dec_GraphIsConst(pGraph) )
        return Ivy_NotCond( Ivy_ManConst1(p), Dec_GraphIsComplement(pGraph) );
    // check for a literal
    if ( Dec_GraphIsVar(pGraph) )
    {
        // get the variable node
        pNode = Dec_GraphVar(pGraph);
        // add the remaining latches
        for ( k = 0; k < (int)pNode->nLat2; k++ )
            pNode->pFunc = Ivy_Latch( p, pNode->pFunc, IVY_INIT_DC );
        return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
    }
    // build the AIG nodes corresponding to the AND gates of the graph
    Dec_GraphForEachNode( pGraph, pNode, i )
    {
        pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
        pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
        // add the latches
        for ( k = 0; k < (int)pNode->nLat0; k++ )
            pAnd0 = Ivy_Latch( p, pAnd0, IVY_INIT_DC );
        for ( k = 0; k < (int)pNode->nLat1; k++ )
            pAnd1 = Ivy_Latch( p, pAnd1, IVY_INIT_DC );
        // create the node
        pNode->pFunc = Ivy_And( p, pAnd0, pAnd1 );
    }
    // add the remaining latches
    for ( k = 0; k < (int)pNode->nLat2; k++ )
        pNode->pFunc = Ivy_Latch( p, pNode->pFunc, IVY_INIT_DC );
    // complement the result if necessary
    return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
}

void Ivy_GraphUpdateNetworkSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain )
{
    Ivy_Obj_t * pRootNew;
    int nNodesNew, nNodesOld;
    nNodesOld = Ivy_ManNodeNum(p);
    // create the new structure of nodes
    pRootNew = Ivy_GraphToNetworkSeq( p, pGraph );
    Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0, 0 );
    // compare the gains
    nNodesNew = Ivy_ManNodeNum(p);
    assert( nGain <= nNodesOld - nNodesNew );
    // propagate the buffer
    Ivy_ManPropagateBuffers( p, 0 );
}









unsigned Ivy_CutGetTruth_rec( Ivy_Man_t * p, int Leaf, int * pNums, int nNums )
{
    static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
    unsigned uTruth0, uTruth1;
    Ivy_Obj_t * pObj;
    int i;
    for ( i = 0; i < nNums; i++ )
        if ( Leaf == pNums[i] )
            return uMasks[i];
    pObj = Ivy_ManObj( p, Ivy_LeafId(Leaf) );
    if ( Ivy_ObjIsLatch(pObj) )
    {
        assert( !Ivy_ObjFaninC0(pObj) );
        Leaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pObj), Ivy_LeafLat(Leaf) + 1 );
        return Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
    }
    assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
    Leaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pObj), Ivy_LeafLat(Leaf) );
    uTruth0 = Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
    if ( Ivy_ObjFaninC0(pObj) )
        uTruth0 = ~uTruth0;
    if ( Ivy_ObjIsBuf(pObj) )
        return uTruth0;
    Leaf = Ivy_LeafCreate( Ivy_ObjFaninId1(pObj), Ivy_LeafLat(Leaf) );
    uTruth1 = Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums );
    if ( Ivy_ObjFaninC1(pObj) )
        uTruth1 = ~uTruth1;
    return uTruth0 & uTruth1;
}


unsigned Ivy_CutGetTruth( Ivy_Man_t * p, Ivy_Obj_t * pObj, int * pNums, int nNums )
{
    assert( Ivy_ObjIsNode(pObj) );
    assert( nNums < 6 );
    return Ivy_CutGetTruth_rec( p, Ivy_LeafCreate(pObj->Id, 0), pNums, nNums );
}





static inline int Ivy_CutPrescreen( Ivy_Cut_t * pCut, int Id0, int Id1 )
{
    int i;
    if ( pCut->nSize < pCut->nSizeMax )
        return 1;
    for ( i = 0; i < pCut->nSize; i++ )
        if ( pCut->pArray[i] == Id0 || pCut->pArray[i] == Id1 )
            return 1;
    return 0;
}

static inline int Ivy_CutDeriveNew2( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
{
    unsigned uHash = 0;
    int i, k;
    assert( pCut->nSize > 0 );
    assert( IdNew0 < IdNew1 );
    for ( i = k = 0; i < pCut->nSize; i++ )
    {
        if ( pCut->pArray[i] == IdOld )
            continue;
        if ( IdNew0 >= 0 )
        {
            if ( IdNew0 <= pCut->pArray[i] )
            {
                if ( IdNew0 < pCut->pArray[i] )
                {
                    if ( k == pCut->nSizeMax )
                        return 0;
                    pCutNew->pArray[ k++ ] = IdNew0;
                    uHash |= Ivy_CutHashValue( IdNew0 );
                }
                IdNew0 = -1;
            }
        }
        if ( IdNew1 >= 0 )
        {
            if ( IdNew1 <= pCut->pArray[i] )
            {
                if ( IdNew1 < pCut->pArray[i] )
                {
                    if ( k == pCut->nSizeMax )
                        return 0;
                    pCutNew->pArray[ k++ ] = IdNew1;
                    uHash |= Ivy_CutHashValue( IdNew1 );
                }
                IdNew1 = -1;
            }
        }
        if ( k == pCut->nSizeMax )
            return 0;
        pCutNew->pArray[ k++ ] = pCut->pArray[i];
        uHash |= Ivy_CutHashValue( pCut->pArray[i] );
    }
    if ( IdNew0 >= 0 )
    {
        if ( k == pCut->nSizeMax )
            return 0;
        pCutNew->pArray[ k++ ] = IdNew0;
        uHash |= Ivy_CutHashValue( IdNew0 );
    }
    if ( IdNew1 >= 0 )
    {
        if ( k == pCut->nSizeMax )
            return 0;
        pCutNew->pArray[ k++ ] = IdNew1;
        uHash |= Ivy_CutHashValue( IdNew1 );
    }
    pCutNew->nSize = k;
    pCutNew->uHash = uHash;
    assert( pCutNew->nSize <= pCut->nSizeMax );
    for ( i = 1; i < pCutNew->nSize; i++ )
        assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] );
    return 1;
}

static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
{
    unsigned uHash = 0;
    int i, k; 
    assert( pCut->nSize > 0 );
    assert( IdNew0 < IdNew1 );
    for ( i = k = 0; i < pCut->nSize; i++ )
    {
        if ( pCut->pArray[i] == IdOld )
            continue;
        if ( IdNew0 <= pCut->pArray[i] )
        {
            if ( IdNew0 < pCut->pArray[i] )
            {
                pCutNew->pArray[ k++ ] = IdNew0;
                uHash |= Ivy_CutHashValue( IdNew0 );
            }
            IdNew0 = 0x7FFFFFFF;
        }
        if ( IdNew1 <= pCut->pArray[i] )
        {
            if ( IdNew1 < pCut->pArray[i] )
            {
                pCutNew->pArray[ k++ ] = IdNew1;
                uHash |= Ivy_CutHashValue( IdNew1 );
            }
            IdNew1 = 0x7FFFFFFF;
        }
        pCutNew->pArray[ k++ ] = pCut->pArray[i];
        uHash |= Ivy_CutHashValue( pCut->pArray[i] );
    }
    if ( IdNew0 < 0x7FFFFFFF )
    {
        pCutNew->pArray[ k++ ] = IdNew0;
        uHash |= Ivy_CutHashValue( IdNew0 );
    }
    if ( IdNew1 < 0x7FFFFFFF )
    {
        pCutNew->pArray[ k++ ] = IdNew1;
        uHash |= Ivy_CutHashValue( IdNew1 );
    }
    pCutNew->nSize = k;
    pCutNew->uHash = uHash;
    assert( pCutNew->nSize <= pCut->nSizeMax );
//    for ( i = 1; i < pCutNew->nSize; i++ )
//        assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] );
    return 1;
}

static inline unsigned Ivy_NodeCutHash( Ivy_Cut_t * pCut )
{
    int i;
    pCut->uHash = 0;
    for ( i = 0; i < pCut->nSize; i++ )
        pCut->uHash |= (1 << (pCut->pArray[i] % 31));
    return pCut->uHash;
}

static inline int Ivy_CutDeriveNew3( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
{
    int i, k; 
    assert( pCut->nSize > 0 );
    assert( IdNew0 < IdNew1 );
    for ( i = k = 0; i < pCut->nSize; i++ )
    {
        if ( pCut->pArray[i] == IdOld )
            continue;
        if ( IdNew0 <= pCut->pArray[i] )
        {
            if ( IdNew0 < pCut->pArray[i] )
                pCutNew->pArray[ k++ ] = IdNew0;
            IdNew0 = 0x7FFFFFFF;
        }
        if ( IdNew1 <= pCut->pArray[i] )
        {
            if ( IdNew1 < pCut->pArray[i] )
                pCutNew->pArray[ k++ ] = IdNew1;
            IdNew1 = 0x7FFFFFFF;
        }
        pCutNew->pArray[ k++ ] = pCut->pArray[i];
    }
    if ( IdNew0 < 0x7FFFFFFF )
        pCutNew->pArray[ k++ ] = IdNew0;
    if ( IdNew1 < 0x7FFFFFFF )
        pCutNew->pArray[ k++ ] = IdNew1;
    pCutNew->nSize = k;
    assert( pCutNew->nSize <= pCut->nSizeMax );
    Ivy_NodeCutHash( pCutNew );
    return 1;
}

static inline int Ivy_CutCheckDominance( Ivy_Cut_t * pDom, Ivy_Cut_t * pCut )
{
    int i, k;
    for ( i = 0; i < pDom->nSize; i++ )
    {
        assert( i==0 || pDom->pArray[i-1] < pDom->pArray[i] );
        for ( k = 0; k < pCut->nSize; k++ )
            if ( pDom->pArray[i] == pCut->pArray[k] )
                break;
        if ( k == pCut->nSize ) // node i in pDom is not contained in pCut
            return 0;
    }
    // every node in pDom is contained in pCut
    return 1;
}

int Ivy_CutFindOrAddFilter( Ivy_Store_t * pCutStore, Ivy_Cut_t * pCutNew )
{
    Ivy_Cut_t * pCut;
    int i, k;
    assert( pCutNew->uHash );
    // try to find the cut
    for ( i = 0; i < pCutStore->nCuts; i++ )
    {
        pCut = pCutStore->pCuts + i;
        if ( pCut->nSize == 0 )
            continue;
        if ( pCut->nSize == pCutNew->nSize )
        {
            if ( pCut->uHash == pCutNew->uHash )
            {
                for ( k = 0; k < pCutNew->nSize; k++ )
                    if ( pCut->pArray[k] != pCutNew->pArray[k] )
                        break;
                if ( k == pCutNew->nSize )
                    return 1;
            }
            continue;
        }
        if ( pCut->nSize < pCutNew->nSize )
        {
            // skip the non-contained cuts
            if ( (pCut->uHash & pCutNew->uHash) != pCut->uHash )
                continue;
            // check containment seriously
            if ( Ivy_CutCheckDominance( pCut, pCutNew ) )
                return 1;
            continue;
        }
        // check potential containment of other cut

        // skip the non-contained cuts
        if ( (pCut->uHash & pCutNew->uHash) != pCutNew->uHash )
            continue;
        // check containment seriously
        if ( Ivy_CutCheckDominance( pCutNew, pCut ) )
        {
            // remove the current cut
            pCut->nSize = 0;
        }
    }
    assert( pCutStore->nCuts < pCutStore->nCutsMax );
    // add the cut
    pCut = pCutStore->pCuts + pCutStore->nCuts++;
    *pCut = *pCutNew;
    return 0;
}

void Ivy_CutCompactAll( Ivy_Store_t * pCutStore )
{
    Ivy_Cut_t * pCut;
    int i, k;
    pCutStore->nCutsM = 0;
    for ( i = k = 0; i < pCutStore->nCuts; i++ )
    {
        pCut = pCutStore->pCuts + i;
        if ( pCut->nSize == 0 )
            continue;
        if ( pCut->nSize < pCut->nSizeMax )
            pCutStore->nCutsM++;
        pCutStore->pCuts[k++] = *pCut;
    }
    pCutStore->nCuts = k;
}

void Ivy_CutPrintForNode( Ivy_Cut_t * pCut )
{
    int i;
    assert( pCut->nSize > 0 );
    printf( "%d : {", pCut->nSize );
    for ( i = 0; i < pCut->nSize; i++ )
        printf( " %d", pCut->pArray[i] );
    printf( " }\n" );
}

void Ivy_CutPrintForNodes( Ivy_Store_t * pCutStore )
{
    int i;
    printf( "Node %d\n", pCutStore->pCuts[0].pArray[0] );
    for ( i = 0; i < pCutStore->nCuts; i++ )
        Ivy_CutPrintForNode( pCutStore->pCuts + i );
}

static inline int Ivy_CutReadLeaf( Ivy_Obj_t * pFanin )
{
    int nLats, iLeaf;
    assert( !Ivy_IsComplement(pFanin) );
    if ( !Ivy_ObjIsLatch(pFanin) )
        return Ivy_LeafCreate( pFanin->Id, 0 );
    iLeaf = Ivy_CutReadLeaf(Ivy_ObjFanin0(pFanin));
    nLats = Ivy_LeafLat(iLeaf);
    assert( nLats < IVY_LEAF_MASK );
    return 1 + iLeaf;
}

Ivy_Store_t * Ivy_CutComputeForNode( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves )
{
    static Ivy_Store_t CutStore, * pCutStore = &CutStore;
    Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
    Ivy_Man_t * pMan = p;
    Ivy_Obj_t * pLeaf;
    int i, k, Temp, nLats, iLeaf0, iLeaf1;

    assert( nLeaves <= IVY_CUT_INPUT );

    // start the structure
    pCutStore->nCuts = 0;
    pCutStore->nCutsMax = IVY_CUT_LIMIT;
    // start the trivial cut
    pCutNew->uHash = 0;
    pCutNew->nSize = 1;
    pCutNew->nSizeMax = nLeaves;
    pCutNew->pArray[0] = Ivy_LeafCreate( pObj->Id, 0 );
    pCutNew->uHash = Ivy_CutHashValue( pCutNew->pArray[0] );
    // add the trivial cut
    pCutStore->pCuts[pCutStore->nCuts++] = *pCutNew;
    assert( pCutStore->nCuts == 1 );

    // explore the cuts
    for ( i = 0; i < pCutStore->nCuts; i++ )
    {
        // expand this cut
        pCut = pCutStore->pCuts + i;
        if ( pCut->nSize == 0 )
            continue;
        for ( k = 0; k < pCut->nSize; k++ )
        {
            pLeaf = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[k]) );
            if ( Ivy_ObjIsCi(pLeaf) || Ivy_ObjIsConst1(pLeaf) )
                continue;
            assert( Ivy_ObjIsNode(pLeaf) );
            nLats = Ivy_LeafLat(pCut->pArray[k]);

            // get the fanins fanins
            iLeaf0 = Ivy_CutReadLeaf( Ivy_ObjFanin0(pLeaf) );
            iLeaf1 = Ivy_CutReadLeaf( Ivy_ObjFanin1(pLeaf) );
            assert( nLats + Ivy_LeafLat(iLeaf0) < IVY_LEAF_MASK && nLats + Ivy_LeafLat(iLeaf1) < IVY_LEAF_MASK );
            iLeaf0 = nLats + iLeaf0;
            iLeaf1 = nLats + iLeaf1;
            if ( !Ivy_CutPrescreen( pCut, iLeaf0, iLeaf1 ) )
                continue;
            // the given cut exist
            if ( iLeaf0 > iLeaf1 )
                Temp = iLeaf0, iLeaf0 = iLeaf1, iLeaf1 = Temp;
            // create the new cut
            if ( !Ivy_CutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 ) )
                continue;
            // add the cut
            Ivy_CutFindOrAddFilter( pCutStore, pCutNew );
            if ( pCutStore->nCuts == IVY_CUT_LIMIT )
                break;
        }
        if ( pCutStore->nCuts == IVY_CUT_LIMIT )
            break;
    }
    if ( pCutStore->nCuts == IVY_CUT_LIMIT )
        pCutStore->fSatur = 1;
    else
        pCutStore->fSatur = 0;
//    printf( "%d ", pCutStore->nCuts );
    Ivy_CutCompactAll( pCutStore );
//    printf( "%d \n", pCutStore->nCuts );
//    Ivy_CutPrintForNodes( pCutStore );
    return pCutStore;
}

void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs )
{
    Ivy_Store_t * pStore;
    Ivy_Obj_t * pObj;
    int i, nCutsTotal, nCutsTotalM, nNodeTotal, nNodeOver;
    int clk = clock();
    if ( nInputs > IVY_CUT_INPUT )
    {
        printf( "Cannot compute cuts for more than %d inputs.\n", IVY_CUT_INPUT );
        return;
    }
    nNodeTotal = nNodeOver = 0;
    nCutsTotal = nCutsTotalM = -Ivy_ManNodeNum(p);
    Ivy_ManForEachObj( p, pObj, i )
    {
        if ( !Ivy_ObjIsNode(pObj) )
            continue;
        pStore = Ivy_CutComputeForNode( p, pObj, nInputs );
        nCutsTotal  += pStore->nCuts;
        nCutsTotalM += pStore->nCutsM;
        nNodeOver   += pStore->fSatur;
        nNodeTotal++;
    }
    printf( "All = %6d. Minus = %6d. Triv = %6d.   Node = %6d. Satur = %6d.  ", 
        nCutsTotal, nCutsTotalM, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
    PRT( "Time", clock() - clk );
}

---