aigDfs.c File Reference

#include "aig.h"
#include "misc/tim/tim.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START int	Aig_ManVerifyTopoOrder (Aig_Man_t *p)
	DECLARATIONS ///. More...
void	Aig_ManDfs_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Vec_Ptr_t *	Aig_ManDfs (Aig_Man_t *p, int fNodesOnly)
void	Aig_ManDfsAll_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Vec_Ptr_t *	Aig_ManDfsAll (Aig_Man_t *p)
void	Aig_ManDfsPreorder_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Vec_Ptr_t *	Aig_ManDfsPreorder (Aig_Man_t *p, int fNodesOnly)
Vec_Vec_t *	Aig_ManLevelize (Aig_Man_t *p)
Vec_Ptr_t *	Aig_ManDfsNodes (Aig_Man_t *p, Aig_Obj_t **ppNodes, int nNodes)
void	Aig_ManDfsChoices_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Vec_Ptr_t *	Aig_ManDfsChoices (Aig_Man_t *p)
void	Aig_ManDfsReverse_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Vec_Ptr_t *	Aig_ManDfsReverse (Aig_Man_t *p)
int	Aig_ManLevelNum (Aig_Man_t *p)
void	Aig_ManChoiceLevel_rec (Aig_Man_t *p, Aig_Obj_t *pObj)
int	Aig_ManChoiceLevel (Aig_Man_t *p)
void	Aig_ConeMark_rec (Aig_Obj_t *pObj)
void	Aig_ConeCleanAndMark_rec (Aig_Obj_t *pObj)
int	Aig_ConeCountAndMark_rec (Aig_Obj_t *pObj)
void	Aig_ConeUnmark_rec (Aig_Obj_t *pObj)
int	Aig_DagSize (Aig_Obj_t *pObj)
void	Aig_SupportSize_rec (Aig_Man_t *p, Aig_Obj_t *pObj, int *pCounter)
int	Aig_SupportSize (Aig_Man_t *p, Aig_Obj_t *pObj)
int	Aig_SupportSizeTest (Aig_Man_t *p)
void	Aig_Support_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vSupp)
Vec_Ptr_t *	Aig_Support (Aig_Man_t *p, Aig_Obj_t *pObj)
void	Aig_SupportNodes (Aig_Man_t *p, Aig_Obj_t **ppObjs, int nObjs, Vec_Ptr_t *vSupp)
void	Aig_Transfer_rec (Aig_Man_t *pDest, Aig_Obj_t *pObj)
Aig_Obj_t *	Aig_Transfer (Aig_Man_t *pSour, Aig_Man_t *pDest, Aig_Obj_t *pRoot, int nVars)
void	Aig_Compose_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pFunc, Aig_Obj_t *pVar)
Aig_Obj_t *	Aig_Compose (Aig_Man_t *p, Aig_Obj_t *pRoot, Aig_Obj_t *pFunc, int iVar)
void	Aig_ObjCollectCut_rec (Aig_Obj_t *pNode, Vec_Ptr_t *vNodes)
void	Aig_ObjCollectCut (Aig_Obj_t *pRoot, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes)
int	Aig_ObjCollectSuper_rec (Aig_Obj_t *pRoot, Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
int	Aig_ObjCollectSuper (Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)

Function Documentation

Aig_Obj_t* Aig_Compose	(	Aig_Man_t *	p,
		Aig_Obj_t *	pRoot,
		Aig_Obj_t *	pFunc,
		int	iVar
	)

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

Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]

Description []

SideEffects []

SeeAlso []

Definition at line 966 of file aigDfs.c.

{
    // quit if the PI variable is not defined
    if ( iVar >= Aig_ManCiNum(p) )
    {
        printf( "Aig_Compose(): The PI variable %d is not defined.\n", iVar );
        return NULL;
    }
    // recursively perform composition
    Aig_Compose_rec( p, Aig_Regular(pRoot), pFunc, Aig_ManCi(p, iVar) );
    // clear the markings
    Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
    return Aig_NotCond( (Aig_Obj_t *)Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
}

void Aig_Compose_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Aig_Obj_t *	pFunc,
		Aig_Obj_t *	pVar
	)

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

Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]

Description []

SideEffects []

SeeAlso []

Definition at line 938 of file aigDfs.c.

