saigWnd.c File Reference

#include "saig.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	Saig_ManWindowOutline_rec (Aig_Man_t *p, Aig_Obj_t *pObj, int nDist, Vec_Ptr_t *vNodes, int *pDists)
	DECLARATIONS ///. More...
Vec_Ptr_t *	Saig_ManWindowOutline (Aig_Man_t *p, Aig_Obj_t *pObj, int nDist)
Aig_Obj_t *	Saig_ObjHasUnlabeledFanout (Aig_Man_t *p, Aig_Obj_t *pObj)
Vec_Ptr_t *	Saig_ManWindowCollectPis (Aig_Man_t *p, Vec_Ptr_t *vNodes)
Vec_Ptr_t *	Saig_ManWindowCollectPos (Aig_Man_t *p, Vec_Ptr_t *vNodes, Vec_Ptr_t **pvPointers)
Aig_Man_t *	Saig_ManWindowExtractNodes (Aig_Man_t *p, Vec_Ptr_t *vNodes)
static void	Saig_ManWindowInsertSmall_rec (Aig_Man_t *pNew, Aig_Obj_t *pObjSmall, Vec_Ptr_t *vBigNode2SmallPo, Vec_Ptr_t *vSmallPi2BigNode)
void	Saig_ManWindowInsertBig_rec (Aig_Man_t *pNew, Aig_Obj_t *pObjBig, Vec_Ptr_t *vBigNode2SmallPo, Vec_Ptr_t *vSmallPi2BigNode)
Aig_Man_t *	Saig_ManWindowInsertNodes (Aig_Man_t *p, Vec_Ptr_t *vNodes, Aig_Man_t *pWnd)
Aig_Obj_t *	Saig_ManFindPivot (Aig_Man_t *p)
Aig_Man_t *	Saig_ManWindowExtract (Aig_Man_t *p, Aig_Obj_t *pObj, int nDist)
Aig_Man_t *	Saig_ManWindowInsert (Aig_Man_t *p, Aig_Obj_t *pObj, int nDist, Aig_Man_t *pWnd)
Aig_Man_t *	Saig_ManWindowTest (Aig_Man_t *p)
Vec_Ptr_t *	Saig_ManCollectedDiffNodes (Aig_Man_t *p0, Aig_Man_t *p1)
void	Saig_ManWindowCreatePis (Aig_Man_t *pNew, Aig_Man_t *p0, Aig_Man_t *p1, Vec_Ptr_t *vNodes0)
void	Saig_ManWindowCreatePos (Aig_Man_t *pNew, Aig_Man_t *p0, Aig_Man_t *p1)
Aig_Man_t *	Saig_ManWindowExtractMiter (Aig_Man_t *p0, Aig_Man_t *p1)

Function Documentation

Vec_Ptr_t* Saig_ManCollectedDiffNodes	(	Aig_Man_t *	p0,
		Aig_Man_t *	p1
	)

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

Synopsis [Collects the nodes that are not linked to each other.]

Description []

SideEffects []

SeeAlso []

Definition at line 552 of file saigWnd.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj0, * pObj1;
    int i;
    // collect nodes that are not linked
    Aig_ManIncrementTravId( p0 );
    vNodes = Vec_PtrAlloc( 1000 );
    Aig_ManForEachObj( p0, pObj0, i )
    {
        pObj1 = Aig_ObjRepr( p0, pObj0 );
        if ( pObj1 != NULL )
        {
            assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );   
            continue;
        }
        // mark and collect unmatched objects
        Aig_ObjSetTravIdCurrent( p0, pObj0 ); 
        if ( Aig_ObjIsNode(pObj0) || Aig_ObjIsCi(pObj0) )
            Vec_PtrPush( vNodes, pObj0 );
    }
    // make sure LI/LO are labeled/unlabeled mutually
    Saig_ManForEachLiLo( p0, pObj0, pObj1, i )
        assert( Aig_ObjIsTravIdCurrent(p0, pObj0) == 
                Aig_ObjIsTravIdCurrent(p0, pObj1) );
    return vNodes;
}

