diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-04 20:28:17 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-04 20:28:17 -0800 |
| commit | b781c1c1d5f3f3dc5f3c880d6ff07d6cfa39bae1 (patch) | |
| tree | 1b7824bd2dfaf363c0393069da74b6937a974712 /src/sat/bmc | |
| parent | 2076d38ea3c552c47967a6c2e08376560baf6cb5 (diff) | |
| parent | 22fd7dca452be1c996436c5e5faa673ceff5ac96 (diff) | |
| download | abc-b781c1c1d5f3f3dc5f3c880d6ff07d6cfa39bae1.tar.gz abc-b781c1c1d5f3f3dc5f3c880d6ff07d6cfa39bae1.tar.bz2 abc-b781c1c1d5f3f3dc5f3c880d6ff07d6cfa39bae1.zip | |
Merging heads.
Diffstat (limited to 'src/sat/bmc')
| -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; } |