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/gia/giaDup.c | |
parent | 50e17ae0f444aadee3621ef5f0c68eb386755cf6 (diff) | |
download | abc-e21052dfdd1656ca6fee96a4470d1e062a1c8d78.tar.gz abc-e21052dfdd1656ca6fee96a4470d1e062a1c8d78.tar.bz2 abc-e21052dfdd1656ca6fee96a4470d1e062a1c8d78.zip |
Improvements to quantification.
Diffstat (limited to 'src/aig/gia/giaDup.c')
-rw-r--r-- | src/aig/gia/giaDup.c | 77 |
1 files changed, 77 insertions, 0 deletions
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 [] |