giaUtil.c File Reference

#include "gia.h"
#include "base/main/mainInt.h"

Go to the source code of this file.

Macros
#define	NUMBER1   3716960521u
	DECLARATIONS ///. More...
#define	NUMBER2   2174103536u

Functions
unsigned	Gia_ManRandom (int fReset)
	FUNCTION DEFINITIONS ///. More...
word	Gia_ManRandomW (int fReset)
void	Gia_ManRandomInfo (Vec_Ptr_t *vInfo, int iInputStart, int iWordStart, int iWordStop)
char *	Gia_TimeStamp ()
char *	Gia_FileNameGenericAppend (char *pBase, char *pSuffix)
void	Gia_ManIncrementTravId (Gia_Man_t *p)
void	Gia_ManCleanMark01 (Gia_Man_t *p)
void	Gia_ManSetMark0 (Gia_Man_t *p)
void	Gia_ManCleanMark0 (Gia_Man_t *p)
void	Gia_ManCheckMark0 (Gia_Man_t *p)
void	Gia_ManSetMark1 (Gia_Man_t *p)
void	Gia_ManCleanMark1 (Gia_Man_t *p)
void	Gia_ManCheckMark1 (Gia_Man_t *p)
void	Gia_ManCleanValue (Gia_Man_t *p)
void	Gia_ManFillValue (Gia_Man_t *p)
void	Gia_ObjSetPhase (Gia_Man_t *p, Gia_Obj_t *pObj)
void	Gia_ManSetPhase (Gia_Man_t *p)
void	Gia_ManSetPhasePattern (Gia_Man_t *p, Vec_Int_t *vCiValues)
void	Gia_ManSetPhase1 (Gia_Man_t *p)
void	Gia_ManCleanPhase (Gia_Man_t *p)
int	Gia_ManCheckCoPhase (Gia_Man_t *p)
void	Gia_ManCleanLevels (Gia_Man_t *p, int Size)
void	Gia_ManCleanTruth (Gia_Man_t *p)
int	Gia_ManLevelNum (Gia_Man_t *p)
float	Gia_ManLevelAve (Gia_Man_t *p)
Vec_Int_t *	Gia_ManGetCiLevels (Gia_Man_t *p)
int	Gia_ManSetLevels (Gia_Man_t *p, Vec_Int_t *vCiLevels)
Vec_Int_t *	Gia_ManReverseLevel (Gia_Man_t *p)
Vec_Int_t *	Gia_ManRequiredLevel (Gia_Man_t *p)
Vec_Int_t *	Gia_ManComputeSlacks (Gia_Man_t *p)
void	Gia_ManCreateValueRefs (Gia_Man_t *p)
void	Gia_ManCreateRefs (Gia_Man_t *p)
int *	Gia_ManCreateMuxRefs (Gia_Man_t *p)
void	Gia_ManDfsForCrossCut_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
Vec_Int_t *	Gia_ManDfsForCrossCut (Gia_Man_t *p, int fReverse)
int	Gia_ManCrossCut (Gia_Man_t *p, int fReverse)
Vec_Int_t *	Gia_ManCollectPoIds (Gia_Man_t *p)
int	Gia_ObjIsMuxType (Gia_Obj_t *pNode)
int	Gia_ObjRecognizeExor (Gia_Obj_t *pObj, Gia_Obj_t **ppFan0, Gia_Obj_t **ppFan1)
Gia_Obj_t *	Gia_ObjRecognizeMux (Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
int	Gia_ObjRecognizeMuxLits (Gia_Man_t *p, Gia_Obj_t *pNode, int *iLitT, int *iLitE)
int	Gia_NodeDeref_rec (Gia_Man_t *p, Gia_Obj_t *pNode)
int	Gia_NodeRef_rec (Gia_Man_t *p, Gia_Obj_t *pNode)
int	Gia_ManPoMffcSize (Gia_Man_t *p)
int	Gia_NodeMffcSize (Gia_Man_t *p, Gia_Obj_t *pNode)
int	Gia_ManHasDangling (Gia_Man_t *p)
int	Gia_ManMarkDangling (Gia_Man_t *p)
Vec_Int_t *	Gia_ManGetDangling (Gia_Man_t *p)
void	Gia_ObjPrint (Gia_Man_t *p, Gia_Obj_t *pObj)
void	Gia_ManPrint (Gia_Man_t *p)
void	Gia_ManPrintCo_rec (Gia_Man_t *p, Gia_Obj_t *pObj)
void	Gia_ManPrintCo (Gia_Man_t *p, Gia_Obj_t *pObj)
void	Gia_ManPrintCollect_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
void	Gia_ManPrintCone (Gia_Man_t *p, Gia_Obj_t *pObj, int *pLeaves, int nLeaves, Vec_Int_t *vNodes)
void	Gia_ManPrintCollect2_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes)
void	Gia_ManPrintCone2 (Gia_Man_t *p, Gia_Obj_t *pObj)
void	Gia_ManInvertConstraints (Gia_Man_t *pAig)
void	Gia_ManInvertPos (Gia_Man_t *pAig)
void	Gia_ManCollectObjs_rec (Gia_Man_t *p, int iObjId, Vec_Int_t *vObjs, int Limit)
unsigned *	Gia_ManComputePoTruthTables (Gia_Man_t *p, int nBytesMax)
int	Gia_ManCompare (Gia_Man_t *p1, Gia_Man_t *p2)
void	Gia_ManMarkFanoutDrivers (Gia_Man_t *p)
void	Gia_ManSwapPos (Gia_Man_t *p, int i)
Vec_Int_t *	Gia_ManSaveValue (Gia_Man_t *p)
void	Gia_ManLoadValue (Gia_Man_t *p, Vec_Int_t *vValues)
Vec_Int_t *	Gia_ManFirstFanouts (Gia_Man_t *p)
int	Gia_ManHasChoices_very_old (Gia_Man_t *p)
Vec_Int_t *	Gia_ManGroupProve (Gia_Man_t *pInit, char *pCommLine, int nGroupSize, int fVerbose)
Vec_Int_t *	Gia_ManPoXSim (Gia_Man_t *p, int nFrames, int fVerbose)

Macro Definition Documentation

#define NUMBER1   3716960521u

DECLARATIONS ///.

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

FileName [giaUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Various utilities.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

giaUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 31 of file giaUtil.c.

#define NUMBER2   2174103536u

Definition at line 32 of file giaUtil.c.

Function Documentation

char* Gia_FileNameGenericAppend	(	char *	pBase,
		char *	pSuffix
	)

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

Synopsis [Returns the composite name of the file.]

Description []

SideEffects []

SeeAlso []

Definition at line 125 of file giaUtil.c.

{
    static char Buffer[1000];
    char * pDot;
    strcpy( Buffer, pBase );
    if ( (pDot = strrchr( Buffer, '.' )) )
        *pDot = 0;
    strcat( Buffer, pSuffix );
    if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) )
        return pDot+1;
    return Buffer;
}

int Gia_ManCheckCoPhase

(

Gia_Man_t *

p

)

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

Synopsis [Returns the number of COs whose value is 1.]

Description []

SideEffects []

SeeAlso []

Definition at line 450 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i, Counter = 0;
    Gia_ManForEachCo( p, pObj, i )
        Counter += pObj->fPhase;
    return Counter;
}

void Gia_ManCheckMark0

(

Gia_Man_t *

p

)

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