{
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsMarkA(pObj) )
        return;
    if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsCi(pObj) )
    {
        pObj->pData = pObj == pVar ? pFunc : pObj;
        return;
    }
    Aig_Compose_rec( p, Aig_ObjFanin0(pObj), pFunc, pVar ); 
    Aig_Compose_rec( p, Aig_ObjFanin1(pObj), pFunc, pVar );
    pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
    Aig_ObjSetMarkA( pObj );
}

void Aig_ConeCleanAndMark_rec

(

Aig_Obj_t *

pObj

)

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

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 643 of file aigDfs.c.

{
    assert( !Aig_IsComplement(pObj) );
    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
        return;
    Aig_ConeCleanAndMark_rec( Aig_ObjFanin0(pObj) );
    Aig_ConeCleanAndMark_rec( Aig_ObjFanin1(pObj) );
    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
    Aig_ObjSetMarkA( pObj );
    pObj->pData = NULL;
}

int Aig_ConeCountAndMark_rec

(

Aig_Obj_t *

pObj

)

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

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 666 of file aigDfs.c.

{
    int Counter;
    assert( !Aig_IsComplement(pObj) );
    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
        return 0;
    Counter = 1 + Aig_ConeCountAndMark_rec( Aig_ObjFanin0(pObj) ) + 
        Aig_ConeCountAndMark_rec( Aig_ObjFanin1(pObj) );
    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
    Aig_ObjSetMarkA( pObj );
    return Counter;
}

void Aig_ConeMark_rec

(

Aig_Obj_t *

pObj

)

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

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 621 of file aigDfs.c.

{
    assert( !Aig_IsComplement(pObj) );
    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
        return;
    Aig_ConeMark_rec( Aig_ObjFanin0(pObj) );
    Aig_ConeMark_rec( Aig_ObjFanin1(pObj) );
    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
    Aig_ObjSetMarkA( pObj );
}

void Aig_ConeUnmark_rec

(

Aig_Obj_t *

pObj

)

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

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 690 of file aigDfs.c.

{
    assert( !Aig_IsComplement(pObj) );
    if ( !Aig_ObjIsNode(pObj) || !Aig_ObjIsMarkA(pObj) )
        return;
    Aig_ConeUnmark_rec( Aig_ObjFanin0(pObj) ); 
    Aig_ConeUnmark_rec( Aig_ObjFanin1(pObj) );
    assert( Aig_ObjIsMarkA(pObj) ); // loop detection
    Aig_ObjClearMarkA( pObj );
}

int Aig_DagSize

(

Aig_Obj_t *

pObj

)

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

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 712 of file aigDfs.c.

{
    int Counter;
    Counter = Aig_ConeCountAndMark_rec( Aig_Regular(pObj) );
    Aig_ConeUnmark_rec( Aig_Regular(pObj) );
    return Counter;
}

int Aig_ManChoiceLevel

(

Aig_Man_t *

p

)

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

