From a0052e22b43ff9d0125ca8e71f96589226e44e42 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 15 Nov 2012 16:00:29 -0800 Subject: Added switch 'cexcut -m' to generate bad states for all frames after G. --- src/aig/gia/gia.h | 3 +++ src/aig/gia/giaDup.c | 6 +++--- 2 files changed, 6 insertions(+), 3 deletions(-) (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index d261e433..9d361fe8 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -316,6 +316,9 @@ static inline void Gia_ObjSetValue( Gia_Obj_t * pObj, int i ) { static inline int Gia_ObjPhase( Gia_Obj_t * pObj ) { return pObj->fPhase; } static inline int Gia_ObjPhaseReal( Gia_Obj_t * pObj ) { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj); } +static inline int Gia_Obj2Lit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit(Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj)); } +static inline Gia_Obj_t * Gia_Lit2Obj( Gia_Man_t * p, int iLit ) { return Gia_NotCond(Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit)); } + static inline int Gia_ManIdToCioId( Gia_Man_t * p, int Id ) { return Gia_ObjCioId( Gia_ManObj(p, Id) ); } static inline int Gia_ManCiIdToId( Gia_Man_t * p, int CiId ) { return Gia_ObjId( p, Gia_ManCi(p, CiId) ); } static inline int Gia_ManCoIdToId( Gia_Man_t * p, int CoId ) { return Gia_ObjId( p, Gia_ManCo(p, CoId) ); } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index eddbd320..3b8980af 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1233,7 +1233,7 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 ) // there is no flops in p2 assert( Gia_ManRegNum(p2) == 0 ); // there is only one PO in p2 - assert( Gia_ManPoNum(p2) == 1 ); +// assert( Gia_ManPoNum(p2) == 1 ); // input count of p2 is equal to flop count of p1 assert( Gia_ManPiNum(p2) == Gia_ManRegNum(p1) ); @@ -1255,8 +1255,8 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 ) Gia_ManForEachAnd( p2, pObj, i ) pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); // add property output - pObj = Gia_ManPo( p2, 0 ); - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachPo( p2, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); // add flop inputs Gia_ManForEachRi( p1, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); -- cgit v1.2.3