Aig_Obj_t* Saig_ManFindPivot

(

Aig_Man_t *

p

)

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

Synopsis [Find a good object.]

Description []

SideEffects []

SeeAlso []

Definition at line 427 of file saigWnd.c.

{
    Aig_Obj_t * pObj;
    int i, Counter;
    if ( Aig_ManRegNum(p) > 0 )
    {
        if ( Aig_ManRegNum(p) == 1 )
            return Saig_ManLo( p, 0 );
        Saig_ManForEachLo( p, pObj, i )
        {
            if ( i == Aig_ManRegNum(p)/2 )
                return pObj;
        }
    }
    else
    {
        Counter = 0;
        assert( Aig_ManNodeNum(p) > 1 );
        Aig_ManForEachNode( p, pObj, i )
        {
            if ( Counter++ == Aig_ManNodeNum(p)/2 )
                return pObj;
        }
    }
    return NULL;
}

Vec_Ptr_t* Saig_ManWindowCollectPis	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vNodes
	)

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

Synopsis [Collects primary inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file saigWnd.c.

{
    Vec_Ptr_t * vNodesPi;
    Aig_Obj_t * pObj, * pMatch, * pFanin;
    int i;
    vNodesPi = Vec_PtrAlloc( 1000 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        if ( Saig_ObjIsPi(p, pObj) )
        {
            assert( pObj->pData == NULL );
            Vec_PtrPush( vNodesPi, pObj );
        }
        else if ( Saig_ObjIsLo(p, pObj) )
        {
            pMatch = Saig_ObjLoToLi( p, pObj );
            pFanin = Aig_ObjFanin0(pMatch);
            if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
                Vec_PtrPush( vNodesPi, pFanin );
        }
        else
        {
            assert( Aig_ObjIsNode(pObj) );
            pFanin = Aig_ObjFanin0(pObj);
            if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
                Vec_PtrPush( vNodesPi, pFanin );
            pFanin = Aig_ObjFanin1(pObj);
            if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
                Vec_PtrPush( vNodesPi, pFanin );
        }
    }
    return vNodesPi;
}

Vec_Ptr_t* Saig_ManWindowCollectPos	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vNodes,
		Vec_Ptr_t **	pvPointers
	)

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