Synopsis [Computes levels for AIG with choices and white boxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 581 of file aigDfs.c.

{
    Aig_Obj_t * pObj;
    int i, LevelMax = 0;
    Aig_ManForEachObj( p, pObj, i )
        Aig_ObjSetLevel( pObj, 0 );
    Aig_ManSetCioIds( p );
    Aig_ManIncrementTravId( p );
    Aig_ManForEachCo( p, pObj, i )
    {
        Aig_ManChoiceLevel_rec( p, pObj );
        if ( LevelMax < Aig_ObjLevel(pObj) )
            LevelMax = Aig_ObjLevel(pObj);
    }
    // account for dangling boxes
    Aig_ManForEachCi( p, pObj, i )
    {
        Aig_ManChoiceLevel_rec( p, pObj );
        if ( LevelMax < Aig_ObjLevel(pObj) )
            LevelMax = Aig_ObjLevel(pObj);
    }
    Aig_ManCleanCioIds( p );
//    Aig_ManForEachNode( p, pObj, i )
//        assert( Aig_ObjLevel(pObj) > 0 );
    return LevelMax;
} 

void Aig_ManChoiceLevel_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Computes levels for AIG with choices and white boxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 509 of file aigDfs.c.

{
    Aig_Obj_t * pNext;
    int i, iBox, iTerm1, nTerms, LevelMax = 0;
    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
        return;
    Aig_ObjSetTravIdCurrent( p, pObj );
    if ( Aig_ObjIsCi(pObj) )
    {
        if ( p->pManTime )
        {
            iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
            if ( iBox >= 0 ) // this is not a true PI
            {
                iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox );
                nTerms = Tim_ManBoxInputNum( (Tim_Man_t *)p->pManTime, iBox );
                for ( i = 0; i < nTerms; i++ )
                {
                    pNext = Aig_ManCo(p, iTerm1 + i);
                    Aig_ManChoiceLevel_rec( p, pNext );
                    if ( LevelMax < Aig_ObjLevel(pNext) )
                        LevelMax = Aig_ObjLevel(pNext);
                }
                LevelMax++;
            }
        }
//        printf( "%d ", pObj->Level );
    }
    else if ( Aig_ObjIsCo(pObj) )
    {
        pNext = Aig_ObjFanin0(pObj);
        Aig_ManChoiceLevel_rec( p, pNext );
        if ( LevelMax < Aig_ObjLevel(pNext) )
            LevelMax = Aig_ObjLevel(pNext);
    }
    else if ( Aig_ObjIsNode(pObj) )
    { 
        // get the maximum level of the two fanins
        pNext = Aig_ObjFanin0(pObj);
        Aig_ManChoiceLevel_rec( p, pNext );
        if ( LevelMax < Aig_ObjLevel(pNext) )
            LevelMax = Aig_ObjLevel(pNext);
        pNext = Aig_ObjFanin1(pObj);
        Aig_ManChoiceLevel_rec( p, pNext );
        if ( LevelMax < Aig_ObjLevel(pNext) )
            LevelMax = Aig_ObjLevel(pNext);
        LevelMax++;

        // get the level of the nodes in the choice node
        if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
        {
            Aig_ManChoiceLevel_rec( p, pNext );
            if ( LevelMax < Aig_ObjLevel(pNext) )
                LevelMax = Aig_ObjLevel(pNext);
        }
    }
    else if ( !Aig_ObjIsConst1(pObj) )
        assert( 0 );
    Aig_ObjSetLevel( pObj, LevelMax );
}

Vec_Ptr_t* Aig_ManDfs	(	Aig_Man_t *	p,
		int	fNodesOnly
	)

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

Synopsis [Collects objects of the AIG in the DFS order.]

Description [Works with choice nodes.]

SideEffects []

SeeAlso []

Definition at line 145 of file aigDfs.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i;
    Aig_ManIncrementTravId( p );
    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
    // start the array of nodes
    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
    // mark PIs if they should not be collected
    if ( fNodesOnly )
        Aig_ManForEachCi( p, pObj, i )
            Aig_ObjSetTravIdCurrent( p, pObj );
    else
        Vec_PtrPush( vNodes, Aig_ManConst1(p) );
    // collect nodes reachable in the DFS order
    Aig_ManForEachCo( p, pObj, i )
        Aig_ManDfs_rec( p, fNodesOnly? Aig_ObjFanin0(pObj): pObj, vNodes );
    if ( fNodesOnly )
        assert( Vec_PtrSize(vNodes) == Aig_ManNodeNum(p) );
    else
        assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) );
    return vNodes;
}

void Aig_ManDfs_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vNodes
	)

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

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 119 of file aigDfs.c.

{
    if ( pObj == NULL )
        return;
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
        Aig_ManDfs_rec( p, Aig_ObjEquiv(p, pObj), vNodes );
    Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
    Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
    Vec_PtrPush( vNodes, pObj );
}

Vec_Ptr_t* Aig_ManDfsAll

(

Aig_Man_t *

p

)

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

Synopsis [Collects objects of the AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file aigDfs.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i;
    Aig_ManIncrementTravId( p );
    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
    // add constant
    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
    Vec_PtrPush( vNodes, Aig_ManConst1(p) );
    // collect nodes reachable in the DFS order
    Aig_ManForEachCo( p, pObj, i )
        Aig_ManDfsAll_rec( p, pObj, vNodes );
    Aig_ManForEachCi( p, pObj, i )
        if ( !Aig_ObjIsTravIdCurrent(p, pObj) )
            Vec_PtrPush( vNodes, pObj );
    assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) );
    return vNodes;
}

void Aig_ManDfsAll_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vNodes
	)

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

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file aigDfs.c.

