ivySeq.c File Reference

#include "ivy.h"
#include "bool/deco/deco.h"
#include "opt/rwt/rwt.h"

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START int	Ivy_NodeRewriteSeq (Ivy_Man_t *pMan, Rwt_Man_t *p, Ivy_Obj_t *pNode, int fUseZeroCost)
	DECLARATIONS ///. More...
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 int	Ivy_CutHashValue (int NodeId)
int	Ivy_ManRewriteSeq (Ivy_Man_t *p, int fUseZeroCost, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
unsigned	Ivy_CutGetTruth_rec (Ivy_Man_t *p, int Leaf, int *pNums, int nNums)
static int	Ivy_CutPrescreen (Ivy_Cut_t *pCut, int Id0, int Id1)
static int	Ivy_CutDeriveNew2 (Ivy_Cut_t *pCut, Ivy_Cut_t *pCutNew, int IdOld, int IdNew0, int IdNew1)
static int	Ivy_CutDeriveNew (Ivy_Cut_t *pCut, Ivy_Cut_t *pCutNew, int IdOld, int IdNew0, int IdNew1)
static unsigned	Ivy_NodeCutHash (Ivy_Cut_t *pCut)
static int	Ivy_CutDeriveNew3 (Ivy_Cut_t *pCut, Ivy_Cut_t *pCutNew, int IdOld, int IdNew0, int IdNew1)
static int	Ivy_CutCheckDominance (Ivy_Cut_t *pDom, Ivy_Cut_t *pCut)
int	Ivy_CutFindOrAddFilter (Ivy_Store_t *pCutStore, Ivy_Cut_t *pCutNew)
void	Ivy_CutCompactAll (Ivy_Store_t *pCutStore)
void	Ivy_CutPrintForNode (Ivy_Cut_t *pCut)
void	Ivy_CutPrintForNodes (Ivy_Store_t *pCutStore)
static int	Ivy_CutReadLeaf (Ivy_Obj_t *pFanin)
void	Ivy_CutComputeAll (Ivy_Man_t *p, int nInputs)

Function Documentation

static int Ivy_CutCheckDominance ( Ivy_Cut_t *  pDom, Ivy_Cut_t *  pCut  )

inlinestatic

Function*************************************************************

Synopsis [Returns 1 if pDom is contained in pCut.]

Description []

SideEffects []

SeeAlso []

Definition at line 846 of file ivySeq.c.

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

void Ivy_CutCompactAll

(

Ivy_Store_t *

pCutStore

)

Function*************************************************************

Synopsis [Compresses the cut representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 936 of file ivySeq.c.

{
    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_CutComputeAll	(	Ivy_Man_t *	p,
		int	nInputs
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1108 of file ivySeq.c.

{
    Ivy_Store_t * pStore;
    Ivy_Obj_t * pObj;
    int i, nCutsTotal, nCutsTotalM, nNodeTotal, nNodeOver;
    abctime clk = Abc_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 );
    ABC_PRT( "Time", Abc_Clock() - clk );
}

Ivy_Store_t * Ivy_CutComputeForNode ( Ivy_Man_t *  p, Ivy_Obj_t *  pObj, int  nLeaves  )

static

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1027 of file ivySeq.c.

{
    static Ivy_Store_t CutStore, * pCutStore = &CutStore;
    Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
    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;
}

static int Ivy_CutDeriveNew ( Ivy_Cut_t *  pCut, Ivy_Cut_t *  pCutNew, int  IdOld, int  IdNew0, int  IdNew1  )

inlinestatic

Function*************************************************************

Synopsis [Derives new cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 722 of file ivySeq.c.

{
    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 int Ivy_CutDeriveNew2 ( Ivy_Cut_t *  pCut, Ivy_Cut_t *  pCutNew, int  IdOld, int  IdNew0, int  IdNew1  )

inlinestatic

Function*************************************************************

Synopsis [Derives new cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 646 of file ivySeq.c.

{
    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 int Ivy_CutDeriveNew3 ( Ivy_Cut_t *  pCut, Ivy_Cut_t *  pCutNew, int  IdOld, int  IdNew0, int  IdNew1  )

inlinestatic

Function*************************************************************

Synopsis [Derives new cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 802 of file ivySeq.c.

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

int Ivy_CutFindOrAddFilter	(	Ivy_Store_t *	pCutStore,
		Ivy_Cut_t *	pCutNew
	)

Function*************************************************************

Synopsis [Check if the cut exists.]

Description [Returns 1 if the cut exists.]

SideEffects []

SeeAlso []

Definition at line 873 of file ivySeq.c.

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

unsigned Ivy_CutGetTruth ( Ivy_Man_t *  p, Ivy_Obj_t *  pObj, int *  pNums, int  nNums  )

static

Function*************************************************************

Synopsis [Computes the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 602 of file ivySeq.c.

{
    assert( Ivy_ObjIsNode(pObj) );
    assert( nNums < 6 );
    return Ivy_CutGetTruth_rec( p, Ivy_LeafCreate(pObj->Id, 0), pNums, nNums );
}

unsigned Ivy_CutGetTruth_rec	(	Ivy_Man_t *	p,
		int	Leaf,
		int *	pNums,
		int	nNums
	)

Function*************************************************************

Synopsis [Computes the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 560 of file ivySeq.c.

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

static int Ivy_CutHashValue ( int  NodeId )

inlinestatic

Definition at line 41 of file ivySeq.c.

{ return 1 << (NodeId % 31); }

static int Ivy_CutPrescreen ( Ivy_Cut_t *  pCut, int  Id0, int  Id1  )

inlinestatic

Function*************************************************************

Synopsis [Returns 1 if the cut can be constructed; 0 otherwise.]

Description []

SideEffects []

SeeAlso []

Definition at line 624 of file ivySeq.c.

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

void Ivy_CutPrintForNode

(

Ivy_Cut_t *

pCut

)

Function*************************************************************

Synopsis [Print the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 964 of file ivySeq.c.

{
    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

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 985 of file ivySeq.c.

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

static int Ivy_CutReadLeaf ( Ivy_Obj_t *  pFanin )

inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1004 of file ivySeq.c.

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

void Ivy_GraphPrepare ( Dec_Graph_t *  pGraph, Ivy_Cut_t *  pCut, Vec_Ptr_t *  vFanins, char *  pPerm  )

static

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 364 of file ivySeq.c.

{
    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[(int)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;
    }
}

Ivy_Obj_t * Ivy_GraphToNetworkSeq ( Ivy_Man_t *  p, Dec_Graph_t *  pGraph  )

static

Function*************************************************************

Synopsis [Transforms the decomposition graph into the AIG.]

Description [AIG nodes for the fanins should be assigned to pNode->pFunc of the leaves of the graph before calling this procedure.]

SideEffects []

SeeAlso []

Definition at line 477 of file ivySeq.c.

{
    Ivy_Obj_t * pAnd0, * pAnd1;
    Dec_Node_t * pNode = NULL; // Suppress "might be used uninitialized"
    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, (Ivy_Obj_t *)pNode->pFunc, IVY_INIT_DC );
        return Ivy_NotCond( (Ivy_Obj_t *)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( (Ivy_Obj_t *)Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
        pAnd1 = Ivy_NotCond( (Ivy_Obj_t *)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, (Ivy_Obj_t *)pNode->pFunc, IVY_INIT_DC );
    // complement the result if necessary
    return Ivy_NotCond( (Ivy_Obj_t *)pNode->pFunc, Dec_GraphIsComplement(pGraph) );
}

int Ivy_GraphToNetworkSeqCountSeq ( Ivy_Man_t *  p, Ivy_Obj_t *  pRoot, Dec_Graph_t *  pGraph, int  NodeMax  )

static

Function*************************************************************

Synopsis [Counts the number of new nodes added when using this graph.]

Description [AIG nodes for the fanins should be assigned to pNode->pFunc of the leaves of the graph before calling this procedure. Returns -1 if the number of nodes and levels exceeded the given limit or the number of levels exceeded the maximum allowed level.]

SideEffects []

SeeAlso []

Definition at line 403 of file ivySeq.c.

{
    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 = (Ivy_Obj_t *)pNode0->pFunc; 
        pAnd1 = (Ivy_Obj_t *)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;
}

void Ivy_GraphUpdateNetworkSeq ( Ivy_Man_t *  p, Ivy_Obj_t *  pRoot, Dec_Graph_t *  pGraph, int  nGain  )

static

Function*************************************************************

Synopsis [Replaces MFFC of the node by the new factored form.]

Description []

SideEffects []

SeeAlso []

Definition at line 526 of file ivySeq.c.

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

int Ivy_ManRewriteSeq	(	Ivy_Man_t *	p,
		int	fUseZeroCost,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Performs incremental rewriting of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file ivySeq.c.

{ 
    Rwt_Man_t * pManRwt;
    Ivy_Obj_t * pNode;
    int i, nNodes, nGain;
    abctime clk, clkStart = Abc_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 = (Dec_Graph_t *)Rwt_ManReadDecs(pManRwt);
            int fCompl           = Rwt_ManReadCompl(pManRwt);
            // complement the FF if needed
clk = Abc_Clock();
            if ( fCompl ) Dec_GraphComplement( pGraph );
            Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain );
            if ( fCompl ) Dec_GraphComplement( pGraph );
Rwt_ManAddTimeUpdate( pManRwt, Abc_Clock() - clk );
        }
    }
Rwt_ManAddTimeTotal( pManRwt, Abc_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;
}

static unsigned Ivy_NodeCutHash ( Ivy_Cut_t *  pCut )

inlinestatic

Function*************************************************************

Synopsis [Find the hash value of the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 782 of file ivySeq.c.

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

int Ivy_NodeRewriteSeq ( Ivy_Man_t *  pMan, Rwt_Man_t *  p, Ivy_Obj_t *  pNode, int  fUseZeroCost  )

static

DECLARATIONS ///.

CFile****************************************************************

FileName [ivySeq.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id:

ivySeq.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]

Function*************************************************************

Synopsis [Performs rewriting for one node.]

Description [This procedure considers all the cuts computed for the node and tries to rewrite each of them using the "forest" of different AIG structures precomputed and stored in the RWR manager. Determines the best rewriting and computes the gain in the number of AIG nodes in the final network. In the end, p->vFanins contains information about the best cut that can be used for rewriting, while p->pGraph gives the decomposition dag (represented using decomposition graph data structure). Returns gain in the number of nodes or -1 if node cannot be rewritten.]

SideEffects []

SeeAlso []

Definition at line 145 of file ivySeq.c.

{
    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;
    unsigned uTruthBest = 0; // Suppress "might be used uninitialized"
    unsigned uTruth;//, nNewClauses;
    char * pPerm;
    int nNodesSaved;
    int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
    int i, c, GainCur = -1, GainBest = -1;
    abctime clk, clk2;//, clk3;

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

    // go through the cuts
clk = Abc_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 = Abc_Clock();
        uTruth = 0xFFFF & Ivy_CutGetTruth( pMan, pNode, pCut->pArray, pCut->nSize );  // truth table
p->timeTruth += Abc_Clock() - clk2;
        pPerm = p->pPerms4[ (int)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[(int)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 = Abc_Clock();
        // mark the fanin boundary 
        Vec_PtrForEachEntry( Ivy_Obj_t *, 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( Ivy_Obj_t *, p->vFaninsCur, pFanin, i )
            Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
p->timeMffc += Abc_Clock() - clk2;

        // evaluate the cut
clk2 = Abc_Clock();
        pGraph = Rwt_CutEvaluateSeq( pMan, p, pNode, pCut, pPerm, p->vFaninsCur, nNodesSaved, &GainCur, uTruth );
p->timeEval += Abc_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( Ivy_Obj_t *, p->vFaninsCur, pFanin, i )
                Vec_PtrPush( p->vFanins, pFanin );
        }
    }
    Vec_PtrFree( vFanout );
p->timeRes += Abc_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 = Abc_Clock();
//nNewClauses = Ivy_CutTruthPrint( pMan, p->pCut, uTruth );
//timeInv += Abc_Clock() - clk;

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

    // copy the leaves
    Ivy_GraphPrepare( (Dec_Graph_t *)p->pGraph, (Ivy_Cut_t *)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((Dec_Graph_t *)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  )

static

Function*************************************************************

Synopsis [Evaluates the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file ivySeq.c.

{
    Vec_Ptr_t * vSubgraphs;
    Dec_Graph_t * pGraphBest = NULL; // Suppress "might be used uninitialized"
    Dec_Graph_t * 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( Rwt_Node_t *, 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( Ivy_Obj_t *, 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;
}