From 64c72f3a49e917ced3c279fbe87911b10e04213f Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 3 Jan 2022 10:29:52 -0800 Subject: [PATCH] Remove static options from sat solver. (#7790) This PR removes options::foo() from minisat. --- src/prop/minisat/core/Solver.cc | 77 ++++++++++++++++----------------- src/prop/minisat/core/Solver.h | 11 +++++ 2 files changed, 49 insertions(+), 39 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index a82ab5e06..9715fc9a7 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -42,48 +42,33 @@ namespace cvc5 { namespace Minisat { namespace { -/* - * Returns true if the solver should add all clauses at the current assertion - * level. - * - * FIXME: This is a workaround. Currently, our resolution proofs do not - * handle clauses with a lower-than-assertion-level correctly because the - * resolution proofs get removed when popping the context but the SAT solver - * keeps using them. - */ -bool assertionLevelOnly() -{ - return (options::produceProofs() || options::unsatCores()) - && options::incrementalSolving(); -} - //================================================================================================= // Helper functions for decision tree tracing // Writes to Trace macro for decision tree tracing static inline void dtviewDecisionHelper(size_t level, const Node& node, - const char* decisiontype) + const char* decisiontype, + bool incremental) { - Trace("dtview") << std::string(level - (options::incrementalSolving() ? 1 : 0), '*') - << " " << node << " :" << decisiontype << "-DECISION:" << std::endl; + Trace("dtview") << std::string(level - (incremental ? 1 : 0), '*') << " " + << node << " :" << decisiontype << "-DECISION:" << std::endl; } // Writes to Trace macro for propagation tracing -static inline void dtviewPropagationHeaderHelper(size_t level) +static inline void dtviewPropagationHeaderHelper(size_t level, bool incremental) { - Trace("dtview::prop") << std::string(level + 1 - (options::incrementalSolving() ? 1 : 0), - '*') + Trace("dtview::prop") << std::string(level + 1 - (incremental ? 1 : 0), '*') << " /Propagations/" << std::endl; } // Writes to Trace macro for propagation tracing static inline void dtviewBoolPropagationHelper(size_t level, Lit& l, - cvc5::prop::TheoryProxy* proxy) + cvc5::prop::TheoryProxy* proxy, + bool incremental) { - Trace("dtview::prop") << std::string( - level + 1 - (options::incrementalSolving() ? 1 : 0), ' ') + Trace("dtview::prop") << std::string(level + 1 - (incremental ? 1 : 0), ' ') << ":BOOL-PROP: " << proxy->getNode(MinisatSatSolver::toSatLiteral(l)) << std::endl; @@ -92,10 +77,11 @@ static inline void dtviewBoolPropagationHelper(size_t level, // Writes to Trace macro for conflict tracing static inline void dtviewPropConflictHelper(size_t level, Clause& confl, - cvc5::prop::TheoryProxy* proxy) + cvc5::prop::TheoryProxy* proxy, + bool incremental) { Trace("dtview::conflict") - << std::string(level + 1 - (options::incrementalSolving() ? 1 : 0), ' ') + << std::string(level + 1 - (incremental ? 1 : 0), ' ') << ":PROP-CONFLICT: (or"; for (int i = 0; i < confl.size(); i++) { @@ -156,6 +142,9 @@ Solver::Solver(Env& env, d_context(context), assertionLevel(0), d_pfManager(nullptr), + d_assertionLevelOnly( + (options().smt.produceProofs || options().smt.unsatCores) + && options().base.incrementalSolving), d_enable_incremental(enableIncremental), minisat_busy(false) // Parameters (user settable): @@ -354,7 +343,7 @@ CRef Solver::reason(Var x) { // Compute the assertion level for this clause int explLevel = 0; - if (assertionLevelOnly()) + if (d_assertionLevelOnly) { explLevel = assertionLevel; } @@ -429,13 +418,13 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) Lit p; int i, j; // Which user-level to assert this clause at - int clauseLevel = (removable && !assertionLevelOnly()) ? 0 : assertionLevel; + int clauseLevel = (removable && !d_assertionLevelOnly) ? 0 : assertionLevel; // Check the clause for tautologies and similar int falseLiteralsCount = 0; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { // Update the level - clauseLevel = assertionLevelOnly() + clauseLevel = d_assertionLevelOnly ? assertionLevel : std::max(clauseLevel, intro_level(var(ps[i]))); // Tautologies are ignored @@ -740,12 +729,14 @@ Lit Solver::pickBranchLit() dtviewDecisionHelper( d_context->getLevel(), d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)), - "THEORY"); + "THEORY", + options().base.incrementalSolving); } if (Trace.isOn("dtview::prop")) { - dtviewPropagationHeaderHelper(d_context->getLevel()); + dtviewPropagationHeaderHelper(d_context->getLevel(), + options().base.incrementalSolving); } return nextLit; @@ -783,12 +774,14 @@ Lit Solver::pickBranchLit() dtviewDecisionHelper( d_context->getLevel(), d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)), - "DE"); + "DE", + options().base.incrementalSolving); } if (Trace.isOn("dtview::prop")) { - dtviewPropagationHeaderHelper(d_context->getLevel()); + dtviewPropagationHeaderHelper(d_context->getLevel(), + options().base.incrementalSolving); } return nextLit; @@ -845,12 +838,14 @@ Lit Solver::pickBranchLit() dtviewDecisionHelper( d_context->getLevel(), d_proxy->getNode(MinisatSatSolver::toSatLiteral(decisionLit)), - "DE"); + "DE", + options().base.incrementalSolving); } if (Trace.isOn("dtview::prop")) { - dtviewPropagationHeaderHelper(d_context->getLevel()); + dtviewPropagationHeaderHelper(d_context->getLevel(), + options().base.incrementalSolving); } return decisionLit; @@ -1237,7 +1232,10 @@ CRef Solver::propagate(TheoryCheckType type) { if (confl != CRef_Undef) { - dtviewPropConflictHelper(decisionLevel(), ca[confl], d_proxy); + dtviewPropConflictHelper(decisionLevel(), + ca[confl], + d_proxy, + options().base.incrementalSolving); } } // Even though in conflict, we still need to discharge the lemmas @@ -1335,7 +1333,8 @@ CRef Solver::propagateBool() // if propagation tracing enabled, print boolean propagation if (Trace.isOn("dtview::prop")) { - dtviewBoolPropagationHelper(decisionLevel(), p, d_proxy); + dtviewBoolPropagationHelper( + decisionLevel(), p, d_proxy, options().base.incrementalSolving); } for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){ @@ -1561,7 +1560,7 @@ lbool Solver::search(int nof_conflicts) } else { - CRef cr = ca.alloc(assertionLevelOnly() ? assertionLevel : max_level, + CRef cr = ca.alloc(d_assertionLevelOnly ? assertionLevel : max_level, learnt_clause, true); clauses_removable.push(cr); @@ -2087,7 +2086,7 @@ CRef Solver::updateLemmas() { if (lemma.size() > 1) { // If the lemmas is removable, we can compute its level by the level int clauseLevel = assertionLevel; - if (removable && !assertionLevelOnly()) + if (removable && !d_assertionLevelOnly) { clauseLevel = 0; for (int k = 0; k < lemma.size(); ++k) diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index c5dc807ac..23dc7baae 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -94,6 +94,17 @@ class Solver : protected EnvObj int getAssertionLevel() const { return assertionLevel; } protected: + /* + * Returns true if the solver should add all clauses at the current assertion + * level. + * + * FIXME: This is a workaround. Currently, our resolution proofs do not + * handle clauses with a lower-than-assertion-level correctly because the + * resolution proofs get removed when popping the context but the SAT solver + * keeps using them. + */ + const bool d_assertionLevelOnly; + /** Do we allow incremental solving */ bool d_enable_incremental; -- 2.30.2