Synopsis [Sets phases of the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 234 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
        assert( pObj->fMark0 == 0 );
}

void Gia_ManCheckMark1

(

Gia_Man_t *

p

)

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

Synopsis [Sets phases of the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
        assert( pObj->fMark1 == 0 );
}

void Gia_ManCleanLevels	(	Gia_Man_t *	p,
		int	Size
	)

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

Synopsis [Prepares copies for the model.]

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file giaUtil.c.

{
    if ( p->vLevels == NULL )
        p->vLevels = Vec_IntAlloc( Size );
    Vec_IntFill( p->vLevels, Size, 0 );
}

void Gia_ManCleanMark0

(

Gia_Man_t *

p

)

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

Synopsis [Sets phases of the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 215 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
        pObj->fMark0 = 0;
}

void Gia_ManCleanMark01

(

Gia_Man_t *

p

)

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

Synopsis [Sets phases of the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
        pObj->fMark0 = pObj->fMark1 = 0;
}

void Gia_ManCleanMark1

(

Gia_Man_t *

p

)

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

Synopsis [Sets phases of the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
        pObj->fMark1 = 0;
}

void Gia_ManCleanPhase

(

Gia_Man_t *

p

)

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

Synopsis [Sets phases of the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 431 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
        pObj->fPhase = 0;
}

void Gia_ManCleanTruth

(

Gia_Man_t *

p

)

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

Synopsis [Prepares copies for the model.]

Description []

SideEffects []

SeeAlso []

Definition at line 487 of file giaUtil.c.

{
    if ( p->vTruths == NULL )
        p->vTruths = Vec_IntAlloc( Gia_ManObjNum(p) );
    Vec_IntFill( p->vTruths, Gia_ManObjNum(p), -1 );
}

void Gia_ManCleanValue

(

Gia_Man_t *

p

)

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

Synopsis [Cleans the value.]

Description []

SideEffects []

SeeAlso []

Definition at line 310 of file giaUtil.c.

{
    int i;
    for ( i = 0; i < p->nObjs; i++ )
        p->pObjs[i].Value = 0;
}

void Gia_ManCollectObjs_rec	(	Gia_Man_t *	p,
		int	iObjId,
		Vec_Int_t *	vObjs,
		int	Limit
	)

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

Synopsis [Testing the speedup due to grouping POs into batches.]

Description []

SideEffects []

SeeAlso []

Definition at line 1444 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    if ( Vec_IntSize(vObjs) == Limit )
        return;
    if ( Gia_ObjIsTravIdCurrentId(p, iObjId) )
        return;
    Gia_ObjSetTravIdCurrentId(p, iObjId);
    pObj = Gia_ManObj( p, iObjId );
    if ( Gia_ObjIsAnd(pObj) )
    {
        Gia_ManCollectObjs_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, Limit );
        if ( Vec_IntSize(vObjs) == Limit )
            return;
        Gia_ManCollectObjs_rec( p, Gia_ObjFaninId1p(p, pObj), vObjs, Limit );
        if ( Vec_IntSize(vObjs) == Limit )
            return;
    }
    Vec_IntPush( vObjs, iObjId );
}

Vec_Int_t* Gia_ManCollectPoIds

(

Gia_Man_t *

p

)

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

Synopsis [Collects PO Ids into one array.]

Description []

SideEffects []

SeeAlso []

Definition at line 863 of file giaUtil.c.

{
    Vec_Int_t * vStart;
    int Entry, i;
    vStart = Vec_IntAlloc( Gia_ManPoNum(p) );
    Vec_IntForEachEntryStop( p->vCos, Entry, i, Gia_ManPoNum(p) )
        Vec_IntPush( vStart, Entry );
    return vStart;
}

int Gia_ManCompare	(	Gia_Man_t *	p1,
		Gia_Man_t *	p2
	)

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

Synopsis [Returns 1 if the manager are structural identical.]

Description []

SideEffects []

SeeAlso []

Definition at line 1511 of file giaUtil.c.

{
    Gia_Obj_t * pObj1, * pObj2;
    int i;
    if ( Gia_ManObjNum(p1) != Gia_ManObjNum(p2) )
    {
        printf( "AIGs have different number of objects.\n" );
        return 0;
    }
    Gia_ManCleanValue( p1 );
    Gia_ManCleanValue( p2 );
    Gia_ManForEachObj( p1, pObj1, i )
    {
        pObj2 = Gia_ManObj( p2, i );
        if ( memcmp( pObj1, pObj2, sizeof(Gia_Obj_t) ) )
        {
            printf( "Objects %d are different.\n", i );
            return 0;
        }
        if ( p1->pReprs && p2->pReprs )
        {
            if ( memcmp( &p1->pReprs[i], &p2->pReprs[i], sizeof(Gia_Rpr_t) ) )
            {
                printf( "Representatives of objects %d are different.\n", i );
                return 0;
            }
        }
    }
    return 1;
}

unsigned* Gia_ManComputePoTruthTables	(	Gia_Man_t *	p,
		int	nBytesMax
	)

Definition at line 1464 of file giaUtil.c.

{
    int nVars = Gia_ManPiNum(p);
    int nTruthWords = Abc_TruthWordNum( nVars );
    int nTruths = nBytesMax / (sizeof(unsigned) * nTruthWords);
    int nTotalNodes = 0, nRounds = 0;
    Vec_Int_t * vObjs;
    Gia_Obj_t * pObj;
    abctime clk = Abc_Clock();
    int i;
    printf( "Var = %d. Words = %d. Truths = %d.\n", nVars, nTruthWords, nTruths );
    vObjs = Vec_IntAlloc( nTruths );
    Gia_ManIncrementTravId( p );
    Gia_ManForEachPo( p, pObj, i )
    {
        Gia_ManCollectObjs_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, nTruths );
        if ( Vec_IntSize(vObjs) == nTruths )
        {
            nRounds++;
//            printf( "%d ", i );
            nTotalNodes += Vec_IntSize( vObjs );
            Vec_IntClear( vObjs );
            Gia_ManIncrementTravId( p );
        }
    }
//    printf( "\n" );
    nTotalNodes += Vec_IntSize( vObjs );
    Vec_IntFree( vObjs );

    printf( "Rounds = %d. Objects = %d. Total = %d.   ", nRounds, Gia_ManObjNum(p), nTotalNodes );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

    return NULL;
}

Vec_Int_t* Gia_ManComputeSlacks

(

Gia_Man_t *

p

)

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

Synopsis [Compute slacks measured using the number of AIG levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 663 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i, nLevels = Gia_ManLevelNum( p );
    Vec_Int_t * vLevelR = Gia_ManReverseLevel( p );
    Vec_Int_t * vSlacks = Vec_IntAlloc( Gia_ManObjNum(p) );
    Gia_ManForEachObj( p, pObj, i )
        Vec_IntPush( vSlacks, nLevels - Gia_ObjLevelId(p, i) - Vec_IntEntry(vLevelR, i) );
    assert( Vec_IntSize(vSlacks) == Gia_ManObjNum(p) );
    Vec_IntFree( vLevelR );
    return vSlacks;
}

int* Gia_ManCreateMuxRefs

(

Gia_Man_t *

p

)

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

Synopsis [Assigns references.]

Description []

SideEffects []

SeeAlso []

Definition at line 746 of file giaUtil.c.

