diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-04 16:20:31 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-04 16:20:31 -0800 |
| commit | 22fd7dca452be1c996436c5e5faa673ceff5ac96 (patch) | |
| tree | fa86614526163bbbd4f5baf06db1ab084e248c29 /src/sat/bmc/bmcICheck.c | |
| parent | a0529ec5c80482253d451b90c00b6c22d664dfb2 (diff) | |
| download | abc-22fd7dca452be1c996436c5e5faa673ceff5ac96.tar.gz abc-22fd7dca452be1c996436c5e5faa673ceff5ac96.tar.bz2 abc-22fd7dca452be1c996436c5e5faa673ceff5ac96.zip | |
Specialized inductive check.
Diffstat (limited to 'src/sat/bmc/bmcICheck.c')
| -rw-r--r-- | src/sat/bmc/bmcICheck.c | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c index 4376c336..17408e78 100644 --- a/src/sat/bmc/bmcICheck.c +++ b/src/sat/bmc/bmcICheck.c @@ -94,6 +94,7 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC Vec_Int_t * vLits; Gia_Obj_t * pObj, * pObj0, * pObj1; int i, k, iVar0, iVar1, iVarOut; + int VarShift = 0; // start the SAT solver pSat = sat_solver_new(); @@ -108,6 +109,8 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC // load the last timeframe Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) ); + VarShift += Gia_ManRegNum(p) + Gia_ManCoNum(p); + // add XOR clauses Gia_ManForEachPo( p, pObj, i ) { @@ -141,6 +144,7 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pMiter, pObj)] ); // lift CNF again Cnf_DataLiftGia( pCnf, pMiter, pCnf->nVars ); + VarShift += pCnf->nVars; // stitch the clauses Gia_ManForEachRi( pMiter, pObj, i ) { @@ -173,6 +177,7 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC assert( 0 ); } // sat_solver_compress( pSat ); + Cnf_DataLiftGia( pCnf, pMiter, -VarShift ); Vec_IntFree( vLits ); return pSat; } |