#include "giaAig.h"
#include "proof/fra/fra.h"
#include "proof/dch/dch.h"
#include "opt/dar/dar.h"

Functions
static ABC_NAMESPACE_IMPL_START int	Gia_ObjChild0Copy (Aig_Obj_t *pObj)
	DECLARATIONS ///. More...

static int	Gia_ObjChild1Copy (Aig_Obj_t *pObj)

static Aig_Obj_t *	Gia_ObjChild0Copy2 (Aig_Obj_t *ppNodes, Gia_Obj_t pObj, int Id)

static Aig_Obj_t *	Gia_ObjChild1Copy2 (Aig_Obj_t *ppNodes, Gia_Obj_t pObj, int Id)

void	Gia_ManFromAig_rec (Gia_Man_t pNew, Aig_Man_t p, Aig_Obj_t *pObj)
	FUNCTION DEFINITIONS ///. More...

Gia_Man_t *	Gia_ManFromAig (Aig_Man_t *p)
	INCLUDES ///. More...

void	Gia_ManFromAigChoices_rec (Gia_Man_t pNew, Aig_Man_t p, Aig_Obj_t *pObj)

Gia_Man_t *	Gia_ManFromAigChoices (Aig_Man_t *p)

Gia_Man_t *	Gia_ManFromAigSimple (Aig_Man_t *p)

Gia_Man_t *	Gia_ManFromAigSwitch (Aig_Man_t *p)

void	Gia_ManToAig_rec (Aig_Man_t pNew, Aig_Obj_t ppNodes, Gia_Man_t p, Gia_Obj_t *pObj)

Aig_Man_t *	Gia_ManToAig (Gia_Man_t *p, int fChoices)

Aig_Man_t *	Gia_ManToAigSkip (Gia_Man_t *p, int nOutDelta)

Aig_Man_t *	Gia_ManToAigSimple (Gia_Man_t *p)

Aig_Man_t *	Gia_ManCofactorAig (Aig_Man_t *p, int nFrames, int nCofFanLit)

void	Gia_ManReprToAigRepr (Aig_Man_t pAig, Gia_Man_t pGia)

void	Gia_ManReprToAigRepr2 (Aig_Man_t pAig, Gia_Man_t pGia)

void	Gia_ManReprFromAigRepr (Aig_Man_t pAig, Gia_Man_t pGia)

void	Gia_ManReprFromAigRepr2 (Aig_Man_t pAig, Gia_Man_t pGia)

Gia_Man_t *	Gia_ManCompress2 (Gia_Man_t *p, int fUpdateLevel, int fVerbose)

Gia_Man_t *	Gia_ManPerformDch (Gia_Man_t p, void pPars)

void	Gia_ManSeqCleanupClasses (Gia_Man_t *p, int fConst, int fEquiv, int fVerbose)

int	Gia_ManSolveSat (Gia_Man_t *p)

Function Documentation

Aig_Man_t* Gia_ManCofactorAig	(	Aig_Man_t *	p,
		int	nFrames,
		int	nCofFanLit
	)

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 411 of file giaAig.c.

 {
     Aig_Man_t * pMan;
     Gia_Man_t * pGia, * pTemp;
     pGia = Gia_ManFromAig( p );
     pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 );
     Gia_ManStop( pTemp );
     pMan = Gia_ManToAig( pGia, 0 );
     Gia_ManStop( pGia );
     return pMan;
 }

Gia_Man_t* Gia_ManCompress2	(	Gia_Man_t *	p,
		int	fUpdateLevel,
		int	fVerbose
	)

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

Synopsis [Applies DC2 to the GIA manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 551 of file giaAig.c.

 {
     Gia_Man_t * pGia;
     Aig_Man_t * pNew, * pTemp;
     if ( p->pManTime && p->vLevels == NULL )
         Gia_ManLevelWithBoxes( p );
     pNew = Gia_ManToAig( p, 0 );
     pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose );
     Aig_ManStop( pTemp );
     pGia = Gia_ManFromAig( pNew );
     Aig_ManStop( pNew );
     Gia_ManTransferTiming( pGia, p );
     return pGia;
 }