{
    Gia_Obj_t * pObj, * pCtrl, * pFan0, * pFan1;
    int i, * pMuxRefs;
    pMuxRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) )
            continue;
        if ( !Gia_ObjIsMuxType(pObj) )
            continue;
        pCtrl = Gia_ObjRecognizeMux( pObj, &pFan0, &pFan1 );
        pMuxRefs[ Gia_ObjId(p, Gia_Regular(pCtrl)) ]++;
    }
    return pMuxRefs;
}

void Gia_ManCreateRefs

(

Gia_Man_t *

p

)

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

Synopsis [Assigns references.]

Description []

SideEffects []

SeeAlso []

Definition at line 715 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    assert( p->pRefs == NULL );
    p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
        {
            Gia_ObjRefFanin0Inc( p, pObj );
            Gia_ObjRefFanin1Inc( p, pObj );
            if ( Gia_ObjIsMuxId(p, i) )
                Gia_ObjRefFanin2Inc( p, pObj );
        }
        else if ( Gia_ObjIsCo(pObj) )
            Gia_ObjRefFanin0Inc( p, pObj );
    }
}

void Gia_ManCreateValueRefs

(

Gia_Man_t *

p

)

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

Synopsis [Assigns levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 687 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
    {
        pObj->Value = 0;
        if ( Gia_ObjIsAnd(pObj) )
        {
            Gia_ObjFanin0(pObj)->Value++;
            Gia_ObjFanin1(pObj)->Value++;
        }
        else if ( Gia_ObjIsCo(pObj) )
            Gia_ObjFanin0(pObj)->Value++;
    }
}

int Gia_ManCrossCut	(	Gia_Man_t *	p,
		int	fReverse
	)

Definition at line 820 of file giaUtil.c.

{
    Vec_Int_t * vNodes;
    Gia_Obj_t * pObj;
    int i, nCutCur = 0, nCutMax = 0;
    vNodes = Gia_ManDfsForCrossCut( p, fReverse );
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
    {
        if ( pObj->Value )
            nCutCur++;
        if ( nCutMax < nCutCur )
            nCutMax = nCutCur;
        if ( Gia_ObjIsAnd(pObj) )
        {
            if ( --Gia_ObjFanin0(pObj)->Value == 0 )
                nCutCur--;
            if ( --Gia_ObjFanin1(pObj)->Value == 0 )
                nCutCur--;
        }
        else if ( Gia_ObjIsCo(pObj) )
        {
            if ( --Gia_ObjFanin0(pObj)->Value == 0 )
                nCutCur--;
        }
    }
    Vec_IntFree( vNodes );
    Gia_ManForEachObj( p, pObj, i )
        assert( pObj->Value == 0 );
    return nCutMax;
}

Vec_Int_t* Gia_ManDfsForCrossCut	(	Gia_Man_t *	p,
		int	fReverse
	)

Definition at line 798 of file giaUtil.c.

{
    Vec_Int_t * vNodes;
    Gia_Obj_t * pObj;
    int i;
    Gia_ManCleanValue( p );
    vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
    Gia_ManIncrementTravId( p );
    if ( fReverse )
    {
        Gia_ManForEachCoReverse( p, pObj, i )
            if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
                Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
    }
    else
    {
        Gia_ManForEachCo( p, pObj, i )
            if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
                Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
    }
    return vNodes;
}

void Gia_ManDfsForCrossCut_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vNodes
	)

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

Synopsis [Computes the maximum frontier size.]

Description []

SideEffects []

SeeAlso []

Definition at line 774 of file giaUtil.c.

{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return;
    Gia_ObjSetTravIdCurrent(p, pObj);
    if ( Gia_ObjIsCi(pObj) )
    {
        Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
        return;
    }
    if ( Gia_ObjIsCo(pObj) )
    {
        Gia_ObjFanin0(pObj)->Value++;
        Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin0(pObj), vNodes );
        Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
        return;
    }
    assert( Gia_ObjIsAnd(pObj) );
    Gia_ObjFanin0(pObj)->Value++;
    Gia_ObjFanin1(pObj)->Value++;
    Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin0(pObj), vNodes );
    Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin1(pObj), vNodes );
    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
}

void Gia_ManFillValue

(

Gia_Man_t *

p

)

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

Synopsis [Cleans the value.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file giaUtil.c.

{
    int i;
    for ( i = 0; i < p->nObjs; i++ )
        p->pObjs[i].Value = ~0;
}

Vec_Int_t* Gia_ManFirstFanouts

(

Gia_Man_t *

p

)

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

Synopsis [Returns the array containing the first fanout of each object.]

Description []

SideEffects []

SeeAlso []

Definition at line 1635 of file giaUtil.c.

{
    Vec_Int_t * vFans = Vec_IntStart( Gia_ManObjNum(p) );
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
        {
            if ( Vec_IntEntry(vFans, Gia_ObjFaninId0p(p, pObj)) == 0 )
                Vec_IntWriteEntry(vFans, Gia_ObjFaninId0p(p, pObj), i);
            if ( Vec_IntEntry(vFans, Gia_ObjFaninId1p(p, pObj)) == 0 )
                Vec_IntWriteEntry(vFans, Gia_ObjFaninId1p(p, pObj), i);
            if ( Gia_ObjIsMuxId(p, i) && Vec_IntEntry(vFans, Gia_ObjFaninId2p(p, pObj)) == 0 )
                Vec_IntWriteEntry(vFans, Gia_ObjFaninId2p(p, pObj), i);
        }
        else if ( Gia_ObjIsCo(pObj) )
        {
            if ( Vec_IntEntry(vFans, Gia_ObjFaninId0p(p, pObj)) == 0 )
                Vec_IntWriteEntry(vFans, Gia_ObjFaninId0p(p, pObj), i);
        }
    }
    return vFans;
}

Vec_Int_t* Gia_ManGetCiLevels

(

Gia_Man_t *

p

)

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

Synopsis [Assigns levels using CI level information.]

Description []

SideEffects []

SeeAlso []

Definition at line 546 of file giaUtil.c.

{
    Vec_Int_t * vCiLevels;
    Gia_Obj_t * pObj;
    int i;
    if ( p->vLevels == NULL )
        return NULL;
    vCiLevels = Vec_IntAlloc( Gia_ManCiNum(p) );
    Gia_ManForEachCi( p, pObj, i )
        Vec_IntPush( vCiLevels, Gia_ObjLevel(p, pObj) );
    return vCiLevels;
}

Vec_Int_t* Gia_ManGetDangling

(

Gia_Man_t *

p

)

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

