diff options
Diffstat (limited to 'src/prop/minisat/core/Solver.cc')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 36f31eba9..a82ab5e06 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -145,12 +145,14 @@ class ScopedBool //================================================================================================= // Constructor/Destructor: -Solver::Solver(cvc5::prop::TheoryProxy* proxy, +Solver::Solver(Env& env, + cvc5::prop::TheoryProxy* proxy, cvc5::context::Context* context, cvc5::context::UserContext* userContext, ProofNodeManager* pnm, bool enableIncremental) - : d_proxy(proxy), + : EnvObj(env), + d_proxy(proxy), d_context(context), assertionLevel(0), d_pfManager(nullptr), @@ -454,7 +456,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) // If a literal is false at 0 level (both sat and user level) we also // ignore it, unless we are tracking the SAT solver's reasoning if (value(ps[i]) == l_False) { - if (!options::unsatCores() && !needProof() && level(var(ps[i])) == 0 + if (!options().smt.unsatCores && !needProof() && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { continue; @@ -489,7 +491,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { - if (options::unsatCores() || needProof()) + if (options().smt.unsatCores || needProof()) { // Take care of false units here; otherwise, we need to // construct the clause below to give to the proof manager @@ -520,7 +522,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) clauses_persistent.push(cr); attachClause(cr); - if (options::unsatCores() || needProof()) + if (options().smt.unsatCores || needProof()) { if (ps.size() == falseLiteralsCount) { @@ -2043,7 +2045,7 @@ CRef Solver::updateLemmas() { // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { - Assert(!options::unsatCores() && !needProof()); + Assert(!options().smt.unsatCores && !needProof()); conflict = CRef_Lazy; backtrackLevel = 0; Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl; @@ -2189,8 +2191,8 @@ bool Solver::isProofEnabled() const { return d_pfManager != nullptr; } bool Solver::needProof() const { return isProofEnabled() - && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS - && options::unsatCoresMode() != options::UnsatCoresMode::PP_ONLY; + && options().smt.unsatCoresMode != options::UnsatCoresMode::ASSUMPTIONS + && options().smt.unsatCoresMode != options::UnsatCoresMode::PP_ONLY; } } // namespace Minisat |