Gia_Man_t* Gia_ManFromAig ( Aig_Man_t * p )

INCLUDES ///.

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

FileName [giaAig.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:: giaAig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///MACRO DEFINITIONS ///FUNCTION DECLARATIONS ///

Definition at line 73 of file giaAig.c.

 {
     Gia_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create room to store equivalences
     if ( p->pEquivs )
         pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->iData = 1;
     Aig_ManForEachCi( p, pObj, i )
         pObj->iData = Gia_ManAppendCi( pNew );
     // add logic for the POs
     Aig_ManForEachCo( p, pObj, i )
         Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
     Aig_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     if ( pNew->pNexts )
         Gia_ManDeriveReprs( pNew );
     return pNew;
 }

void Gia_ManFromAig_rec	(	Gia_Man_t *	pNew,
		Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 54 of file giaAig.c.

 {
     Aig_Obj_t * pNext;
     if ( pObj->iData )
         return;
     assert( Aig_ObjIsNode(pObj) );
     Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
     Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
     if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
     {
         int iObjNew, iNextNew;
         Gia_ManFromAig_rec( pNew, p, pNext );
         iObjNew  = Abc_Lit2Var(pObj->iData);
         iNextNew = Abc_Lit2Var(pNext->iData);
         if ( pNew->pNexts )
             pNew->pNexts[iObjNew] = iNextNew;        
     }
 }

Gia_Man_t* Gia_ManFromAigChoices ( Aig_Man_t * p )

Definition at line 132 of file giaAig.c.

 {
     Gia_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
     assert( p->pEquivs != NULL );
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create room to store equivalences
     pNew->pSibls = ABC_CALLOC( int, Aig_ManObjNum(p) );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->iData = 1;
     Aig_ManForEachCi( p, pObj, i )
         pObj->iData = Gia_ManAppendCi( pNew );
     // add logic for the POs
     Aig_ManForEachCo( p, pObj, i )
         Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );        
     Aig_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
     return pNew;
 }

void Gia_ManFromAigChoices_rec	(	Gia_Man_t *	pNew,
		Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file giaAig.c.

 {
     if ( pObj == NULL || pObj->iData )
         return;
     assert( Aig_ObjIsNode(pObj) );
     Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
     Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin1(pObj) );
     Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
     pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
     if ( Aig_ObjEquiv(p, pObj) )
     {
         int iObjNew, iNextNew;
         iObjNew  = Abc_Lit2Var(pObj->iData);
         iNextNew = Abc_Lit2Var(Aig_ObjEquiv(p, pObj)->iData);
         assert( iObjNew > iNextNew );
         assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) );
         pNew->pSibls[iObjNew] = iNextNew;        
     }
 }

Gia_Man_t* Gia_ManFromAigSimple ( Aig_Man_t * p )

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 171 of file giaAig.c.

 {
     Gia_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManForEachObj( p, pObj, i )
     {
         if ( Aig_ObjIsAnd(pObj) )
             pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
         else if ( Aig_ObjIsCi(pObj) )
             pObj->iData = Gia_ManAppendCi( pNew );
         else if ( Aig_ObjIsCo(pObj) )
             pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
         else if ( Aig_ObjIsConst1(pObj) )
             pObj->iData = 1;
         else
             assert( 0 );
     }
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     return pNew;
 }

Gia_Man_t* Gia_ManFromAigSwitch ( Aig_Man_t * p )

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