Synopsis [Returns 1 if AIG has dangling nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1224 of file giaUtil.c.

{
    Vec_Int_t * vDangles;
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
    {
        pObj->fMark0 = 0;
        if ( Gia_ObjIsAnd(pObj) )
        {
            Gia_ObjFanin0(pObj)->fMark0 = 1;
            Gia_ObjFanin1(pObj)->fMark0 = 1;
        }
        else if ( Gia_ObjIsCo(pObj) )
            Gia_ObjFanin0(pObj)->fMark0 = 1;
    }
    vDangles = Vec_IntAlloc( 100 );
    Gia_ManForEachAnd( p, pObj, i )
        if ( !pObj->fMark0 )
            Vec_IntPush( vDangles, i );
    Gia_ManCleanMark0( p );
    return vDangles;
}

Vec_Int_t* Gia_ManGroupProve	(	Gia_Man_t *	pInit,
		char *	pCommLine,
		int	nGroupSize,
		int	fVerbose
	)

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

Synopsis [Proving multi-output properties.]

Description []

SideEffects []

SeeAlso []

Definition at line 1763 of file giaUtil.c.

{
    Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame();
    Gia_Man_t * p = Gia_ManDup( pInit );
    Gia_Man_t * pGroup;
    Vec_Int_t * vOuts;
    Vec_Int_t * vOutMap;
    Vec_Ptr_t * vCexes;
    int i, k, nGroupCur, nGroups;
    abctime clk, timeComm = 0;
    abctime timeStart = Abc_Clock();
    // pre-conditions
    assert( nGroupSize > 0 );
    assert( pCommLine != NULL );
    assert( p->nConstrs == 0 );
    Abc_Print( 1, "RUNNING MultiProve: Group size = %d. Command line = \"%s\".\n", nGroupSize, pCommLine );
    // create output map
    vOuts   = Vec_IntStartNatural( Gia_ManPoNum(p) );
    vOutMap = Vec_IntAlloc( Gia_ManPoNum(p) );
    vCexes  = Vec_PtrAlloc( Gia_ManPoNum(p) );
    nGroups = Gia_ManPoNum(p) / nGroupSize + (int)((Gia_ManPoNum(p) % nGroupSize) > 0);
    for ( i = 0; i < nGroups; i++ )
    {
        // derive the group
        nGroupCur = ((i + 1) * nGroupSize < Gia_ManPoNum(p)) ? nGroupSize : Gia_ManPoNum(p) - i * nGroupSize;
        pGroup = Gia_ManDupCones( p, Vec_IntArray(vOuts) + i * nGroupSize, nGroupCur, 0 );
        Abc_Print( 1, "GROUP %4d : %4d <= PoId < %4d : ", i, i * nGroupSize, i * nGroupSize + nGroupCur );
        // set the current GIA
        Abc_FrameUpdateGia( pAbc, pGroup );
        // solve the group
        clk = Abc_Clock();
        Cmd_CommandExecute( pAbc, pCommLine );
        timeComm += Abc_Clock() - clk;
        // get the solution status
        if ( nGroupSize == 1 )
        {
            Vec_IntPush( vOutMap, Abc_FrameReadProbStatus(pAbc) );
            Vec_PtrPush( vCexes, Abc_FrameReadCex(pAbc) );
        }
        else // if ( nGroupSize > 1 )  
        {
            Vec_Int_t * vStatusCur = Abc_FrameReadPoStatuses( pAbc );
            Vec_Ptr_t * vCexesCur = Abc_FrameReadCexVec( pAbc );
            assert( vStatusCur != NULL ); // only works for "bmc3" and "pdr"
//            assert( vCexesCur != NULL );
            for ( k = 0; k < nGroupCur; k++ )
            {
                Vec_IntPush( vOutMap, Vec_IntEntry(vStatusCur, k) );
                Vec_PtrPush( vCexes, vCexesCur ? Vec_PtrEntry(vCexesCur, k) : NULL );
            }
        }
    }
    assert( Vec_PtrSize(vCexes) == Gia_ManPoNum(p) );
    assert( Vec_IntSize(vOutMap) == Gia_ManPoNum(p) );
    // set CEXes
    if ( Vec_PtrCountZero(vCexes) < Vec_PtrSize(vCexes) )
        Abc_FrameReplaceCexVec( pAbc, &vCexes );
    else  // there is no CEXes
        Vec_PtrFree( vCexes );
    // report the result
    Abc_Print( 1, "SUMMARY:  " );
    Abc_Print( 1, "Properties = %6d. ", Gia_ManPoNum(p) );
    Abc_Print( 1, "UNSAT = %6d. ",      Vec_IntCountEntry(vOutMap, 1) );
    Abc_Print( 1, "SAT = %6d. ",        Vec_IntCountEntry(vOutMap, 0) );
    Abc_Print( 1, "UNDEC = %6d. ",      Vec_IntCountEntry(vOutMap, -1) );
    Abc_Print( 1, "\n" );
    Abc_PrintTime( 1, "Command time", timeComm );
    Abc_PrintTime( 1, "Total time  ", Abc_Clock() - timeStart );
    // cleanup
    Vec_IntFree( vOuts );
    Gia_ManStop( p );
    return vOutMap;
}

int Gia_ManHasChoices_very_old

(

Gia_Man_t *

p

)

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

Synopsis [Returns 1 if AIG has choices.]

Description []

SideEffects []

SeeAlso []

Definition at line 1671 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i, Counter1 = 0, Counter2 = 0;
    int nFailNoRepr = 0;
    int nFailHaveRepr = 0;
    int nChoiceNodes = 0;
    int nChoices = 0;
    if ( p->pReprs == NULL || p->pNexts == NULL )
        return 0;
    // check if there are any representatives
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
        {
//            printf( "%d ", i );
            Counter1++;
        }
//        if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
//            Counter2++;
    }
//    printf( "\n" );
    Gia_ManForEachObj( p, pObj, i )
    {
//        if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
//            Counter1++;
        if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
        {
//            printf( "%d ", i );
            Counter2++;
        }
    }
//    printf( "\n" );
    if ( Counter1 == 0 )
    {
        printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
        return 0;
    }
    printf( "%d nodes have reprs.\n", Counter1 );
    printf( "%d nodes have nexts.\n", Counter2 );
    // check if there are any internal nodes without fanout
    // make sure all nodes without fanout have representatives
    // make sure all nodes with fanout have no representatives
    ABC_FREE( p->pRefs );
    Gia_ManCreateRefs( p );
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( Gia_ObjRefNum(p, pObj) == 0 )
        {
            if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
                nFailNoRepr++;
            else
                nChoices++;
        }
        else
        {
            if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
                nFailHaveRepr++;
            if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
                nChoiceNodes++;
        }
        if ( Gia_ObjReprObj( p, i ) )
            assert( Gia_ObjRepr(p, i) < i );
    }
    if ( nChoices == 0 )
        return 0;
    if ( nFailNoRepr )
    {
        printf( "Gia_ManHasChoices_very_old(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
//        return 0;
    }
    if ( nFailHaveRepr )
    {
        printf( "Gia_ManHasChoices_very_old(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
//        return 0;
    }
//    printf( "Gia_ManHasChoices_very_old(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
    return 1;
}

int Gia_ManHasDangling

(

Gia_Man_t *

p

)

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

Synopsis [Returns 1 if AIG has dangling nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1155 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i, Counter = 0;
    Gia_ManForEachObj( p, pObj, i )
    {
        pObj->fMark0 = 0;
        if ( Gia_ObjIsCo(pObj) )
            Gia_ObjFanin0(pObj)->fMark0 = 1;
        else if ( Gia_ObjIsMux(p, pObj) )
        {
            Gia_ObjFanin0(pObj)->fMark0 = 1;
            Gia_ObjFanin1(pObj)->fMark0 = 1;
            Gia_ObjFanin2(p, pObj)->fMark0 = 1;
        }
        else if ( Gia_ObjIsAnd(pObj) )
        {
            Gia_ObjFanin0(pObj)->fMark0 = 1;
            Gia_ObjFanin1(pObj)->fMark0 = 1;
        }
    }
    Gia_ManForEachAnd( p, pObj, i )
        Counter += !pObj->fMark0;
    Gia_ManCleanMark0( p );
    return Counter;
}

void Gia_ManIncrementTravId

(

Gia_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file giaUtil.c.

{ 
    if ( p->pTravIds == NULL )
    {
        p->nTravIdsAlloc = Gia_ManObjNum(p) + 100; 
        p->pTravIds = ABC_CALLOC( int, p->nTravIdsAlloc ); 
        p->nTravIds = 0;  
    }
    while ( p->nTravIdsAlloc < Gia_ManObjNum(p) )
    {
        p->nTravIdsAlloc *= 2;
        p->pTravIds = ABC_REALLOC( int, p->pTravIds, p->nTravIdsAlloc );
        memset( p->pTravIds + p->nTravIdsAlloc/2, 0, sizeof(int) * p->nTravIdsAlloc/2 );
    }
    p->nTravIds++;                                                    
}

void Gia_ManInvertConstraints

(

Gia_Man_t *

pAig

)

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

Synopsis [Complements the constraint outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1415 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    if ( Gia_ManConstrNum(pAig) == 0 )
        return;
    Gia_ManForEachPo( pAig, pObj, i )
        if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) )
            Gia_ObjFlipFaninC0( pObj );
}

