diff options
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 8 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 2 |
2 files changed, 9 insertions, 1 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index c4847be4..5c9294b0 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -457,6 +457,12 @@ static inline void sat_solver_canceluntil(sat_solver* s, int level) { reasons = s->reasons; bound = (veci_begin(&s->trail_lim))[level]; + //////////////////////////////////////// + // added to cancel all assignments +// if ( level == -1 ) +// bound = 0; + //////////////////////////////////////// + for (c = s->qtail-1; c >= bound; c--) { int x = lit_var(trail[c]); values [x] = l_Undef; @@ -881,7 +887,7 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l return l_Undef; } - if (sat_solver_dlevel(s) == 0) + if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify) // Simplify the set of problem clauses: sat_solver_simplify(s); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 8f71370f..986e48d5 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -170,6 +170,8 @@ struct sat_solver_t Sat_MmStep_t * pMem; + int fSkipSimplify; // set to one to skip simplification of the clause database + // clause store void * pStore; |