diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-10-29 12:24:07 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-10-29 12:24:07 -0700 |
commit | e21052dfdd1656ca6fee96a4470d1e062a1c8d78 (patch) | |
tree | f2078b0f891144c8c86c8c988d338dfdb89c5493 /src/aig | |
parent | 50e17ae0f444aadee3621ef5f0c68eb386755cf6 (diff) | |
download | abc-e21052dfdd1656ca6fee96a4470d1e062a1c8d78.tar.gz abc-e21052dfdd1656ca6fee96a4470d1e062a1c8d78.tar.bz2 abc-e21052dfdd1656ca6fee96a4470d1e062a1c8d78.zip |
Improvements to quantification.
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/gia.h | 3 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 77 |
2 files changed, 80 insertions, 0 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 591dd419..9acbbe48 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -514,6 +514,7 @@ static inline void Gia_ObjFlipFaninC0( Gia_Obj_t * pObj ) { static inline int Gia_ObjFaninNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( Gia_ObjIsMux(p, pObj) ) return 3; if ( Gia_ObjIsAnd(pObj) ) return 2; if ( Gia_ObjIsCo(pObj) ) return 1; return 0; } static inline int Gia_ObjWhatFanin( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) { if ( Gia_ObjFanin0(pObj) == pFanin ) return 0; if ( Gia_ObjFanin1(pObj) == pFanin ) return 1; if ( Gia_ObjFanin2(p, pObj) == pFanin ) return 2; assert(0); return -1; } +static inline int Gia_ManPoIsConst( Gia_Man_t * p, int iPoIndex ) { return Gia_ObjFaninId0p(p, Gia_ManPo(p, iPoIndex)) == 0; } static inline int Gia_ManPoIsConst0( Gia_Man_t * p, int iPoIndex ) { return Gia_ManIsConst0Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); } static inline int Gia_ManPoIsConst1( Gia_Man_t * p, int iPoIndex ) { return Gia_ManIsConst1Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); } @@ -1237,6 +1238,8 @@ extern Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar ); extern Gia_Man_t * Gia_ManDupUniv( Gia_Man_t * p, int iVar ); extern Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj ); +extern Gia_Man_t * Gia_ManDupConeSupp( Gia_Man_t * p, int iLit, Vec_Int_t * vCiIds ); +extern int Gia_ManDupConeBack( Gia_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * vCiIds ); extern Gia_Man_t * Gia_ManDupDfsNode( Gia_Man_t * p, Gia_Obj_t * pObj ); extern Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits ); extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut, int OutValue ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 96ddebd8..1d4f7a22 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1878,6 +1878,83 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot ) /**Function************************************************************* + Synopsis [Duplicates logic cone of the literal and inserts it back.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupConeSupp_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjs ) +{ + int iLit0, iLit1, iObj = Gia_ObjId( p, pObj ); + int iLit = Gia_ObjCopyArray( p, iObj ); + if ( iLit >= 0 ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupConeSupp_rec( pNew, p, Gia_ObjFanin0(pObj), vObjs ); + Gia_ManDupConeSupp_rec( pNew, p, Gia_ObjFanin1(pObj), vObjs ); + iLit0 = Gia_ObjCopyArray( p, Gia_ObjFaninId0(pObj, iObj) ); + iLit1 = Gia_ObjCopyArray( p, Gia_ObjFaninId1(pObj, iObj) ); + iLit0 = Abc_LitNotCond( iLit0, Gia_ObjFaninC0(pObj) ); + iLit1 = Abc_LitNotCond( iLit1, Gia_ObjFaninC1(pObj) ); + iLit = Gia_ManAppendAnd( pNew, iLit0, iLit1 ); + Gia_ObjSetCopyArray( p, iObj, iLit ); + Vec_IntPush( vObjs, iObj ); +} +Gia_Man_t * Gia_ManDupConeSupp( Gia_Man_t * p, int iLit, Vec_Int_t * vCiIds ) +{ + Gia_Man_t * pNew; int i, iLit0; + Gia_Obj_t * pObj, * pRoot = Gia_ManObj( p, Abc_Lit2Var(iLit) ); + Vec_Int_t * vObjs = Vec_IntAlloc( 1000 ); + assert( Gia_ObjIsAnd(pRoot) ); + if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) ) + Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManForEachCiVec( vCiIds, p, pObj, i ) + Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) ); + Gia_ManDupConeSupp_rec( pNew, p, pRoot, vObjs ); + iLit0 = Gia_ObjCopyArray( p, Abc_Lit2Var(iLit) ); + iLit0 = Abc_LitNotCond( iLit0, Abc_LitIsCompl(iLit) ); + Gia_ManAppendCo( pNew, iLit0 ); + Gia_ManForEachCiVec( vCiIds, p, pObj, i ) + Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), -1 ); + Gia_ManForEachObjVec( vObjs, p, pObj, i ) + Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), -1 ); + Vec_IntFree( vObjs ); + //assert( Vec_IntCountLarger(&p->vCopies, -1) == 0 ); + return pNew; +} +void Gia_ManDupConeBack_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupConeBack_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManDupConeBack_rec( pNew, p, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +// pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} +int Gia_ManDupConeBack( Gia_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * vCiIds ) +{ + Gia_Obj_t * pObj, * pRoot; int i; + assert( Gia_ManCiNum(pNew) == Vec_IntSize(vCiIds) ); + Gia_ManFillValue(pNew); + Gia_ManConst0(pNew)->Value = 0; + Gia_ManForEachCi( pNew, pObj, i ) + pObj->Value = Gia_Obj2Lit( p, Gia_ManCi(p, Vec_IntEntry(vCiIds, i)) ); + pRoot = Gia_ManCo(pNew, 0); + Gia_ManDupConeBack_rec( p, pNew, Gia_ObjFanin0(pRoot) ); + return Gia_ObjFanin0Copy(pRoot); +} + + +/**Function************************************************************* + Synopsis [Duplicates AIG in the DFS order while putting CIs first.] Description [] |