void Gia_ManInvertPos

(

Gia_Man_t *

pAig

)

Definition at line 1425 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachPo( pAig, pObj, i )
        Gia_ObjFlipFaninC0( pObj );
}

float Gia_ManLevelAve

(

Gia_Man_t *

p

)

Definition at line 525 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i, Ave = 0;
    assert( p->vLevels );
    Gia_ManForEachCo( p, pObj, i )
        Ave += Gia_ObjLevel(p, pObj);
    return (float)Ave / Gia_ManCoNum(p);
}

int Gia_ManLevelNum

(

Gia_Man_t *

p

)

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

Synopsis [Assigns levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 505 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
    p->nLevels = 0;
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjIsBuf(pObj) )
            Gia_ObjSetBufLevel( p, pObj );
        else if ( Gia_ObjIsAnd(pObj) )
            Gia_ObjSetGateLevel( p, pObj );
        else if ( Gia_ObjIsCo(pObj) )
            Gia_ObjSetCoLevel( p, pObj );
        else
            Gia_ObjSetLevel( p, pObj, 0 );
        p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
    }
    return p->nLevels;
}

void Gia_ManLoadValue	(	Gia_Man_t *	p,
		Vec_Int_t *	vValues
	)

Definition at line 1615 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
        pObj->Value = Vec_IntEntry(vValues, i);
}

int Gia_ManMarkDangling

(

Gia_Man_t *

p

)

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

Synopsis [Returns 1 if AIG has dangling nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1193 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i, Counter = 0;
    Gia_ManForEachObj( p, pObj, i )
    {
        pObj->fMark0 = 0;
        if ( Gia_ObjIsAnd(pObj) )
        {
            Gia_ObjFanin0(pObj)->fMark0 = 1;
            Gia_ObjFanin1(pObj)->fMark0 = 1;
        }
        else if ( Gia_ObjIsCo(pObj) )
            Gia_ObjFanin0(pObj)->fMark0 = 1;
    }
    Gia_ManForEachAnd( p, pObj, i )
        Counter += !pObj->fMark0;
    return Counter;
}

void Gia_ManMarkFanoutDrivers

(

Gia_Man_t *

p

)

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

Synopsis [Marks nodes that appear as faninis of other nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1553 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
    {
        pObj->fMark0 = 0;
        if ( Gia_ObjIsAnd(pObj) )
        {
            Gia_ObjFanin0(pObj)->fMark0 = 1;
            Gia_ObjFanin1(pObj)->fMark0 = 1;
        }
        else if ( Gia_ObjIsCo(pObj) )
            Gia_ObjFanin0(pObj)->fMark0 = 1;
    }
}

int Gia_ManPoMffcSize

(

Gia_Man_t *

p

)

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

Synopsis [References the node's MFFC.]

Description []

SideEffects []

SeeAlso []

Definition at line 1115 of file giaUtil.c.

{
    Gia_ManCreateRefs( p );
    return Gia_NodeDeref_rec( p, Gia_ObjFanin0(Gia_ManPo(p, 0)) );
}

Vec_Int_t* Gia_ManPoXSim	(	Gia_Man_t *	p,
		int	nFrames,
		int	fVerbose
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1849 of file giaUtil.c.

{
    Vec_Int_t * vRes;
    Gia_Obj_t * pObj;
    int f, k, nLeft = Gia_ManPoNum(p);
    vRes = Vec_IntAlloc( Gia_ManPoNum(p) );
    Vec_IntFill( vRes, Gia_ManPoNum(p), nFrames );
    Gia_ObjTerSimSet0( Gia_ManConst0(p) );
    Gia_ManForEachRi( p, pObj, k )
        Gia_ObjTerSimSet0( pObj );
    for ( f = 0; f < nFrames; f++ )
    {
        Gia_ManForEachPi( p, pObj, k )
            Gia_ObjTerSimSetX( pObj );
        Gia_ManForEachRo( p, pObj, k )
            Gia_ObjTerSimRo( p, pObj );
        Gia_ManForEachAnd( p, pObj, k )
            Gia_ObjTerSimAnd( pObj );
        Gia_ManForEachCo( p, pObj, k )
            Gia_ObjTerSimCo( pObj );
        if ( fVerbose )
        {
            Gia_ManForEachPo( p, pObj, k )
                Gia_ObjTerSimPrint( pObj );
            printf( "\n" );
        }
        Gia_ManForEachPo( p, pObj, k )
            if ( Vec_IntEntry(vRes, k) == nFrames && Gia_ObjTerSimGetX(pObj) )
                Vec_IntWriteEntry(vRes, k, f), nLeft--;
        if ( nLeft == 0 )
            break;
    }
    if ( fVerbose )
    {
        if ( nLeft == 0 )
            printf( "Simulation converged after %d frames.\n", f+1 );
        else
            printf( "Simulation terminated after %d frames.\n", nFrames );
    }        
//    Vec_IntPrint( vRes );
    return vRes;
}

void Gia_ManPrint

(

Gia_Man_t *

p

)

Definition at line 1329 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    printf( "GIA manager has %d ANDs, %d XORs, %d MUXes.\n", 
        Gia_ManAndNum(p) - Gia_ManXorNum(p) - Gia_ManMuxNum(p), Gia_ManXorNum(p), Gia_ManMuxNum(p) ); 
    Gia_ManForEachObj( p, pObj, i )
        Gia_ObjPrint( p, pObj );
}

void Gia_ManPrintCo	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

Definition at line 1349 of file giaUtil.c.

{
    assert( Gia_ObjIsCo(pObj) );
    printf( "TFI cone of CO number %d:\n", Gia_ObjCioId(pObj) );
    Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
    Gia_ObjPrint( p, pObj );
}

void Gia_ManPrintCo_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

Definition at line 1338 of file giaUtil.c.

{
    if ( Gia_ObjIsAnd(pObj) )
    {
        Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
        Gia_ManPrintCo_rec( p, Gia_ObjFanin1(pObj) );
        if ( Gia_ObjIsMux(p, pObj) )
            Gia_ManPrintCo_rec( p, Gia_ObjFanin2(p, pObj) );
    }
    Gia_ObjPrint( p, pObj );
}

void Gia_ManPrintCollect2_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vNodes
	)

Definition at line 1380 of file giaUtil.c.

