diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-12-31 20:21:46 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-12-31 20:21:46 +0700 |
| commit | 01924ca118cad9bc8bf84de0525e54f5c4a832ec (patch) | |
| tree | 27bca3f3218ce7def6998a9db88bec6d57dc4222 /src/opt/sbd/sbdWin.c | |
| parent | 54b4692d4bb2a6c5e59b5f54aaff95e2c4966e77 (diff) | |
| download | abc-01924ca118cad9bc8bf84de0525e54f5c4a832ec.tar.gz abc-01924ca118cad9bc8bf84de0525e54f5c4a832ec.tar.bz2 abc-01924ca118cad9bc8bf84de0525e54f5c4a832ec.zip | |
Updates to delay optimization project.
Diffstat (limited to 'src/opt/sbd/sbdWin.c')
| -rw-r--r-- | src/opt/sbd/sbdWin.c | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c index d5b7dd9d..b62332d1 100644 --- a/src/opt/sbd/sbdWin.c +++ b/src/opt/sbd/sbdWin.c @@ -54,7 +54,6 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf ) { Gia_Obj_t * pObj; - int nAddVars = 64; int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue; int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo); int PivotVar = Vec_IntEntry(vObj2Var, Pivot); @@ -67,7 +66,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi pSat = sat_solver_new(); else sat_solver_restart( pSat ); - sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + nAddVars ); + sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + SBD_FVAR_MAX ); // create constant 0 clause sat_solver_addclause( pSat, &iLit, &iLit + 1 ); // add clauses for all nodes @@ -139,7 +138,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi sat_solver_delete( pSat ); return NULL; } - assert( sat_solver_nvars(pSat) == nVars + nAddVars ); + assert( sat_solver_nvars(pSat) == nVars + SBD_FVAR_MAX ); } else if ( fQbf ) { |