diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-04 15:40:53 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-04 15:40:53 -0700 |
| commit | b11344b454f2df60de7b303b1b102ec62a96d01d (patch) | |
| tree | 990c16f3f5feb6f145b17b5852749f3997105b05 /src/sat/bsat | |
| parent | a207f6c07117fc577076f924984a0cbad1c0b0b0 (diff) | |
| download | abc-b11344b454f2df60de7b303b1b102ec62a96d01d.tar.gz abc-b11344b454f2df60de7b303b1b102ec62a96d01d.tar.bz2 abc-b11344b454f2df60de7b303b1b102ec62a96d01d.zip | |
Experiments with SAT-based collapsing.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 7 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 053b0587..24c60dac 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1861,7 +1861,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit int fConfl = sat_solver_propagate(s); if (fConfl){ sat_solver_analyze_final(s, fConfl, 0); - assert(s->conf_final.size > 0); + //assert(s->conf_final.size > 0); sat_solver_canceluntil(s, 0); return l_False; } } diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 8e171031..89391d2d 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -234,6 +234,13 @@ static void sat_solver_prepare_enum(sat_solver* s, int * pVars, int nVars ) for ( v = 0; v < nVars; v++ ) veci_push(&s->vDeciVars,pVars[v]); } +static void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars ) +{ + int i; + assert( veci_size(&s->vDeciVars) == 0 ); + for ( i = 0; i < nVars; i++ ) + s->polarity[pVars[i]] = 0; +} static int sat_solver_final(sat_solver* s, int ** ppArray) { |