{
    if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 )
        return;
    if ( Gia_ObjIsCo(pObj) || Gia_ObjIsAnd(pObj) )
        Gia_ManPrintCollect2_rec( p, Gia_ObjFanin0(pObj), vNodes );
    if ( Gia_ObjIsAnd(pObj) )
        Gia_ManPrintCollect2_rec( p, Gia_ObjFanin1(pObj), vNodes );
    if ( Gia_ObjIsMux(p, pObj) )
        Gia_ManPrintCollect2_rec( p, Gia_ObjFanin2(p, pObj), vNodes );
    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
}

void Gia_ManPrintCollect_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vNodes
	)

Definition at line 1357 of file giaUtil.c.

{
    if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 )
        return;
    assert( Gia_ObjIsAnd(pObj) );
    Gia_ManPrintCollect_rec( p, Gia_ObjFanin0(pObj), vNodes );
    Gia_ManPrintCollect_rec( p, Gia_ObjFanin1(pObj), vNodes );
    if ( Gia_ObjIsMux(p, pObj) )
        Gia_ManPrintCollect_rec( p, Gia_ObjFanin2(p, pObj), vNodes );
    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
}

void Gia_ManPrintCone	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		int *	pLeaves,
		int	nLeaves,
		Vec_Int_t *	vNodes
	)

Definition at line 1368 of file giaUtil.c.

{
    int i;
    Vec_IntClear( vNodes );
    for ( i = 0; i < nLeaves; i++ )
        Vec_IntPush( vNodes, pLeaves[i] );
    Gia_ManPrintCollect_rec( p, pObj, vNodes );
    printf( "GIA logic cone for node %d:\n", Gia_ObjId(p, pObj) );
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        Gia_ObjPrint( p, pObj );
}

void Gia_ManPrintCone2	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

Definition at line 1392 of file giaUtil.c.

{
    Vec_Int_t * vNodes;
    int i;
    vNodes = Vec_IntAlloc( 100 );
    Gia_ManPrintCollect2_rec( p, pObj, vNodes );
    printf( "GIA logic cone for node %d:\n", Gia_ObjId(p, pObj) );
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        Gia_ObjPrint( p, pObj );
    Vec_IntFree( vNodes );
}

unsigned Gia_ManRandom

(

int

fReset

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Creates a sequence or random numbers.]

Description []

SideEffects []

SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]

Definition at line 49 of file giaUtil.c.

{
    static unsigned int m_z = NUMBER1;
    static unsigned int m_w = NUMBER2;
    if ( fReset )
    {
        m_z = NUMBER1;
        m_w = NUMBER2;
    }
    m_z = 36969 * (m_z & 65535) + (m_z >> 16);
    m_w = 18000 * (m_w & 65535) + (m_w >> 16);
    return (m_z << 16) + m_w;
}

void Gia_ManRandomInfo	(	Vec_Ptr_t *	vInfo,
		int	iInputStart,
		int	iWordStart,
		int	iWordStop
	)

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

Synopsis [Creates random info for the primary inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file giaUtil.c.

{
    unsigned * pInfo;
    int i, w;
    Vec_PtrForEachEntryStart( unsigned *, vInfo, pInfo, i, iInputStart )
        for ( w = iWordStart; w < iWordStop; w++ )
            pInfo[w] = Gia_ManRandom(0);
}

word Gia_ManRandomW

(

int

fReset

)

Definition at line 62 of file giaUtil.c.

{ 
    return ((word)Gia_ManRandom(fReset) << 32) | ((word)Gia_ManRandom(fReset) << 0);
}

Vec_Int_t* Gia_ManRequiredLevel

(

Gia_Man_t *

p

)

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

Synopsis [Compute required levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 639 of file giaUtil.c.

{
    Vec_Int_t * vRequired;
    Gia_Obj_t * pObj;
    int i, LevelMax = 0;
    vRequired = Gia_ManReverseLevel( p );
    Gia_ManForEachCi( p, pObj, i )
        LevelMax = Abc_MaxInt( LevelMax, Vec_IntEntry(vRequired, Gia_ObjId(p, pObj)) );
    Gia_ManForEachObj( p, pObj, i )
        Vec_IntWriteEntry( vRequired, i, LevelMax - Vec_IntEntry(vRequired, i) );
    return vRequired;
}

Vec_Int_t* Gia_ManReverseLevel

(

Gia_Man_t *

p

)

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

Synopsis [Compute reverse levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 595 of file giaUtil.c.

{
    Vec_Int_t * vLevelRev;
    Gia_Obj_t * pObj;
    int i;
    vLevelRev = Vec_IntStart( Gia_ManObjNum(p) );
    Gia_ManForEachAndReverse( p, pObj, i )
    {
        int LevelR = Vec_IntEntry( vLevelRev, i );
        if ( Gia_ObjIsMux(p, pObj) )
        {
            Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR + 2 );
            Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId1(pObj, i), LevelR + 2 );
            Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId2(p, i), LevelR + 2 );
        }
        else if ( Gia_ObjIsXor(pObj) )
        {
            Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR + 2 );
            Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId1(pObj, i), LevelR + 2 );
        }
        else if ( Gia_ObjIsBuf(pObj) )
        {
            Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR );
        }
        else
        {
            Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR + 1 );
            Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId1(pObj, i), LevelR + 1 );
        }
    }
    return vLevelRev;
}

Vec_Int_t* Gia_ManSaveValue

(

Gia_Man_t *

p

)

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

Synopsis [Save/load value from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 1605 of file giaUtil.c.

{
    Vec_Int_t * vValues;
    Gia_Obj_t * pObj;
    int i;
    vValues = Vec_IntAlloc( Gia_ManObjNum(p) );
    Gia_ManForEachObj( p, pObj, i )
        Vec_IntPush( vValues, pObj->Value );
    return vValues;
}

int Gia_ManSetLevels	(	Gia_Man_t *	p,
		Vec_Int_t *	vCiLevels
	)

Definition at line 558 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    if ( vCiLevels == NULL )
        return Gia_ManLevelNum( p );
    assert( Vec_IntSize(vCiLevels) == Gia_ManCiNum(p) );
    Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
    p->nLevels = 0;
    Gia_ManForEachCi( p, pObj, i )
    {
        Gia_ObjSetLevel( p, pObj, Vec_IntEntry(vCiLevels, i) );
        p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
    }
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
            Gia_ObjSetGateLevel( p, pObj );
        else if ( Gia_ObjIsCo(pObj) )
            Gia_ObjSetCoLevel( p, pObj );
        else continue;
        p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
    }
    return p->nLevels;
}

void Gia_ManSetMark0

(

Gia_Man_t *

p

)

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

Synopsis [Sets phases of the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
        pObj->fMark0 = 1;
}

void Gia_ManSetMark1

(

Gia_Man_t *

p

)

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

Synopsis [Sets phases of the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
        pObj->fMark1 = 1;
}

void Gia_ManSetPhase

(

Gia_Man_t *

p

)

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

Synopsis [Sets phases of the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 379 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj( p, pObj, i )
        Gia_ObjSetPhase( p, pObj );
}

void Gia_ManSetPhase1

(

Gia_Man_t *

p

)

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

Synopsis [Sets phases of the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 409 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachCi( p, pObj, i )
        pObj->fPhase = 1;
    Gia_ManForEachObj( p, pObj, i )
        if ( !Gia_ObjIsCi(pObj) )
            Gia_ObjSetPhase( p, pObj );
}

void Gia_ManSetPhasePattern	(	Gia_Man_t *	p,
		Vec_Int_t *	vCiValues
	)

Definition at line 386 of file giaUtil.c.