Synopsis [Handles choices as additional combinational outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file giaAig.c.

 {
     Gia_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->iData = 1;
     Aig_ManForEachCi( p, pObj, i )
         pObj->iData = Gia_ManAppendCi( pNew );
     // add POs corresponding to the nodes with choices
     Aig_ManForEachNode( p, pObj, i )
         if ( Aig_ObjRefs(pObj) == 0 )
         {
             Gia_ManFromAig_rec( pNew, p, pObj );        
             Gia_ManAppendCo( pNew, pObj->iData );
         }
     // add logic for the POs
     Aig_ManForEachCo( p, pObj, i )
         Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
     Aig_ManForEachCo( p, pObj, i )
         pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     return pNew;
 }

Gia_Man_t* Gia_ManPerformDch	(	Gia_Man_t *	p,
		void *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 577 of file giaAig.c.

 {
     Gia_Man_t * pGia;
     Aig_Man_t * pNew;
     if ( p->pManTime && p->vLevels == NULL )
         Gia_ManLevelWithBoxes( p );
     pNew = Gia_ManToAig( p, 0 );
     pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars );
 //    pGia = Gia_ManFromAig( pNew );
     pGia = Gia_ManFromAigChoices( pNew );
     Aig_ManStop( pNew );
     Gia_ManTransferTiming( pGia, p );
     return pGia;
 }

void Gia_ManReprFromAigRepr	(	Aig_Man_t *	pAig,
		Gia_Man_t *	pGia
	)

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

Synopsis [Transfers representatives from pAig to pGia.]

Description []

SideEffects []

SeeAlso []

Definition at line 487 of file giaAig.c.

 {
     Gia_Obj_t * pObjGia; 
     Aig_Obj_t * pObjAig, * pReprAig;
     int i;
     assert( pAig->pReprs != NULL );
     assert( pGia->pReprs == NULL );
     assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) );
     pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
     for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
         Gia_ObjSetRepr( pGia, i, GIA_VOID );
     // move pointers from GIA to AIG
     Gia_ManForEachObj( pGia, pObjGia, i )
     {
         if ( Gia_ObjIsCo(pObjGia) )
             continue;
         assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) );
         pObjAig  = Aig_ManObj( pAig, Abc_Lit2Var(Gia_ObjValue(pObjGia)) );
         pObjAig->iData = i;
     }
     Aig_ManForEachObj( pAig, pObjAig, i )
     {
         if ( Aig_ObjIsCo(pObjAig) )
             continue;
         if ( pAig->pReprs[i] == NULL )
             continue;
         pReprAig = pAig->pReprs[i];
         Gia_ObjSetRepr( pGia, pObjAig->iData, pReprAig->iData );
     }
     pGia->pNexts = Gia_ManDeriveNexts( pGia );
 }

void Gia_ManReprFromAigRepr2	(	Aig_Man_t *	pAig,
		Gia_Man_t *	pGia
	)

Definition at line 518 of file giaAig.c.

 {
     Aig_Obj_t * pObjAig, * pReprAig;
     int i;
     assert( pAig->pReprs != NULL );
     assert( pGia->pReprs == NULL );
     assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) );
     pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
     for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
         Gia_ObjSetRepr( pGia, i, GIA_VOID );
     Aig_ManForEachObj( pAig, pObjAig, i )
     {
         if ( Aig_ObjIsCo(pObjAig) )
             continue;
         if ( pAig->pReprs[i] == NULL )
             continue;
         pReprAig = pAig->pReprs[i];
         Gia_ObjSetRepr( pGia, Abc_Lit2Var(pObjAig->iData), Abc_Lit2Var(pReprAig->iData) );
     }
     pGia->pNexts = Gia_ManDeriveNexts( pGia );
 }

void Gia_ManReprToAigRepr	(	Aig_Man_t *	pAig,
		Gia_Man_t *	pGia
	)

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

Synopsis [Transfers representatives from pGia to pAig.]

Description [Assumes that pGia was created from pAig.]

SideEffects []

SeeAlso []