{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( Aig_ObjIsCi(pObj) )
    {
        Vec_PtrPush( vNodes, pObj );
        return;
    }
    if ( Aig_ObjIsCo(pObj) )
    {
        Aig_ManDfsAll_rec( p, Aig_ObjFanin0(pObj), vNodes );
        Vec_PtrPush( vNodes, pObj );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    Aig_ManDfsAll_rec( p, Aig_ObjFanin0(pObj), vNodes );
    Aig_ManDfsAll_rec( p, Aig_ObjFanin1(pObj), vNodes );
    Vec_PtrPush( vNodes, pObj );
}

Vec_Ptr_t* Aig_ManDfsChoices

(

Aig_Man_t *

p

)

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

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 391 of file aigDfs.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i, Counter = 0;

    Aig_ManForEachNode( p, pObj, i )
    {
        if ( Aig_ObjEquiv(p, pObj) == NULL )
            continue;
        Counter = 0;
        for ( pObj = Aig_ObjEquiv(p, pObj) ; pObj; pObj = Aig_ObjEquiv(p, pObj) )
            Counter++;
//        printf( "%d ", Counter );
    }
//    printf( "\n" );

    assert( p->pEquivs != NULL );
    Aig_ManIncrementTravId( p );
    // mark constant and PIs
    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
    Aig_ManForEachCi( p, pObj, i )
        Aig_ObjSetTravIdCurrent( p, pObj );
    // go through the nodes
    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
    Aig_ManForEachCo( p, pObj, i )
        Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
    return vNodes;
}

void Aig_ManDfsChoices_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vNodes
	)

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

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 364 of file aigDfs.c.

{
    if ( pObj == NULL )
        return;
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    assert( Aig_ObjIsNode(pObj) );
    Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
    Aig_ManDfsChoices_rec( p, Aig_ObjFanin1(pObj), vNodes );
    Aig_ManDfsChoices_rec( p, Aig_ObjEquiv(p, pObj), vNodes );
    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
    Aig_ObjSetTravIdCurrent(p, pObj);
    Vec_PtrPush( vNodes, pObj );
}

Vec_Ptr_t* Aig_ManDfsNodes	(	Aig_Man_t *	p,
		Aig_Obj_t **	ppNodes,
		int	nNodes
	)

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

Synopsis [Collects internal nodes and PIs in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 333 of file aigDfs.c.

{
    Vec_Ptr_t * vNodes;
//    Aig_Obj_t * pObj;
    int i;
    Aig_ManIncrementTravId( p );
    // mark constant and PIs
    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
//    Aig_ManForEachCi( p, pObj, i )
//        Aig_ObjSetTravIdCurrent( p, pObj );
    // go through the nodes
    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
    for ( i = 0; i < nNodes; i++ )
        if ( Aig_ObjIsCo(ppNodes[i]) )
            Aig_ManDfs_rec( p, Aig_ObjFanin0(ppNodes[i]), vNodes );
        else
            Aig_ManDfs_rec( p, ppNodes[i], vNodes );
    return vNodes;
}

Vec_Ptr_t* Aig_ManDfsPreorder	(	Aig_Man_t *	p,
		int	fNodesOnly
	)

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

Synopsis [Collects objects of the AIG in the DFS order.]

Description [Works with choice nodes.]

SideEffects []

SeeAlso []

Definition at line 271 of file aigDfs.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i;
    Aig_ManIncrementTravId( p );
    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
    // start the array of nodes
    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
    // mark PIs if they should not be collected
    if ( fNodesOnly )
        Aig_ManForEachCi( p, pObj, i )
            Aig_ObjSetTravIdCurrent( p, pObj );
    else
        Vec_PtrPush( vNodes, Aig_ManConst1(p) );
    // collect nodes reachable in the DFS order
    Aig_ManForEachCo( p, pObj, i )
        Aig_ManDfsPreorder_rec( p, fNodesOnly? Aig_ObjFanin0(pObj): pObj, vNodes );
    if ( fNodesOnly )
        assert( Vec_PtrSize(vNodes) == Aig_ManNodeNum(p) );
    else
        assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) );
    return vNodes;
}

void Aig_ManDfsPreorder_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vNodes
	)

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

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 245 of file aigDfs.c.