Synopsis [Collects primary outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 195 of file saigWnd.c.

{
    Vec_Ptr_t * vNodesPo;
    Aig_Obj_t * pObj, * pPointer;
    int i;
    vNodesPo = Vec_PtrAlloc( 1000 );
    if ( pvPointers )
        *pvPointers = Vec_PtrAlloc( 1000 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        if ( (pPointer = Saig_ObjHasUnlabeledFanout(p, pObj)) )
        {
            Vec_PtrPush( vNodesPo, pObj );
            if ( pvPointers )
                Vec_PtrPush( *pvPointers, pPointer );
        }
    }
    return vNodesPo;
}

void Saig_ManWindowCreatePis	(	Aig_Man_t *	pNew,
		Aig_Man_t *	p0,
		Aig_Man_t *	p1,
		Vec_Ptr_t *	vNodes0
	)

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

Synopsis [Creates PIs of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 591 of file saigWnd.c.

{
    Aig_Obj_t * pObj, * pMatch, * pFanin;
    int i, Counter = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj, i )
    {
        if ( Saig_ObjIsLo(p0, pObj) )
        {
            pMatch = Saig_ObjLoToLi( p0, pObj );
            pFanin = Aig_ObjFanin0(pMatch);
            if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
            {
                pFanin->pData = Aig_ObjCreateCi(pNew);
                pMatch = Aig_ObjRepr( p0, pFanin );
                assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
                assert( pMatch != NULL );
                pMatch->pData = pFanin->pData;
                Counter++;
            }
        }
        else
        {
            assert( Aig_ObjIsNode(pObj) );
            pFanin = Aig_ObjFanin0(pObj);
            if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
            {
                pFanin->pData = Aig_ObjCreateCi(pNew);
                pMatch = Aig_ObjRepr( p0, pFanin );
                assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
                assert( pMatch != NULL );
                pMatch->pData = pFanin->pData;
                Counter++;
            }
            pFanin = Aig_ObjFanin1(pObj);
            if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
            {
                pFanin->pData = Aig_ObjCreateCi(pNew);
                pMatch = Aig_ObjRepr( p0, pFanin );
                assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
                assert( pMatch != NULL );
                pMatch->pData = pFanin->pData;
                Counter++;
            }
        }
    }
//    printf( "Added %d primary inputs.\n", Counter );
}

void Saig_ManWindowCreatePos	(	Aig_Man_t *	pNew,
		Aig_Man_t *	p0,
		Aig_Man_t *	p1
	)

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

Synopsis [Creates POs of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 650 of file saigWnd.c.

{
    Aig_Obj_t * pObj0, * pObj1, * pMiter;
    Aig_Obj_t * pFanin0, * pFanin1;
    int i;
    Aig_ManForEachObj( p0, pObj0, i )
    {
        if ( Aig_ObjIsTravIdCurrent(p0, pObj0) )
            continue;
        if ( Aig_ObjIsConst1(pObj0) )
            continue;
        if ( Aig_ObjIsCi(pObj0) )
            continue;
        pObj1 = Aig_ObjRepr( p0, pObj0 );
        assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
        if ( Aig_ObjIsCo(pObj0) )
        {
            pFanin0 = Aig_ObjFanin0(pObj0);
            pFanin1 = Aig_ObjFanin0(pObj1);
            assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
                    Aig_ObjIsTravIdCurrent(p1, pFanin1) );
            if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
            {
                pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData );
                Aig_ObjCreateCo( pNew, pMiter );
            }
        }
        else
        {
            assert( Aig_ObjIsNode(pObj0) );

            pFanin0 = Aig_ObjFanin0(pObj0);
            pFanin1 = Aig_ObjFanin0(pObj1);
            assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
                    Aig_ObjIsTravIdCurrent(p1, pFanin1) );
            if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
            {
                pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData );
                Aig_ObjCreateCo( pNew, pMiter );
            }

            pFanin0 = Aig_ObjFanin1(pObj0);
            pFanin1 = Aig_ObjFanin1(pObj1);
            assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
                    Aig_ObjIsTravIdCurrent(p1, pFanin1) );
            if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
            {
                pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData );
                Aig_ObjCreateCo( pNew, pMiter );
            }
        }
    }
}

Aig_Man_t* Saig_ManWindowExtract	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		int	nDist
	)

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

