diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2018-01-23 19:45:17 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2018-01-23 19:45:17 -0800 |
| commit | 066e8d1b173d11aeb837ffda56a8ba1bb7ddb214 (patch) | |
| tree | 8ec71d116a19e18d9b9b120772e7a577312167d1 /src/proof/cec | |
| parent | 67e820a5eb49127594f0a552e5e86b69897686c9 (diff) | |
| download | abc-066e8d1b173d11aeb837ffda56a8ba1bb7ddb214.tar.gz abc-066e8d1b173d11aeb837ffda56a8ba1bb7ddb214.tar.bz2 abc-066e8d1b173d11aeb837ffda56a8ba1bb7ddb214.zip | |
Experiments with SAT-based simulation.
Diffstat (limited to 'src/proof/cec')
| -rw-r--r-- | src/proof/cec/cecSat.c | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c index 0f4bf2bb..1d2ebd1d 100644 --- a/src/proof/cec/cecSat.c +++ b/src/proof/cec/cecSat.c @@ -301,12 +301,19 @@ void Cec2_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) } void Cec2_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat ) { + int iVar; assert( !Gia_IsComplement(pObj) ); assert( !Gia_ObjIsConst0(pObj) ); if ( Cec2_ObjSatId(p, pObj) >= 0 ) return; assert( Cec2_ObjSatId(p, pObj) == -1 ); - Cec2_ObjSetSatId( p, pObj, satoko_add_variable(pSat, 0) ); + iVar = satoko_add_variable(pSat, 0); + if ( p->vVar2Obj ) + { + assert( Vec_IntSize(p->vVar2Obj) == iVar ); + Vec_IntPush( p->vVar2Obj, Gia_ObjId(p, pObj) ); + } + Cec2_ObjSetSatId( p, pObj, iVar ); if ( Gia_ObjIsAnd(pObj) ) Vec_PtrPush( vFrontier, pObj ); } @@ -322,7 +329,15 @@ int Gia_ObjGetCnfVar( Gia_Man_t * pGia, int iObj, Vec_Ptr_t * vFrontier, Vec_Ptr return Cec2_ObjSatId(pGia,pObj); assert( iObj > 0 ); if ( Gia_ObjIsCi(pObj) ) - return Cec2_ObjSetSatId( pGia, pObj, satoko_add_variable(pSat, 0) ); + { + int iVar = satoko_add_variable(pSat, 0); + if ( pGia->vVar2Obj ) + { + assert( Vec_IntSize(pGia->vVar2Obj) == iVar ); + Vec_IntPush( pGia->vVar2Obj, iObj ); + } + return Cec2_ObjSetSatId( pGia, pObj, iVar ); + } assert( Gia_ObjIsAnd(pObj) ); // start the frontier Vec_PtrClear( vFrontier ); |