Remove static options from sat solver. (#7790)

This PR removes options::foo() from minisat.

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index a82ab5e06d92097f76dd12a8a466136c31d7a4a9..9715fc9a7fc431ef89d0c8a04aefdf7de85fad4a 100644 (file)
--- 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<Lit>& 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 c5dc807ac4f25286020bcc76de8c73370ded0fbb..23dc7baae7b63404d56b120dcba2898ca70a8b2f 100644 (file)
--- 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;