Synopsis [Computes sequential window of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 465 of file saigWnd.c.

{
    Aig_Man_t * pWnd;
    Vec_Ptr_t * vNodes;
    Aig_ManFanoutStart( p );
    vNodes = Saig_ManWindowOutline( p, pObj, nDist );
    pWnd = Saig_ManWindowExtractNodes( p, vNodes );
    Vec_PtrFree( vNodes );
    Aig_ManFanoutStop( p );
    return pWnd;
}

Aig_Man_t* Saig_ManWindowExtractMiter	(	Aig_Man_t *	p0,
		Aig_Man_t *	p1
	)

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

Synopsis [Extracts the window AIG from the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 716 of file saigWnd.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj0, * pObj1, * pMatch0, * pMatch1;
    Vec_Ptr_t * vNodes0, * vNodes1;
    int i, nRegCount;
    // add matching of POs and LIs
    Saig_ManForEachPo( p0, pObj0, i )
    {
        pObj1 = Aig_ManCo( p1, i );
        Aig_ObjSetRepr( p0, pObj0, pObj1 );
        Aig_ObjSetRepr( p1, pObj1, pObj0 );
    }
    Saig_ManForEachLi( p0, pObj0, i )
    {
        pMatch0 = Saig_ObjLiToLo( p0, pObj0 );
        pMatch1 = Aig_ObjRepr( p0, pMatch0 );
        if ( pMatch1 == NULL )
            continue;
        assert( pMatch0 == Aig_ObjRepr( p1, pMatch1 ) );
        pObj1 = Saig_ObjLoToLi( p1, pMatch1 );
        Aig_ObjSetRepr( p0, pObj0, pObj1 );
        Aig_ObjSetRepr( p1, pObj1, pObj0 );
    }
    // clean the markings
    Aig_ManCleanData( p0 ); 
    Aig_ManCleanData( p1 ); 
    // collect nodes that are not linked
    vNodes0 = Saig_ManCollectedDiffNodes( p0, p1 );
    vNodes1 = Saig_ManCollectedDiffNodes( p1, p0 );
    // create the new manager
    pNew = Aig_ManStart( Vec_PtrSize(vNodes0) + Vec_PtrSize(vNodes1) );
    pNew->pName = Abc_UtilStrsav( "wnd" );
    pNew->pSpec = NULL;
    // map constant nodes
    pObj0 = Aig_ManConst1( p0 );
    pObj0->pData = Aig_ManConst1( pNew );
    pObj1 = Aig_ManConst1( p1 );
    pObj1->pData = Aig_ManConst1( pNew );
    // create real PIs
    Saig_ManWindowCreatePis( pNew, p0, p1, vNodes0 );
    Saig_ManWindowCreatePis( pNew, p1, p0, vNodes1 );
    // create register outputs
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i )
    {
        if ( Saig_ObjIsLo(p0, pObj0) )
            pObj0->pData = Aig_ObjCreateCi(pNew);
    }
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i )
    {
        if ( Saig_ObjIsLo(p1, pObj1) )
            pObj1->pData = Aig_ObjCreateCi(pNew);
    }
    // create internal nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i )
    {
        if ( Aig_ObjIsNode(pObj0) )
            pObj0->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) );
    }
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i )
    {
        if ( Aig_ObjIsNode(pObj1) )
            pObj1->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj1), Aig_ObjChild1Copy(pObj1) );
    }
    // create POs
    Saig_ManWindowCreatePos( pNew, p0, p1 );
//    Saig_ManWindowCreatePos( pNew, p1, p0 );
    // create register inputs
    nRegCount = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i )
    {
        if ( Saig_ObjIsLo(p0, pObj0) )
        {
            pMatch0 = Saig_ObjLoToLi( p0, pObj0 );
            Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch0) );
            nRegCount++;
        }
    }
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i )
    {
        if ( Saig_ObjIsLo(p1, pObj1) )
        {
            pMatch1 = Saig_ObjLoToLi( p1, pObj1 );
            Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch1) );
            nRegCount++;
        }
    }
    Aig_ManSetRegNum( pNew, nRegCount );
    Aig_ManCleanup( pNew );
    Vec_PtrFree( vNodes0 );
    Vec_PtrFree( vNodes1 );
    return pNew;
}

Aig_Man_t* Saig_ManWindowExtractNodes	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vNodes
	)

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

Synopsis [Extracts the window AIG from the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 226 of file saigWnd.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pMatch;
    Vec_Ptr_t * vNodesPi, * vNodesPo;
    int i, nRegCount;
    Aig_ManCleanData( p ); 
    // create the new manager
    pNew = Aig_ManStart( Vec_PtrSize(vNodes) );
    pNew->pName = Abc_UtilStrsav( "wnd" );
    pNew->pSpec = NULL;
    // map constant nodes
    pObj = Aig_ManConst1( p );
    pObj->pData = Aig_ManConst1( pNew );
    // create real PIs
    vNodesPi = Saig_ManWindowCollectPis( p, vNodes );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPi, pObj, i )
        pObj->pData = Aig_ObjCreateCi(pNew);
    Vec_PtrFree( vNodesPi );
    // create register outputs
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        if ( Saig_ObjIsLo(p, pObj) )
            pObj->pData = Aig_ObjCreateCi(pNew);
    }
    // create internal nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        if ( Aig_ObjIsNode(pObj) )
            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }
    // create POs
    vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPo, pObj, i )
        Aig_ObjCreateCo( pNew, (Aig_Obj_t *)pObj->pData );
    Vec_PtrFree( vNodesPo );
    // create register inputs
    nRegCount = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        if ( Saig_ObjIsLo(p, pObj) )
        {
            pMatch = Saig_ObjLoToLi( p, pObj );
            Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
            nRegCount++;
        }
    }
    Aig_ManSetRegNum( pNew, nRegCount );
    Aig_ManCleanup( pNew );
    return pNew;
}

