src/aig/ivy/ivySeq.c File Reference

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

Include dependency graph for ivySeq.c:

Go to the source code of this file.

Functions
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 int	Ivy_CutHashValue (int NodeId)
int	Ivy_ManRewriteSeq (Ivy_Man_t *p, int fUseZeroCost, int fVerbose)
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
	)			[inline, static]

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 839 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 929 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 1102 of file ivySeq.c.

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

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1020 of file ivySeq.c.

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

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

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

Synopsis [Derives new cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 715 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
	)			[inline, static]

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

Synopsis [Derives new cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 639 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
	)			[inline, static]

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

Synopsis [Derives new cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 795 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 866 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 595 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 553 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

)

[inline, static]

Definition at line 38 of file ivySeq.c.

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

static int Ivy_CutPrescreen	(	Ivy_Cut_t *	pCut,
		int	Id0,
		int	Id1
	)			[inline, static]

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 617 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 957 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 978 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

)

[inline, static]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 997 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 357 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[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 470 of file ivySeq.c.

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

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

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 519 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 60 of file ivySeq.c.

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

static unsigned Ivy_NodeCutHash

(

Ivy_Cut_t *

pCut

)

[inline, static]

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

Synopsis [Find the hash value of the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 775 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]

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

] DECLARATIONS ///

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 142 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, 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
	)			[static]

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

Synopsis [Evaluates the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 305 of file ivySeq.c.

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