Definition at line 435 of file giaAig.c.

 {
     Aig_Obj_t * pObj;
     Gia_Obj_t * pGiaObj, * pGiaRepr;
     int i;
     assert( pAig->pReprs == NULL );
     assert( pGia->pReprs != NULL );
     // move pointers from AIG to GIA
     Aig_ManForEachObj( pAig, pObj, i )
     {
         assert( i == 0 || !Abc_LitIsCompl(pObj->iData) );
         pGiaObj = Gia_ManObj( pGia, Abc_Lit2Var(pObj->iData) );
         pGiaObj->Value = i;
     }
     // set the pointers to the nodes in AIG
     Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
     Gia_ManForEachObj( pGia, pGiaObj, i )
     {
         pGiaRepr = Gia_ObjReprObj( pGia, i );
         if ( pGiaRepr == NULL )
             continue;
         Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, pGiaRepr->Value), Aig_ManObj(pAig, pGiaObj->Value) );
     }
 }

void Gia_ManReprToAigRepr2	(	Aig_Man_t *	pAig,
		Gia_Man_t *	pGia
	)

Definition at line 459 of file giaAig.c.

 {
     Gia_Obj_t * pGiaObj, * pGiaRepr;
     int i;
     assert( pAig->pReprs == NULL );
     assert( pGia->pReprs != NULL );
     // set the pointers to the nodes in AIG
     Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
     Gia_ManForEachObj( pGia, pGiaObj, i )
     {
         pGiaRepr = Gia_ObjReprObj( pGia, i );
         if ( pGiaRepr == NULL )
             continue;
         Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Abc_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Abc_Lit2Var(pGiaObj->Value)) );
     }
 }

void Gia_ManSeqCleanupClasses	(	Gia_Man_t *	p,
		int	fConst,
		int	fEquiv,
		int	fVerbose
	)

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

Synopsis [Computes equivalences after structural sequential cleanup.]

Description []

SideEffects []

SeeAlso []

Definition at line 603 of file giaAig.c.

 {
     Aig_Man_t * pNew, * pTemp;
     pNew  = Gia_ManToAigSimple( p );
     pTemp = Aig_ManScl( pNew, fConst, fEquiv, 0, -1, -1, fVerbose, 0 );
     Gia_ManReprFromAigRepr( pNew, p );
     Aig_ManStop( pTemp );
     Aig_ManStop( pNew );
 }

int Gia_ManSolveSat ( Gia_Man_t * p )

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