Aig_Man_t* Saig_ManWindowInsert	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		int	nDist,
		Aig_Man_t *	pWnd
	)

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

Synopsis [Computes sequential window of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 488 of file saigWnd.c.

{
    Aig_Man_t * pNew, * pWndTest;
    Vec_Ptr_t * vNodes;
    Aig_ManFanoutStart( p );

    vNodes = Saig_ManWindowOutline( p, pObj, nDist );
    pWndTest = Saig_ManWindowExtractNodes( p, vNodes );
    if ( Saig_ManPiNum(pWndTest) != Saig_ManPiNum(pWnd) ||
         Saig_ManPoNum(pWndTest) != Saig_ManPoNum(pWnd) )
    {
        printf( "The window cannot be reinserted because PI/PO counts do not match.\n" );
        Aig_ManStop( pWndTest );
        Vec_PtrFree( vNodes );
        Aig_ManFanoutStop( p );
        return NULL;
    }
    Aig_ManStop( pWndTest );
    Vec_PtrFree( vNodes );

    // insert the nodes
    Aig_ManCleanData( p ); 
    vNodes = Saig_ManWindowOutline( p, pObj, nDist );
    pNew = Saig_ManWindowInsertNodes( p, vNodes, pWnd );
    Vec_PtrFree( vNodes );
    Aig_ManFanoutStop( p );
    return pNew;
}

void Saig_ManWindowInsertBig_rec	(	Aig_Man_t *	pNew,
		Aig_Obj_t *	pObjBig,
		Vec_Ptr_t *	vBigNode2SmallPo,
		Vec_Ptr_t *	vSmallPi2BigNode
	)

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

Synopsis [Adds nodes for the big manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 292 of file saigWnd.c.

{
    Aig_Obj_t * pMatch;
    if ( pObjBig->pData )
        return;
    if ( (pMatch = (Aig_Obj_t *)Vec_PtrEntry( vBigNode2SmallPo, pObjBig->Id )) )
    {
        Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pMatch), vBigNode2SmallPo, vSmallPi2BigNode );
        pObjBig->pData = Aig_ObjChild0Copy(pMatch);
        return;        
    }
    assert( Aig_ObjIsNode(pObjBig) );
    Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin0(pObjBig), vBigNode2SmallPo, vSmallPi2BigNode );
    Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin1(pObjBig), vBigNode2SmallPo, vSmallPi2BigNode );
    pObjBig->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObjBig), Aig_ObjChild1Copy(pObjBig) );
}

Aig_Man_t* Saig_ManWindowInsertNodes	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vNodes,
		Aig_Man_t *	pWnd
	)

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

