Workaround for incremental unsat cores (#1962)

This commit implements a workaround for computing unsat cores while
doing incremental solving to address #1349. Currently, our resolution
proofs do not handle clauses with a lower-than-assertion-level correctly
because the resolution proofs for them get removed when popping the
context but the SAT solver keeps using them. The workaround changes the
behavior of the SAT solver to add clauses always at the current level if
incremental solving and unsat cores are enabled. This makes sure that
all learned clauses are removed when we pop below the level that they
were learned at. This may degrade performance because the SAT solver has
to relearn clauses.

1 files changed, 91 insertions, 52 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index aa59f18e1..3c8023395 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -26,7 +26,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <unordered_set>
 
 #include "base/output.h"
+#include "options/main_options.h"
 #include "options/prop_options.h"
+#include "options/smt_options.h"
 #include "proof/clause_id.h"
 #include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
@@ -40,6 +42,22 @@ using namespace CVC4::prop;
 namespace CVC4 {
 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::unsatCores() && options::incrementalSolving();
+}
+}  // namespace
+
 //=================================================================================================
 // Options:
 
@@ -242,43 +260,60 @@ CRef Solver::reason(Var x) {
 
     // Compute the assertion level for this clause
     int explLevel = 0;
-    int i, j;
-    Lit prev = lit_Undef;
-    for (i = 0, j = 0; i < explanation.size(); ++ i) {
-      // This clause is valid theory propagation, so its level is the level of the top literal
-      explLevel = std::max(explLevel, intro_level(var(explanation[i])));
-
-      Assert(value(explanation[i]) != l_Undef);
-      Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i])));
-
-      // Always keep the first literal
-      if (i == 0) {
+    if (assertionLevelOnly())
+    {
+      explLevel = assertionLevel;
+    }
+    else
+    {
+      int i, j;
+      Lit prev = lit_Undef;
+      for (i = 0, j = 0; i < explanation.size(); ++i)
+      {
+        // This clause is valid theory propagation, so its level is the level of
+        // the top literal
+        explLevel = std::max(explLevel, intro_level(var(explanation[i])));
+
+        Assert(value(explanation[i]) != l_Undef);
+        Assert(i == 0
+               || trail_index(var(explanation[0]))
+                      > trail_index(var(explanation[i])));
+
+        // Always keep the first literal
+        if (i == 0)
+        {
+          prev = explanation[j++] = explanation[i];
+          continue;
+        }
+        // Ignore duplicate literals
+        if (explanation[i] == prev)
+        {
+          continue;
+        }
+        // Ignore zero level literals
+        if (level(var(explanation[i])) == 0
+            && user_level(var(explanation[i]) == 0))
+        {
+          continue;
+        }
+        // Keep this literal
         prev = explanation[j++] = explanation[i];
-        continue;
-      }
-      // Ignore duplicate literals
-      if (explanation[i] == prev) {
-        continue;
-      }
-      // Ignore zero level literals
-      if (level(var(explanation[i])) == 0 && user_level(var(explanation[i]) == 0)) {
-        continue;
       }
-      // Keep this literal
-      prev = explanation[j++] = explanation[i];
-    }
-    explanation.shrink(i - j);
+      explanation.shrink(i - j);
 
-    Debug("pf::sat") << "Solver::reason: explanation = " ;
-    for (int i = 0; i < explanation.size(); ++i) {
-      Debug("pf::sat") << explanation[i] << " ";
-    }
-    Debug("pf::sat") << std::endl;
+      Debug("pf::sat") << "Solver::reason: explanation = ";
+      for (int i = 0; i < explanation.size(); ++i)
+      {
+        Debug("pf::sat") << explanation[i] << " ";
+      }
+      Debug("pf::sat") << std::endl;
 
-    // We need an explanation clause so we add a fake literal
-    if (j == 1) {
-      // Add not TRUE to the clause
-      explanation.push(mkLit(varTrue, true));
+      // We need an explanation clause so we add a fake literal
+      if (j == 1)
+      {
+        // Add not TRUE to the clause
+        explanation.push(mkLit(varTrue, true));
+      }
     }
 
     // Construct the reason
@@ -306,13 +341,15 @@ 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 ? 0 : assertionLevel;
+    int clauseLevel = (removable && !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 = std::max(clauseLevel, intro_level(var(ps[i])));
+      clauseLevel = assertionLevelOnly()
+                        ? assertionLevel
+                        : std::max(clauseLevel, intro_level(var(ps[i])));
       // Tautologies are ignored
       if (ps[i] == ~p) {
         id = ClauseIdUndef;
@@ -1221,22 +1258,23 @@ lbool Solver::search(int nof_conflicts)
                 PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); )
 
             } else {
-                CRef cr = ca.alloc(max_level, learnt_clause, true);
-                clauses_removable.push(cr);
-                attachClause(cr);
-                claBumpActivity(ca[cr]);
-                uncheckedEnqueue(learnt_clause[0], cr);
-                PROOF(
-                      ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
-                      PSTATS(
-                      std::unordered_set<int> cl_levels;
-                      for (int i = 0; i < learnt_clause.size(); ++i) {
-                        cl_levels.insert(level(var(learnt_clause[i])));
-                      }
-                      ProofManager::getSatProof()->storeClauseGlue(id, cl_levels.size());
-                            )
-                      ProofManager::getSatProof()->endResChain(id);
-                      );
+              CRef cr =
+                  ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
+                           learnt_clause,
+                           true);
+              clauses_removable.push(cr);
+              attachClause(cr);
+              claBumpActivity(ca[cr]);
+              uncheckedEnqueue(learnt_clause[0], cr);
+              PROOF(ClauseId id =
+                        ProofManager::getSatProof()->registerClause(cr, LEARNT);
+                    PSTATS(std::unordered_set<int> cl_levels;
+                           for (int i = 0; i < learnt_clause.size(); ++i) {
+                             cl_levels.insert(level(var(learnt_clause[i])));
+                           } ProofManager::getSatProof()
+                               ->storeClauseGlue(id, cl_levels.size());)
+                        ProofManager::getSatProof()
+                            ->endResChain(id););
             }
 
             varDecayActivity();
@@ -1748,7 +1786,8 @@ 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) {
+      if (removable && !assertionLevelOnly())
+      {
         clauseLevel = 0;
         for (int i = 0; i < lemma.size(); ++ i) {
           clauseLevel = std::max(clauseLevel, intro_level(var(lemma[i])));