Synopsis [Solves SAT problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 624 of file giaAig.c.

 {
 //    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
     Aig_Man_t * pNew;
     int RetValue;//, clk = Abc_Clock();
     pNew = Gia_ManToAig( p, 0 );
     RetValue = Fra_FraigSat( pNew, 10000000, 0, 0, 0, 0, 1, 1, 0, 0 );
     if ( RetValue == 0 )
     {
         Gia_Obj_t * pObj;
         int i, * pInit = (int *)pNew->pData;
         Gia_ManConst0(p)->fMark0 = 0;
         Gia_ManForEachPi( p, pObj, i )
             pObj->fMark0 = pInit[i];
         Gia_ManForEachAnd( p, pObj, i )
             pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
                            (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
         Gia_ManForEachPo( p, pObj, i )
             pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
         Gia_ManForEachPo( p, pObj, i )
             if ( pObj->fMark0 != 1 )
                 break;
         if ( i != Gia_ManPoNum(p) )
             Abc_Print( 1, "Counter-example verification has failed.  " );
 //        else
 //            Abc_Print( 1, "Counter-example verification succeeded.  " );
     }
 /*
     else if ( RetValue == 1 )
         Abc_Print( 1, "The SAT problem is unsatisfiable.  " );
     else if ( RetValue == -1 )
         Abc_Print( 1, "The SAT problem is undecided.  " );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 */
     Aig_ManStop( pNew );
     return RetValue;
 }

Aig_Man_t* Gia_ManToAig	(	Gia_Man_t *	p,
		int	fChoices
	)

Definition at line 277 of file giaAig.c.

 {
     Aig_Man_t * pNew;
     Aig_Obj_t ** ppNodes;
     Gia_Obj_t * pObj;
     int i;
     assert( !fChoices || (p->pNexts && p->pReprs) );
     // create the new manager
     pNew = Aig_ManStart( Gia_ManAndNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
 //    pNew->pSpec = Abc_UtilStrsav( p->pName );
     // duplicate representation of choice nodes
     if ( fChoices )
         pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     // create the PIs
     ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     ppNodes[0] = Aig_ManConst0(pNew);
     Gia_ManForEachCi( p, pObj, i )
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
     // transfer level
     if ( p->vLevels )
     Gia_ManForEachCi( p, pObj, i )
         Aig_ObjSetLevel( ppNodes[Gia_ObjId(p, pObj)], Gia_ObjLevel(p, pObj) );
     // add logic for the POs
     Gia_ManForEachCo( p, pObj, i )
     {
         Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
     }
     Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     ABC_FREE( ppNodes );
     return pNew;
 }

void Gia_ManToAig_rec	(	Aig_Man_t *	pNew,
		Aig_Obj_t **	ppNodes,
		Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file giaAig.c.

 {
     Gia_Obj_t * pNext;
     if ( ppNodes[Gia_ObjId(p, pObj)] )
         return;
     if ( Gia_ObjIsCi(pObj) )
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
     else
     {
         assert( Gia_ObjIsAnd(pObj) );
         Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
         Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
         ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
     }
     if ( pNew->pEquivs && (pNext = Gia_ObjNextObj(p, Gia_ObjId(p, pObj))) )
     {
         Aig_Obj_t * pObjNew, * pNextNew;
         Gia_ManToAig_rec( pNew, ppNodes, p, pNext );
         pObjNew  = ppNodes[Gia_ObjId(p, pObj)];
         pNextNew = ppNodes[Gia_ObjId(p, pNext)];
         if ( pNew->pEquivs )
             pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);        
     }
 }

Aig_Man_t* Gia_ManToAigSimple ( Gia_Man_t * p )

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 367 of file giaAig.c.

 {
     Aig_Man_t * pNew;
     Aig_Obj_t ** ppNodes;
     Gia_Obj_t * pObj;
     int i;
     ppNodes = ABC_FALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     // create the new manager
     pNew = Aig_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create the PIs
     Gia_ManForEachObj( p, pObj, i )
     {
         if ( Gia_ObjIsAnd(pObj) )
             ppNodes[i] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
         else if ( Gia_ObjIsCi(pObj) )
             ppNodes[i] = Aig_ObjCreateCi( pNew );
         else if ( Gia_ObjIsCo(pObj) )
             ppNodes[i] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
         else if ( Gia_ObjIsConst0(pObj) )
             ppNodes[i] = Aig_ManConst0(pNew);
         else
             assert( 0 );
         pObj->Value = Abc_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
         assert( i == 0 || Aig_ObjId(ppNodes[i]) == i );
     }
     Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     ABC_FREE( ppNodes );
     return pNew;
 }

Aig_Man_t* Gia_ManToAigSkip	(	Gia_Man_t *	p,
		int	nOutDelta
	)

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 324 of file giaAig.c.

 {
     Aig_Man_t * pNew;
     Aig_Obj_t ** ppNodes;
     Gia_Obj_t * pObj;
     int i;
     assert( p->pNexts == NULL && p->pReprs == NULL );
     assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 );
     // create the new manager
     pNew = Aig_ManStart( Gia_ManAndNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
 //    pNew->pSpec = Abc_UtilStrsav( p->pName );
     // create the PIs
     ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     ppNodes[0] = Aig_ManConst0(pNew);
     Gia_ManForEachCi( p, pObj, i )
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
     // add logic for the POs
     Gia_ManForEachCo( p, pObj, i )
     {
         Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
         if ( i % nOutDelta != 0 )
             continue;
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
     }
     Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     ABC_FREE( ppNodes );
     return pNew;
 }