Synopsis [Extracts the network from the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file saigWnd.c.

{
    Aig_Man_t * pNew;
    Vec_Ptr_t * vBigNode2SmallPo, * vSmallPi2BigNode;
    Vec_Ptr_t * vNodesPi, * vNodesPo;
    Aig_Obj_t * pObj;
    int i;

    // set mapping of small PIs into big nodes
    vSmallPi2BigNode = Vec_PtrStart( Aig_ManObjNumMax(pWnd) ); 
    vNodesPi = Saig_ManWindowCollectPis( p, vNodes );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPi, pObj, i )
        Vec_PtrWriteEntry( vSmallPi2BigNode, Aig_ManCi(pWnd, i)->Id, pObj );
    assert( i == Saig_ManPiNum(pWnd) );
    Vec_PtrFree( vNodesPi );

    // set mapping of big nodes into small POs
    vBigNode2SmallPo = Vec_PtrStart( Aig_ManObjNumMax(p) ); 
    vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPo, pObj, i )
        Vec_PtrWriteEntry( vBigNode2SmallPo, pObj->Id, Aig_ManCo(pWnd, i) );
    assert( i == Saig_ManPoNum(pWnd) );
    Vec_PtrFree( vNodesPo );

    // create the new manager
    Aig_ManCleanData( p ); 
    Aig_ManCleanData( pWnd ); 
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    // map constant nodes
    pObj = Aig_ManConst1( p );
    pObj->pData = Aig_ManConst1( pNew );
    pObj = Aig_ManConst1( pWnd );
    pObj->pData = Aig_ManConst1( pNew );

    // create real PIs
    Aig_ManForEachCi( p, pObj, i )
        if ( Saig_ObjIsPi(p, pObj) || !Aig_ObjIsTravIdCurrent(p, pObj) )
            pObj->pData = Aig_ObjCreateCi(pNew);
    // create additional latch outputs
    Saig_ManForEachLo( pWnd, pObj, i )
        pObj->pData = Aig_ObjCreateCi(pNew);

    // create internal nodes starting from the big
    Aig_ManForEachCo( p, pObj, i )
        if ( Saig_ObjIsPo(p, pObj) || !Aig_ObjIsTravIdCurrent(p, pObj) )
        {
            Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin0(pObj), vBigNode2SmallPo, vSmallPi2BigNode );
            pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
        }
    // create internal nodes starting from the small
    Saig_ManForEachLi( pWnd, pObj, i )
    {
        Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pObj), vBigNode2SmallPo, vSmallPi2BigNode );
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
    Vec_PtrFree( vBigNode2SmallPo );
    Vec_PtrFree( vSmallPi2BigNode );
    // set the new number of registers
    assert( Aig_ManCiNum(pNew) - Aig_ManCiNum(p) == Aig_ManCoNum(pNew) - Aig_ManCoNum(p) );
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) + (Aig_ManCiNum(pNew) - Aig_ManCiNum(p)) );
    Aig_ManCleanup( pNew );
    return pNew;
}

void Saig_ManWindowInsertSmall_rec ( Aig_Man_t *  pNew, Aig_Obj_t *  pObjSmall, Vec_Ptr_t *  vBigNode2SmallPo, Vec_Ptr_t *  vSmallPi2BigNode  )

static

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

Synopsis [Adds nodes for the small manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file saigWnd.c.

{
    Aig_Obj_t * pMatch;
    if ( pObjSmall->pData )
        return;
    if ( (pMatch = (Aig_Obj_t *)Vec_PtrEntry( vSmallPi2BigNode, pObjSmall->Id )) )
    {
        Saig_ManWindowInsertBig_rec( pNew, pMatch, vBigNode2SmallPo, vSmallPi2BigNode );
        pObjSmall->pData = pMatch->pData;
        return;        
    }
    assert( Aig_ObjIsNode(pObjSmall) );
    Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pObjSmall), vBigNode2SmallPo, vSmallPi2BigNode );
    Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin1(pObjSmall), vBigNode2SmallPo, vSmallPi2BigNode );
    pObjSmall->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObjSmall), Aig_ObjChild1Copy(pObjSmall) );
}

Vec_Ptr_t* Saig_ManWindowOutline	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		int	nDist
	)

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

Synopsis [Returns the array of PI/internal nodes.]

Description [Marks all the visited nodes with the current ID.]

SideEffects []

SeeAlso []