{
    Gia_Obj_t * pObj;
    int i;
    assert( Gia_ManCiNum(p) == Vec_IntSize(vCiValues) );
    Gia_ManForEachObj( p, pObj, i )
        if ( Gia_ObjIsCi(pObj) )
            pObj->fPhase = Vec_IntEntry( vCiValues, Gia_ObjCioId(pObj) );
        else
            Gia_ObjSetPhase( p, pObj );
}

void Gia_ManSwapPos	(	Gia_Man_t *	p,
		int	i
	)

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

Synopsis [Swaps PO number 0 with PO number i.]

Description []

SideEffects []

SeeAlso []

Definition at line 1582 of file giaUtil.c.

{
    int Lit0, LitI;
    assert( i >= 0 && i < Gia_ManPoNum(p) );
    if ( i == 0 )
        return;
    Lit0 = Gia_ObjFaninLit0p( p, Gia_ManPo(p, 0) );
    LitI = Gia_ObjFaninLit0p( p, Gia_ManPo(p, i) );
    Gia_ManPatchCoDriver( p, 0, LitI );
    Gia_ManPatchCoDriver( p, i, Lit0 );
}

int Gia_NodeDeref_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pNode
	)

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

Synopsis [Dereferences the node's MFFC.]

Description []

SideEffects []

SeeAlso []

Definition at line 1058 of file giaUtil.c.

{
    Gia_Obj_t * pFanin;
    int Counter = 0;
    if ( Gia_ObjIsCi(pNode) )
        return 0;
    assert( Gia_ObjIsAnd(pNode) );
    pFanin = Gia_ObjFanin0(pNode);
    assert( Gia_ObjRefNum(p, pFanin) > 0 );
    if ( Gia_ObjRefDec(p, pFanin) == 0 )
        Counter += Gia_NodeDeref_rec( p, pFanin );
    pFanin = Gia_ObjFanin1(pNode);
    assert( Gia_ObjRefNum(p, pFanin) > 0 );
    if ( Gia_ObjRefDec(p, pFanin) == 0 )
        Counter += Gia_NodeDeref_rec( p, pFanin );
    return Counter + 1;
}

int Gia_NodeMffcSize	(	Gia_Man_t *	p,
		Gia_Obj_t *	pNode
	)

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

Synopsis [Returns the number of internal nodes in the MFFC.]

Description []

SideEffects []

SeeAlso []

Definition at line 1132 of file giaUtil.c.

{
    int ConeSize1, ConeSize2;
    assert( !Gia_IsComplement(pNode) );
    assert( Gia_ObjIsCand(pNode) );
    ConeSize1 = Gia_NodeDeref_rec( p, pNode );
    ConeSize2 = Gia_NodeRef_rec( p, pNode );
    assert( ConeSize1 == ConeSize2 );
    assert( ConeSize1 >= 0 );
    return ConeSize1;
}

int Gia_NodeRef_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pNode
	)

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

Synopsis [References the node's MFFC.]

Description []

SideEffects []

SeeAlso []

Definition at line 1087 of file giaUtil.c.

{
    Gia_Obj_t * pFanin;
    int Counter = 0;
    if ( Gia_ObjIsCi(pNode) )
        return 0;
    assert( Gia_ObjIsAnd(pNode) );
    pFanin = Gia_ObjFanin0(pNode);
    if ( Gia_ObjRefInc(p, pFanin) == 0 )
        Counter += Gia_NodeRef_rec( p, pFanin );
    pFanin = Gia_ObjFanin1(pNode);
    if ( Gia_ObjRefInc(p, pFanin) == 0 )
        Counter += Gia_NodeRef_rec( p, pFanin );
    return Counter + 1;
}

int Gia_ObjIsMuxType

(

Gia_Obj_t *

pNode

)

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

Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]

Description []

SideEffects []

SeeAlso []

Definition at line 885 of file giaUtil.c.

{
    Gia_Obj_t * pNode0, * pNode1;
    // check that the node is regular
    assert( !Gia_IsComplement(pNode) );
    // if the node is not AND, this is not MUX
    if ( !Gia_ObjIsAnd(pNode) || Gia_ObjIsBuf(pNode) )
        return 0;
    // if the children are not complemented, this is not MUX
    if ( !Gia_ObjFaninC0(pNode) || !Gia_ObjFaninC1(pNode) )
        return 0;
    // get children
    pNode0 = Gia_ObjFanin0(pNode);
    pNode1 = Gia_ObjFanin1(pNode);
    // if the children are not ANDs, this is not MUX
    if ( !Gia_ObjIsAnd(pNode0) || !Gia_ObjIsAnd(pNode1) )
        return 0;
    // otherwise the node is MUX iff it has a pair of equal grandchildren
    return (Gia_ObjFanin0(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC0(pNode1))) || 
           (Gia_ObjFanin0(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC1(pNode1))) ||
           (Gia_ObjFanin1(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC0(pNode1))) ||
           (Gia_ObjFanin1(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC1(pNode1)));
}

void Gia_ObjPrint	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis [Verbose printing of the AIG node.]

Description []

SideEffects []

SeeAlso []

Definition at line 1258 of file giaUtil.c.

{
    if ( pObj == NULL )
    {
        printf( "Object is NULL." );
        return;
    }
    if ( Gia_IsComplement(pObj) )
    {
        printf( "Compl " );
        pObj = Gia_Not(pObj);
    }
    assert( !Gia_IsComplement(pObj) );
    printf( "Obj %4d : ", Gia_ObjId(p, pObj) );
    if ( Gia_ObjIsConst0(pObj) )
        printf( "constant 0" );
    else if ( Gia_ObjIsPi(p, pObj) )
        printf( "PI" );
    else if ( Gia_ObjIsPo(p, pObj) )
        printf( "PO( %4d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
    else if ( Gia_ObjIsCi(pObj) )
        printf( "RO( %4d%s )", Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)), (Gia_ObjFaninC0(Gia_ObjRoToRi(p, pObj))? "\'" : " ") );
    else if ( Gia_ObjIsCo(pObj) )
        printf( "RI( %4d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
//    else if ( Gia_ObjIsBuf(pObj) )
//        printf( "BUF( %d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
    else if ( Gia_ObjIsXor(pObj) )
        printf( "XOR( %4d%s, %4d%s )", 
            Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " "), 
            Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " ") );
    else if ( Gia_ObjIsMuxId(p, Gia_ObjId(p, pObj)) )
        printf( "MUX( %4d%s, %4d%s, %4d%s )", 
            Gia_ObjFaninId2p(p, pObj), (Gia_ObjFaninC2(p, pObj)? "\'" : " "), 
            Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " "), 
            Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
    else
        printf( "AND( %4d%s, %4d%s )", 
            Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " "), 
            Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " ") );
    if ( p->pRefs )
        printf( " (refs = %3d)", Gia_ObjRefNum(p, pObj) );
    if ( pObj->fMark0 )
        printf( " mark0" );
    if ( pObj->fMark1 )
        printf( " mark1" );
    printf( "\n" );
