diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2021-04-27 14:46:05 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2021-04-27 14:46:05 -0700 |
| commit | 5f8a8a596a009046896acd8af6397acecc1e36a9 (patch) | |
| tree | 111b1022a28a4ef86a12ed2252ada6e6874e4eda /src/sat/glucose2/SimpSolver.h | |
| parent | de71e5f61038748b59bcbb2bf6f0c8666b45190a (diff) | |
| download | abc-5f8a8a596a009046896acd8af6397acecc1e36a9.tar.gz abc-5f8a8a596a009046896acd8af6397acecc1e36a9.tar.bz2 abc-5f8a8a596a009046896acd8af6397acecc1e36a9.zip | |
Upgrade to the circuit-based solver.
Diffstat (limited to 'src/sat/glucose2/SimpSolver.h')
| -rw-r--r-- | src/sat/glucose2/SimpSolver.h | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/sat/glucose2/SimpSolver.h b/src/sat/glucose2/SimpSolver.h index 00dbfa4c..36d625e9 100644 --- a/src/sat/glucose2/SimpSolver.h +++ b/src/sat/glucose2/SimpSolver.h @@ -61,12 +61,25 @@ class SimpSolver : public Solver { // bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); + int solveLimited(int * lit0, int nlits, bool do_simp = false, bool turn_off_simp = false); bool solve ( bool do_simp = true, bool turn_off_simp = false); bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification. + void prelocate(int base_var_num){ + Solver::prelocate(base_var_num); + frozen .prelocate( base_var_num ); + eliminated.prelocate( base_var_num ); + + if (use_simplification){ + n_occ .prelocate( base_var_num << 1 ); + occurs .prelocate( base_var_num ); + touched .prelocate( base_var_num ); + elim_heap .prelocate( base_var_num ); + } + } // Memory managment: // virtual void reset(); @@ -199,6 +212,14 @@ inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, boo inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); } +inline int SimpSolver::solveLimited(int * lit0, int nlits, bool do_simp, bool turn_off_simp){ + assumptions.clear(); + for(int i = 0; i < nlits; i ++) + assumptions.push(toLit(lit0[i])); + lbool res = solve_(do_simp, turn_off_simp); + return res == l_True ? 1 : (res == l_False ? -1 : 0); +} + inline void SimpSolver::addVar(Var v) { while (v >= nVars()) newVar(); } //================================================================================================= |