Definition at line 100 of file saigWnd.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObjLi, * pObjLo;
    int * pDists, i;
    pDists = ABC_CALLOC( int, Aig_ManObjNumMax(p) );
    vNodes = Vec_PtrAlloc( 1000 );
    Aig_ManIncrementTravId( p );
    Saig_ManWindowOutline_rec( p, pObj, nDist, vNodes, pDists );
    Vec_PtrSort( vNodes, (int (*)(void))Aig_ObjCompareIdIncrease );
    // make sure LI/LO are labeled/unlabeled mutually
    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
        assert( Aig_ObjIsTravIdCurrent(p, pObjLi) == 
                Aig_ObjIsTravIdCurrent(p, pObjLo) );
    ABC_FREE( pDists );
    return vNodes;
}

ABC_NAMESPACE_IMPL_START void Saig_ManWindowOutline_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		int	nDist,
		Vec_Ptr_t *	vNodes,
		int *	pDists
	)

DECLARATIONS ///.

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

FileName [saigWnd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Sequential windowing.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Returns the array of PI/internal nodes.]

Description [Marks all the visited nodes with the current ID. Does not collect constant node and PO/LI nodes.]

SideEffects []

SeeAlso []

Definition at line 46 of file saigWnd.c.

{
    Aig_Obj_t * pMatch, * pFanout;
    int fCollected, iFanout = -1, i;
    if ( nDist == 0 )
        return;
    if ( pDists[pObj->Id] >= nDist )
        return;
    pDists[pObj->Id] = nDist;
    fCollected = Aig_ObjIsTravIdCurrent( p, pObj );
    Aig_ObjSetTravIdCurrent( p, pObj );    
    if ( Aig_ObjIsConst1(pObj) )
        return;
    if ( Saig_ObjIsPo(p, pObj) )
        return;
    if ( Saig_ObjIsLi(p, pObj) )
    {
        pMatch = Saig_ObjLiToLo( p, pObj );
        if ( !Aig_ObjIsTravIdCurrent( p, pMatch ) )
            Saig_ManWindowOutline_rec( p, pMatch, nDist, vNodes, pDists );
        Saig_ManWindowOutline_rec( p, Aig_ObjFanin0(pObj), nDist-1, vNodes, pDists );
        return;
    }
    if ( !fCollected )
        Vec_PtrPush( vNodes, pObj );
    if ( Saig_ObjIsPi(p, pObj) )
        return;
    if ( Saig_ObjIsLo(p, pObj) )
    {
        pMatch = Saig_ObjLoToLi( p, pObj );
        if ( !Aig_ObjIsTravIdCurrent( p, pMatch ) )
            Saig_ManWindowOutline_rec( p, pMatch, nDist, vNodes, pDists );
        Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
            Saig_ManWindowOutline_rec( p, pFanout, nDist-1, vNodes, pDists );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    Saig_ManWindowOutline_rec( p, Aig_ObjFanin0(pObj), nDist-1, vNodes, pDists );
    Saig_ManWindowOutline_rec( p, Aig_ObjFanin1(pObj), nDist-1, vNodes, pDists );
    Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
        Saig_ManWindowOutline_rec( p, pFanout, nDist-1, vNodes, pDists );
}

Aig_Man_t* Saig_ManWindowTest

(

Aig_Man_t *

p

)

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

Synopsis [Tests the above computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 528 of file saigWnd.c.

{
    int nDist = 3;
    Aig_Man_t * pWnd, * pNew;
    Aig_Obj_t * pPivot;
    pPivot = Saig_ManFindPivot( p );
    assert( pPivot != NULL );
    pWnd = Saig_ManWindowExtract( p, pPivot, nDist );
    pNew = Saig_ManWindowInsert( p, pPivot, nDist, pWnd );
    Aig_ManStop( pWnd );
    return pNew;
}

Aig_Obj_t* Saig_ObjHasUnlabeledFanout	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Returns 1 if the node has unlabeled fanout.]

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file saigWnd.c.

{
    Aig_Obj_t * pFanout;
    int iFanout = -1, i;
    Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
        if ( Saig_ObjIsPo(p, pFanout) || !Aig_ObjIsTravIdCurrent(p, pFanout) )
            return pFanout;
    return NULL;
}