/*
    if ( p->pRefs )
    {
        Gia_Obj_t * pFanout;
        int i;
        int iFan = -1; // Suppress "might be used uninitialized"
        printf( "\nFanouts:\n" );
        Gia_ObjForEachFanout( p, pObj, pFanout, iFan, i )
        {
            printf( "    " );
            printf( "Node %4d : ", Gia_ObjId(pFanout) );
            if ( Gia_ObjIsPo(pFanout) )
                printf( "PO( %4d%s )", Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " ") );
            else if ( Gia_ObjIsBuf(pFanout) )
                printf( "BUF( %d%s )", Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " ") );
            else
                printf( "AND( %4d%s, %4d%s )", 
                    Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " "), 
                    Gia_ObjFanin1(pFanout)->Id, (Gia_ObjFaninC1(pFanout)? "\'" : " ") );
            printf( "\n" );
        }
        return;
    }
*/
}

int Gia_ObjRecognizeExor	(	Gia_Obj_t *	pObj,
		Gia_Obj_t **	ppFan0,
		Gia_Obj_t **	ppFan1
	)

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

Synopsis [Recognizes what nodes are inputs of the EXOR.]

Description []

SideEffects []

SeeAlso []

Definition at line 921 of file giaUtil.c.

{
    Gia_Obj_t * p0, * p1;
    assert( !Gia_IsComplement(pObj) );
    if ( !Gia_ObjIsAnd(pObj) || Gia_ObjIsBuf(pObj) )
        return 0;
    assert( Gia_ObjIsAnd(pObj) );
    p0 = Gia_ObjChild0(pObj);
    p1 = Gia_ObjChild1(pObj);
    if ( !Gia_IsComplement(p0) || !Gia_IsComplement(p1) )
        return 0;
    p0 = Gia_Regular(p0);
    p1 = Gia_Regular(p1);
    if ( !Gia_ObjIsAnd(p0) || !Gia_ObjIsAnd(p1) )
        return 0;
    if ( Gia_ObjFanin0(p0) != Gia_ObjFanin0(p1) || Gia_ObjFanin1(p0) != Gia_ObjFanin1(p1) )
        return 0;
    if ( Gia_ObjFaninC0(p0) == Gia_ObjFaninC0(p1) || Gia_ObjFaninC1(p0) == Gia_ObjFaninC1(p1) )
        return 0;
    *ppFan0 = Gia_ObjChild0(p0);
    *ppFan1 = Gia_ObjChild1(p0);
    return 1;
}

Gia_Obj_t* Gia_ObjRecognizeMux	(	Gia_Obj_t *	pNode,
		Gia_Obj_t **	ppNodeT,
		Gia_Obj_t **	ppNodeE
	)

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

Synopsis [Recognizes what nodes are control and data inputs of a MUX.]

Description [If the node is a MUX, returns the control variable C. Assigns nodes T and E to be the then and else variables of the MUX. Node C is never complemented. Nodes T and E can be complemented. This function also recognizes EXOR/NEXOR gates as MUXes.]

SideEffects []

SeeAlso []

Definition at line 959 of file giaUtil.c.

{
    Gia_Obj_t * pNode0, * pNode1;
    assert( !Gia_IsComplement(pNode) );
    assert( Gia_ObjIsMuxType(pNode) );
    // get children
    pNode0 = Gia_ObjFanin0(pNode);
    pNode1 = Gia_ObjFanin1(pNode);

    // find the control variable
    if ( Gia_ObjFanin1(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC1(pNode1)) )
    {
//        if ( FrGia_IsComplement(pNode1->p2) )
        if ( Gia_ObjFaninC1(pNode0) )
        { // pNode2->p2 is positive phase of C
            *ppNodeT = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
            *ppNodeE = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
            return Gia_ObjChild1(pNode1);//pNode2->p2;
        }
        else
        { // pNode1->p2 is positive phase of C
            *ppNodeT = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
            *ppNodeE = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
            return Gia_ObjChild1(pNode0);//pNode1->p2;
        }
    }
    else if ( Gia_ObjFanin0(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC0(pNode1)) )
    {
//        if ( FrGia_IsComplement(pNode1->p1) )
        if ( Gia_ObjFaninC0(pNode0) )
        { // pNode2->p1 is positive phase of C
            *ppNodeT = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
            *ppNodeE = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
            return Gia_ObjChild0(pNode1);//pNode2->p1;
        }
        else
        { // pNode1->p1 is positive phase of C
            *ppNodeT = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
            *ppNodeE = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
            return Gia_ObjChild0(pNode0);//pNode1->p1;
        }
    }
    else if ( Gia_ObjFanin0(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC1(pNode1)) )
    {
//        if ( FrGia_IsComplement(pNode1->p1) )
        if ( Gia_ObjFaninC0(pNode0) )
        { // pNode2->p2 is positive phase of C
            *ppNodeT = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
            *ppNodeE = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
            return Gia_ObjChild1(pNode1);//pNode2->p2;
        }
        else
        { // pNode1->p1 is positive phase of C
            *ppNodeT = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
            *ppNodeE = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
            return Gia_ObjChild0(pNode0);//pNode1->p1;
        }
    }
    else if ( Gia_ObjFanin1(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC0(pNode1)) )
    {
//        if ( FrGia_IsComplement(pNode1->p2) )
        if ( Gia_ObjFaninC1(pNode0) )
        { // pNode2->p1 is positive phase of C
            *ppNodeT = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
            *ppNodeE = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
            return Gia_ObjChild0(pNode1);//pNode2->p1;
        }
        else
        { // pNode1->p2 is positive phase of C
            *ppNodeT = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
            *ppNodeE = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
            return Gia_ObjChild1(pNode0);//pNode1->p2;
        }
    }
    assert( 0 ); // this is not MUX
    return NULL;
}

int Gia_ObjRecognizeMuxLits	(	Gia_Man_t *	p,
		Gia_Obj_t *	pNode,
		int *	iLitT,
		int *	iLitE
	)

Definition at line 1036 of file giaUtil.c.

{
    Gia_Obj_t * pNodeT, * pNodeE;
    Gia_Obj_t * pCtrl = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
    assert( pCtrl != NULL );
    *iLitT = Gia_Obj2Lit( p, pNodeT );
    *iLitE = Gia_Obj2Lit( p, pNodeE );
    return Gia_Obj2Lit( p, pCtrl );
}

void Gia_ObjSetPhase	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis [Sets the phase of one object.]

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file giaUtil.c.

{
    if ( Gia_ObjIsAnd(pObj) )
    {
        int fPhase0 = Gia_ObjPhase(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC0(pObj);
        int fPhase1 = Gia_ObjPhase(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(pObj);
        if ( Gia_ObjIsMux(p, pObj) )
        {
            int fPhase2 = Gia_ObjPhase(Gia_ObjFanin2(p, pObj)) ^ Gia_ObjFaninC2(p, pObj);
            pObj->fPhase = (fPhase2 && fPhase1) || (!fPhase2 && fPhase0);
        }
        else if ( Gia_ObjIsXor(pObj) )
            pObj->fPhase = fPhase0 ^ fPhase1;
        else
            pObj->fPhase = fPhase0 & fPhase1;
    }
    else if ( Gia_ObjIsCo(pObj) )
        pObj->fPhase = (Gia_ObjPhase(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC0(pObj));
    else
        pObj->fPhase = 0;
}

char* Gia_TimeStamp

(

)

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

Synopsis [Returns the time stamp.]

Description [The file should be closed.]

SideEffects []

SeeAlso []

Definition at line 101 of file giaUtil.c.

{
    static char Buffer[100];
    char * TimeStamp;
    time_t ltime;
    // get the current time
    time( &ltime );
    TimeStamp = asctime( localtime( &ltime ) );
    TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
    strcpy( Buffer, TimeStamp );
    return Buffer;
}