From 0398ced8243806439b814f21ca7d6e584cea13a1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 22 Jun 2015 23:04:53 -0700 Subject: Version abc90714 committer: Baruch Sterin --- src/aig/gia/gia.h | 46 +++++++++++++++++++++++++++++++++++++--------- src/aig/gia/giaAig.c | 41 +++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaAig.h | 1 + src/aig/gia/giaCSat.c | 2 ++ src/aig/gia/giaDfs.c | 27 +++++++++++++++++++++++++++ src/aig/gia/giaEquiv.c | 33 +++++++++++++++++++++++++++++++++ src/aig/gia/giaMan.c | 5 +++-- src/aig/gia/giaUtil.c | 38 ++++++++++++++++++++++++++++++++++++-- src/aig/gia/module.make | 1 + 9 files changed, 181 insertions(+), 13 deletions(-) (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 571a6ef8..af92acc9 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -82,7 +82,7 @@ struct Gia_Obj_t_ unsigned Value; // application-specific value }; -// Value is currently use to store several types of information +// Value is currently used to store several types of information // - pointer to the next node in the hash table during structural hashing // - pointer to the node copy during duplication // - traversal ID of the node during traversal @@ -135,6 +135,7 @@ struct Gia_Man_t_ Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc unsigned char* pSwitching; // switching activity for each object Gia_Plc_t * pPlacement; // placement of the objects + int * pTravIds; // separate traversal ID representation }; @@ -309,13 +310,22 @@ static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); } static inline void Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj)); } -static inline void Gia_ManResetTravId( Gia_Man_t * p ) { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1; } -static inline void Gia_ManIncrementTravId( Gia_Man_t * p ) { p->nTravIds++; } -static inline void Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId ) { pObj->Value = TravId; } -static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds; } -static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds - 1; } -static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds); } -static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds - 1); } +static inline void Gia_ManResetTravId( Gia_Man_t * p ) { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1; } +static inline void Gia_ManIncrementTravId( Gia_Man_t * p ) { p->nTravIds++; } +static inline void Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId ) { pObj->Value = TravId; } +static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds; } +static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds - 1; } +static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds); } +static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds - 1); } + +static inline void Gia_ManResetTravIdArray( Gia_Man_t * p ) { ABC_FREE( p->pTravIds ); p->pTravIds = ABC_CALLOC( int, Gia_ManObjNum(p) ); p->nTravIds = 1; } +static inline void Gia_ManIncrementTravIdArray( Gia_Man_t * p ) { p->nTravIds++; } +static inline void Gia_ObjSetTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds; } +static inline void Gia_ObjSetTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; } +static inline int Gia_ObjIsTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); } +static inline int Gia_ObjIsTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); } +static inline void Gia_ObjSetTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { p->pTravIds[Id] = p->nTravIds; } +static inline int Gia_ObjIsTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { return (p->pTravIds[Id] == p->nTravIds); } // AIG construction extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); @@ -402,6 +412,7 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); } static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; } static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { p->pReprs[Id].iRepr = Num; } +static inline void Gia_ObjUnsetRepr( Gia_Man_t * p, int Id ) { p->pReprs[Id].iRepr = GIA_VOID; } static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; } static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; } @@ -423,12 +434,15 @@ static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { r static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; } static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; } +static inline int Gia_ObjIsUsed( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) != GIA_VOID && Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; } static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; } static inline int Gia_ObjIsClass( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0; } static inline int Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k); } +static inline int Gia_ClassIsPair( Gia_Man_t * p, int i ) { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) == 0; } +static inline void Gia_ClassUndoPair( Gia_Man_t * p, int i ) { assert( Gia_ClassIsPair(p,i) ); Gia_ObjSetRepr(p, Gia_ObjNext(p, i), GIA_VOID); Gia_ObjSetNext(p, i, 0); } #define Gia_ManForEachConst( p, i ) \ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else @@ -466,7 +480,9 @@ static inline int * Gia_ObjGateFanins( Gia_Man_t * p, int Id ) { re #define Gia_ManForEachObjReverse( p, pObj, i ) \ for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) #define Gia_ManForEachAnd( p, pObj, i ) \ - for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else + for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else +#define Gia_ManForEachAndReverse( p, pObj, i ) \ + for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) if ( !Gia_ObjIsAnd(pObj) ) {} else #define Gia_ManForEachCi( p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ ) #define Gia_ManForEachCo( p, pObj, i ) \ @@ -498,6 +514,8 @@ extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCsat.c ============================================================*/ extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); +/*=== giaCTas.c ============================================================*/ +extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCof.c =============================================================*/ extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ); extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar ); @@ -508,6 +526,7 @@ extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int n extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes ); extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes ); extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes ); +extern Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p ); /*=== giaDup.c ============================================================*/ extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ); @@ -620,6 +639,7 @@ extern void Gia_ManCheckMark1( Gia_Man_t * p ); extern void Gia_ManCleanValue( Gia_Man_t * p ); extern void Gia_ManFillValue( Gia_Man_t * p ); extern void Gia_ManSetPhase( Gia_Man_t * p ); +extern void Gia_ManCleanPhase( Gia_Man_t * p ); extern int Gia_ManLevelNum( Gia_Man_t * p ); extern void Gia_ManSetRefs( Gia_Man_t * p ); extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p ); @@ -636,6 +656,14 @@ extern void Gia_ManPrintCounterExample( Gia_Cex_t * p ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); extern int Gia_ManHasChoices( Gia_Man_t * p ); extern int Gia_ManHasDandling( Gia_Man_t * p ); +/*=== giaUtil.c ===========================================================*/ +typedef struct Tas_Man_t_ Tas_Man_t; +extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit ); +extern void Tas_ManStop( Tas_Man_t * p ); +extern Vec_Int_t * Tas_ReadModel( Tas_Man_t * p ); +extern void Tas_ManSatPrintStats( Tas_Man_t * p ); +extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); + #ifdef __cplusplus } diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 4b3692e4..07e74e34 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -260,6 +260,47 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta ) +{ + 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 = Gia_UtilStrsav( p->pName ); +// pNew->pSpec = Gia_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_ObjCreatePi( 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_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) ); + } + Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + ABC_FREE( ppNodes ); + return pNew; +} + /**Function************************************************************* Synopsis [Duplicates AIG in the DFS order.] diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h index 507e5143..0e29bf06 100644 --- a/src/aig/gia/giaAig.h +++ b/src/aig/gia/giaAig.h @@ -50,6 +50,7 @@ extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ); extern Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p ); extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ); extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ); +extern Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta ); extern void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia ); #ifdef __cplusplus diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index e005dfc2..644ccda5 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -1020,6 +1020,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt // solve for each output Gia_ManForEachCo( pAig, pRoot, i ) { +// printf( "\n" ); + Vec_IntClear( vCex ); if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) ) { diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c index 8a3aef92..bcc1748f 100644 --- a/src/aig/gia/giaDfs.c +++ b/src/aig/gia/giaDfs.c @@ -264,6 +264,33 @@ int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes ) return Counter; } +/**Function************************************************************* + + Synopsis [Levelizes the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + Vec_Vec_t * vLevels; + int nLevels, Level, i; + nLevels = Gia_ManLevelNum( p ); + vLevels = Vec_VecStart( nLevels + 1 ); + Gia_ManForEachAnd( p, pObj, i ) + { + Level = Gia_ObjLevel( p, pObj ); + assert( Level <= nLevels ); + Vec_VecPush( vLevels, Level, pObj ); + } + return vLevels; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 041be0f5..8458268c 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -277,6 +277,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) assert( Gia_ManEquivCheckLits( p, nLits ) ); if ( fVerbose ) { + int Ent; +/* printf( "Const0 = " ); Gia_ManForEachConst( p, i ) printf( "%d ", i ); @@ -284,6 +286,18 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) Counter = 0; Gia_ManForEachClass( p, i ) Gia_ManEquivPrintOne( p, i, ++Counter ); +*/ + Gia_ManLevelNum( p ); + Gia_ManForEachClass( p, i ) + if ( i % 100 == 0 ) + { +// printf( "%d ", Gia_ManEquivCountOne(p, i) ); + Gia_ClassForEachObj( p, i, Ent ) + { + printf( "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) ); + } + printf( "\n" ); + } } } @@ -370,6 +384,15 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" ); return NULL; } + // check if there are any equivalences defined + Gia_ManForEachObj( p, pObj, i ) + if ( Gia_ObjReprObj(p, i) != NULL ) + break; + if ( i == Gia_ManObjNum(p) ) + { + printf( "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" ); + return NULL; + } /* if ( !Gia_ManCheckTopoOrder( p ) ) { @@ -720,6 +743,16 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose ) printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" ); return NULL; } + // check if there are any equivalences defined + Gia_ManForEachObj( p, pObj, i ) + if ( Gia_ObjReprObj(p, i) != NULL ) + break; + if ( i == Gia_ManObjNum(p) ) + { + printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" ); + return NULL; + } + /* if ( !Gia_ManCheckTopoOrder( p ) ) { diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 7f4da081..37afde13 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -70,6 +70,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFree( p->vFlopClasses ); Vec_IntFree( p->vCis ); Vec_IntFree( p->vCos ); + ABC_FREE( p->pTravIds ); ABC_FREE( p->pPlacement ); ABC_FREE( p->pSwitching ); ABC_FREE( p->pCexSeq ); @@ -203,10 +204,10 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ) void Gia_ManPrintStatsShort( Gia_Man_t * p ) { printf( "i/o =%7d/%7d ", Gia_ManPiNum(p), Gia_ManPoNum(p) ); -// printf( "ff =%7d ", Gia_ManRegNum(p) ); + printf( "ff =%7d ", Gia_ManRegNum(p) ); printf( "and =%8d ", Gia_ManAndNum(p) ); printf( "lev =%5d ", Gia_ManLevelNum(p) ); - printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) ); +// printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) ); printf( "\n" ); } diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 54bc98dd..938c6363 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -315,6 +315,25 @@ void Gia_ManSetPhase( Gia_Man_t * p ) } } +/**Function************************************************************* + + Synopsis [Sets phases of the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCleanPhase( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i; + Gia_ManForEachObj( p, pObj, i ) + pObj->fPhase = 0; +} + /**Function************************************************************* Synopsis [Assigns levels.] @@ -883,17 +902,32 @@ int Gia_ManHasChoices( Gia_Man_t * p ) 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 ); + 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 diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 6f70f7d3..79bfa2fb 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -4,6 +4,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaCof.c \ src/aig/gia/giaCSatOld.c \ src/aig/gia/giaCSat.c \ + src/aig/gia/giaCTas.c \ src/aig/gia/giaDfs.c \ src/aig/gia/giaDup.c \ src/aig/gia/giaEmbed.c \ -- cgit v1.2.3