{
    if ( pObj == NULL )
        return;
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    Vec_PtrPush( vNodes, pObj );
    if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
        Aig_ManDfs_rec( p, Aig_ObjEquiv(p, pObj), vNodes );
    Aig_ManDfsPreorder_rec( p, Aig_ObjFanin0(pObj), vNodes );
    Aig_ManDfsPreorder_rec( p, Aig_ObjFanin1(pObj), vNodes );
}

Vec_Ptr_t* Aig_ManDfsReverse

(

Aig_Man_t *

p

)

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

Synopsis [Collects internal nodes in the reverse DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 458 of file aigDfs.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i;
    Aig_ManIncrementTravId( p );
    // mark POs
    Aig_ManForEachCo( p, pObj, i )
        Aig_ObjSetTravIdCurrent( p, pObj );
    // go through the nodes
    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
    Aig_ManForEachObj( p, pObj, i )
        if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) )
            Aig_ManDfsReverse_rec( p, pObj, vNodes );
    return vNodes;
}

void Aig_ManDfsReverse_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vNodes
	)

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

Synopsis [Collects internal nodes in the reverse DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 432 of file aigDfs.c.

{
    Aig_Obj_t * pFanout;
    int iFanout = -1, i;
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
    Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
        Aig_ManDfsReverse_rec( p, pFanout, vNodes );
    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
    Aig_ObjSetTravIdCurrent(p, pObj);
    Vec_PtrPush( vNodes, pObj );
}

Vec_Vec_t* Aig_ManLevelize

(

Aig_Man_t *

p

)

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

Synopsis [Levelizes the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file aigDfs.c.

{
    Aig_Obj_t * pObj;
    Vec_Vec_t * vLevels;
    int nLevels, i;
    nLevels = Aig_ManLevelNum( p );
    vLevels = Vec_VecStart( nLevels + 1 );
    Aig_ManForEachObj( p, pObj, i )
    {
        assert( (int)pObj->Level <= nLevels );
        Vec_VecPush( vLevels, pObj->Level, pObj );
    }
    return vLevels;
}

int Aig_ManLevelNum

(

Aig_Man_t *

p

)

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

Synopsis [Computes the max number of levels in the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 486 of file aigDfs.c.

{
    Aig_Obj_t * pObj;
    int i, LevelsMax;
    LevelsMax = 0;
    Aig_ManForEachCo( p, pObj, i )
        LevelsMax = Abc_MaxInt( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
    return LevelsMax;
}

ABC_NAMESPACE_IMPL_START int Aig_ManVerifyTopoOrder

(

Aig_Man_t *

p

)

DECLARATIONS ///.

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

FileName [aigDfs.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [DFS traversal procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id:

aigDfs.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Verifies that the objects are in a topo order.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file aigDfs.c.

{
    Aig_Obj_t * pObj, * pNext;
    int i, k, iBox, iTerm1, nTerms;
    Aig_ManSetCioIds( p );
    Aig_ManIncrementTravId( p );
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( Aig_ObjIsNode(pObj) )
        {
            pNext = Aig_ObjFanin0(pObj);
            if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
            {
                printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
                return 0;
            }
            pNext = Aig_ObjFanin1(pObj);
            if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
            {
                printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
                return 0;
            }
        }
        else if ( Aig_ObjIsCo(pObj) || Aig_ObjIsBuf(pObj) )
        {
            pNext = Aig_ObjFanin0(pObj);
            if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
            {
                printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
                return 0;
            }
        }
        else if ( Aig_ObjIsCi(pObj) )
        {
            if ( p->pManTime )
            {
                iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
                if ( iBox >= 0 ) // this is not a true PI
                {
                    iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox );
                    nTerms = Tim_ManBoxInputNum( (Tim_Man_t *)p->pManTime, iBox );
                    for ( k = 0; k < nTerms; k++ )
                    {
                        pNext = Aig_ManCo( p, iTerm1 + k );
                        assert( Tim_ManBoxForCo( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pNext) ) == iBox ); 
                        if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
                        {
                            printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
                            return 0;
                        }
                    }
                }
            }
        }
        else if ( !Aig_ObjIsConst1(pObj) )
            assert( 0 );
        Aig_ObjSetTravIdCurrent( p, pObj );
    }
    Aig_ManCleanCioIds( p );
    return 1;
}

void Aig_ObjCollectCut	(	Aig_Obj_t *	pRoot,
		Vec_Ptr_t *	vLeaves,
		Vec_Ptr_t *	vNodes
	)

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

Synopsis [Computes the internal nodes of the cut.]

Description [Does not include the leaves of the cut.]

SideEffects []

SeeAlso []

Definition at line 1017 of file aigDfs.c.

{
    Aig_Obj_t * pObj;
    int i;
    // collect and mark the leaves
    Vec_PtrClear( vNodes );
    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
    {
        assert( pObj->fMarkA == 0 );
        pObj->fMarkA = 1;
//        printf( "%d " , pObj->Id );
    }
//printf( "\n" );
    // collect and mark the nodes
    Aig_ObjCollectCut_rec( pRoot, vNodes );
    // clean the nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        pObj->fMarkA = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
        pObj->fMarkA = 0;
}

void Aig_ObjCollectCut_rec	(	Aig_Obj_t *	pNode,
		Vec_Ptr_t *	vNodes
	)

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

Synopsis [Computes the internal nodes of the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 992 of file aigDfs.c.

{
//    Aig_Obj_t * pFan0 = Aig_ObjFanin0(pNode);
//    Aig_Obj_t * pFan1 = Aig_ObjFanin1(pNode);
    if ( pNode->fMarkA )
        return;
    pNode->fMarkA = 1;
    assert( Aig_ObjIsNode(pNode) );
    Aig_ObjCollectCut_rec( Aig_ObjFanin0(pNode), vNodes );
    Aig_ObjCollectCut_rec( Aig_ObjFanin1(pNode), vNodes );
    Vec_PtrPush( vNodes, pNode );
//printf( "added %d  ", pNode->Id );
}

int Aig_ObjCollectSuper	(	Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vSuper
	)

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

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 1097 of file aigDfs.c.

{
    int RetValue, i;
    assert( !Aig_IsComplement(pObj) );
    assert( Aig_ObjIsNode(pObj) );
    // collect the nodes in the implication supergate
    Vec_PtrClear( vSuper );
    RetValue = Aig_ObjCollectSuper_rec( pObj, pObj, vSuper );
    assert( Vec_PtrSize(vSuper) > 1 );
    // unmark the visited nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
        Aig_Regular(pObj)->fMarkA = 0;
    // if we found the node and its complement in the same implication supergate, 
    // return empty set of nodes (meaning that we should use constant-0 node)
    if ( RetValue == -1 )
        vSuper->nSize = 0;
    return RetValue;
}

int Aig_ObjCollectSuper_rec	(	Aig_Obj_t *	pRoot,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vSuper
	)

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

Synopsis [Collects the nodes of the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 1051 of file aigDfs.c.

{
    int RetValue1, RetValue2, i;
    // check if the node is visited
    if ( Aig_Regular(pObj)->fMarkA )
    {
        // check if the node occurs in the same polarity
        for ( i = 0; i < vSuper->nSize; i++ )
            if ( vSuper->pArray[i] == pObj )
                return 1;
        // check if the node is present in the opposite polarity
        for ( i = 0; i < vSuper->nSize; i++ )
            if ( vSuper->pArray[i] == Aig_Not(pObj) )
                return -1;
        assert( 0 );
        return 0;
    }
    // if the new node is complemented or a PI, another gate begins
    if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1) )
    {
        Vec_PtrPush( vSuper, pObj );
        Aig_Regular(pObj)->fMarkA = 1;
        return 0;
    }
    assert( !Aig_IsComplement(pObj) );
    assert( Aig_ObjIsNode(pObj) );
    // go through the branches
    RetValue1 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
    RetValue2 = Aig_ObjCollectSuper_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
    if ( RetValue1 == -1 || RetValue2 == -1 )
        return -1;
    // return 1 if at least one branch has a duplicate
    return RetValue1 || RetValue2;
}

Vec_Ptr_t* Aig_Support	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Counts the support size of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 832 of file aigDfs.c.

{
    Vec_Ptr_t * vSupp;
    assert( !Aig_IsComplement(pObj) );
    assert( !Aig_ObjIsCo(pObj) );
    Aig_ManIncrementTravId( p );
    vSupp = Vec_PtrAlloc( 100 );
    Aig_Support_rec( p, pObj, vSupp );
    return vSupp;
}

void Aig_Support_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vSupp
	)

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

Synopsis [Counts the support size of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 803 of file aigDfs.c.

{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( Aig_ObjIsConst1(pObj) )
        return;
    if ( Aig_ObjIsCi(pObj) )
    {
        Vec_PtrPush( vSupp, pObj );
        return;
    }
    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
    Aig_Support_rec( p, Aig_ObjFanin0(pObj), vSupp );
    if ( Aig_ObjFanin1(pObj) )
        Aig_Support_rec( p, Aig_ObjFanin1(pObj), vSupp );
}

void Aig_SupportNodes	(	Aig_Man_t *	p,
		Aig_Obj_t **	ppObjs,
		int	nObjs,
		Vec_Ptr_t *	vSupp
	)

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

Synopsis [Counts the support size of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 854 of file aigDfs.c.

{
    int i;
    Vec_PtrClear( vSupp );
    Aig_ManIncrementTravId( p );
    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
    for ( i = 0; i < nObjs; i++ )
    {
        assert( !Aig_IsComplement(ppObjs[i]) );
        if ( Aig_ObjIsCo(ppObjs[i]) )
            Aig_Support_rec( p, Aig_ObjFanin0(ppObjs[i]), vSupp );
        else
            Aig_Support_rec( p, ppObjs[i], vSupp );
    }
}

int Aig_SupportSize	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Counts the support size of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 758 of file aigDfs.c.

{
    int Counter = 0;
    assert( !Aig_IsComplement(pObj) );
    assert( !Aig_ObjIsCo(pObj) );
    Aig_ManIncrementTravId( p );
    Aig_SupportSize_rec( p, pObj, &Counter );
    return Counter;
}

void Aig_SupportSize_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		int *	pCounter
	)

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

Synopsis [Counts the support size of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 731 of file aigDfs.c.

{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( Aig_ObjIsCi(pObj) )
    {
        (*pCounter)++;
        return;
    }
    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
    Aig_SupportSize_rec( p, Aig_ObjFanin0(pObj), pCounter );
    if ( Aig_ObjFanin1(pObj) )
        Aig_SupportSize_rec( p, Aig_ObjFanin1(pObj), pCounter );
}

int Aig_SupportSizeTest

(

Aig_Man_t *

p

)

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

Synopsis [Counts the support size of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 779 of file aigDfs.c.

{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    abctime clk = Abc_Clock();
    Aig_ManForEachObj( p, pObj, i )
        if ( Aig_ObjIsNode(pObj) )
            Counter += (Aig_SupportSize(p, pObj) <= 16);
    printf( "Nodes with small support %d (out of %d)\n", Counter, Aig_ManNodeNum(p) );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return Counter;
}

Aig_Obj_t* Aig_Transfer	(	Aig_Man_t *	pSour,
		Aig_Man_t *	pDest,
		Aig_Obj_t *	pRoot,
		int	nVars
	)

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

Synopsis [Transfers the AIG from one manager into another.]

Description []

SideEffects []

SeeAlso []

Definition at line 904 of file aigDfs.c.

{
    Aig_Obj_t * pObj;
    int i;
    // solve simple cases
    if ( pSour == pDest )
        return pRoot;
    if ( Aig_ObjIsConst1( Aig_Regular(pRoot) ) )
        return Aig_NotCond( Aig_ManConst1(pDest), Aig_IsComplement(pRoot) );
    // set the PI mapping
    Aig_ManForEachCi( pSour, pObj, i )
    {
        if ( i == nVars )
           break;
        pObj->pData = Aig_IthVar(pDest, i);
    }
    // transfer and set markings
    Aig_Transfer_rec( pDest, Aig_Regular(pRoot) );
    // clear the markings
    Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
    return Aig_NotCond( (Aig_Obj_t *)Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
}

void Aig_Transfer_rec	(	Aig_Man_t *	pDest,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Transfers the AIG from one manager into another.]

Description []

SideEffects []

SeeAlso []

Definition at line 881 of file aigDfs.c.

{
    assert( !Aig_IsComplement(pObj) );
    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
        return;
    Aig_Transfer_rec( pDest, Aig_ObjFanin0(pObj) ); 
    Aig_Transfer_rec( pDest, Aig_ObjFanin1(pObj) );
    pObj->pData = Aig_And( pDest, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
    Aig_ObjSetMarkA( pObj );
}