Reconciling proofs and unsat cores (#6405)

This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:

the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.

3 files changed, 50 insertions, 34 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 981e51e31..ea30c12e9 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -228,7 +228,7 @@ Solver::Solver(cvc5::prop::TheoryProxy* proxy,
     d_pfManager.reset(
         new SatProofManager(this, proxy->getCnfStream(), userContext, pnm));
   }
-  else if (options::unsatCores())
+  else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::currentPM()->initSatProof(this);
   }
@@ -241,7 +241,7 @@ Solver::Solver(cvc5::prop::TheoryProxy* proxy,
   uncheckedEnqueue(mkLit(varTrue, false));
   uncheckedEnqueue(mkLit(varFalse, true));
   // FIXME: these should be axioms I believe
-  if (options::unsatCores())
+  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
     ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
@@ -427,7 +427,7 @@ CRef Solver::reason(Var x) {
     // came from (ie. the theory/sharing)
     Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)"
                      << std::endl;
-    if (options::unsatCores())
+    if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
     {
       ClauseId id = ProofManager::getSatProof()->registerClause(real_reason,
                                                                 THEORY_LEMMA);
@@ -514,7 +514,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
       lemmas.push();
       ps.copyTo(lemmas.last());
       lemmas_removable.push(removable);
-      if (options::unsatCores())
+      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
       {
         // Store the expression being converted to CNF until
         // the clause is actually created
@@ -533,7 +533,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           // construct the clause below to give to the proof manager
           // as the final conflict.
           if(falseLiteralsCount == 1) {
-            if (options::unsatCores())
+            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
             {
               ClauseKind ck =
                   ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -576,7 +576,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
         if (options::unsatCores() || isProofEnabled())
         {
-          if (options::unsatCores())
+          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
           {
             ClauseKind ck =
                 ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -592,7 +592,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           if (ps.size() == falseLiteralsCount)
           {
-            if (options::unsatCores())
+            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
             {
               ProofManager::getSatProof()->finalizeProof(cr);
             }
@@ -614,7 +614,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
                          << std::endl;
           if (ps.size() == 1)
           {
-            if (options::unsatCores())
+            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
             {
               ClauseKind ck =
                   ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -640,7 +640,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           CRef confl = propagate(CHECK_WITHOUT_THEORY);
           if(! (ok = (confl == CRef_Undef)) ) {
-            if (options::unsatCores())
+            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
             {
               if (ca[confl].size() == 1)
               {
@@ -668,7 +668,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           return ok;
         } else {
-          if (options::unsatCores())
+          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
           {
             id = ClauseIdUndef;
           }
@@ -715,7 +715,7 @@ void Solver::detachClause(CRef cr, bool strict) {
       Debug("minisat") << "\n";
     }
     Assert(c.size() > 1);
-    if (options::unsatCores())
+    if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
     {
       ProofManager::getSatProof()->markDeleted(cr);
     }
@@ -997,7 +997,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 
   int max_resolution_level = 0;  // Maximal level of the resolved clauses
 
-  if (options::unsatCores())
+  if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::getSatProof()->startResChain(confl);
     }
@@ -1061,7 +1061,8 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
             // FIXME: can we do it lazily if we actually need the proof?
             if (level(var(q)) == 0)
             {
-              if (options::unsatCores())
+              if (options::unsatCoresMode()
+                  == options::UnsatCoresMode::OLD_PROOF)
               {
                 ProofManager::getSatProof()->resolveOutUnit(q);
               }
@@ -1083,7 +1084,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 
         if (pathC > 0 && confl != CRef_Undef)
         {
-          if (options::unsatCores())
+          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
           {
             ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
           }
@@ -1123,7 +1124,8 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
                 // Literal is not redundant
                 out_learnt[j++] = out_learnt[i];
               } else {
-                if (options::unsatCores())
+                if (options::unsatCoresMode()
+                    == options::UnsatCoresMode::OLD_PROOF)
                 {
                   ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
                 }
@@ -1419,7 +1421,7 @@ void Solver::propagateTheory() {
         addClause(explanation, true, id);
         // explainPropagation() pushes the explanation on the assertion
         // stack in CnfProof, so we need to pop it here.
-        if (options::unsatCores())
+        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
         {
           ProofManager::getCnfProof()->popCurrentAssertion();
         }
@@ -1563,7 +1565,8 @@ void Solver::removeSatisfied(vec<CRef>& cs)
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
         if (satisfied(c)) {
-          if (options::unsatCores() && locked(c))
+          if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+              && locked(c))
           {
             // store a resolution of the literal c propagated
             ProofManager::getSatProof()->storeUnitResolution(c[0]);
@@ -1670,7 +1673,7 @@ lbool Solver::search(int nof_conflicts)
 
       if (decisionLevel() == 0)
       {
-        if (options::unsatCores())
+        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
         {
           ProofManager::getSatProof()->finalizeProof(confl);
         }
@@ -1697,7 +1700,7 @@ lbool Solver::search(int nof_conflicts)
       if (learnt_clause.size() == 1)
       {
         uncheckedEnqueue(learnt_clause[0]);
-        if (options::unsatCores())
+        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
         {
           ProofManager::getSatProof()->endResChain(learnt_clause[0]);
         }
@@ -1715,7 +1718,7 @@ lbool Solver::search(int nof_conflicts)
         attachClause(cr);
         claBumpActivity(ca[cr]);
         uncheckedEnqueue(learnt_clause[0], cr);
-        if (options::unsatCores())
+        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
         {
           ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
           ProofManager::getSatProof()->endResChain(id);
@@ -2058,8 +2061,10 @@ void Solver::relocAll(ClauseAllocator& to)
             {
               ca.reloc(ws[j].cref,
                        to,
-                       options::unsatCores() ? ProofManager::getSatProof()
-                                             : nullptr);
+                       options::unsatCoresMode()
+                               == options::UnsatCoresMode::OLD_PROOF
+                           ? ProofManager::getSatProof()
+                           : nullptr);
             }
         }
 
@@ -2074,7 +2079,9 @@ void Solver::relocAll(ClauseAllocator& to)
           ca.reloc(
               vardata[v].d_reason,
               to,
-              options::unsatCores() ? ProofManager::getSatProof() : nullptr);
+              options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+                  ? ProofManager::getSatProof()
+                  : nullptr);
         }
     }
     // All learnt:
@@ -2083,7 +2090,9 @@ void Solver::relocAll(ClauseAllocator& to)
     {
       ca.reloc(clauses_removable[i],
                to,
-               options::unsatCores() ? ProofManager::getSatProof() : nullptr);
+               options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+                   ? ProofManager::getSatProof()
+                   : nullptr);
     }
     // All original:
     //
@@ -2091,9 +2100,11 @@ void Solver::relocAll(ClauseAllocator& to)
     {
       ca.reloc(clauses_persistent[i],
                to,
-               options::unsatCores() ? ProofManager::getSatProof() : nullptr);
+               options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+                   ? ProofManager::getSatProof()
+                   : nullptr);
     }
-    if (options::unsatCores())
+    if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
     {
       ProofManager::getSatProof()->finishUpdateCRef();
     }
@@ -2263,7 +2274,7 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      if (options::unsatCores())
+      if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
       {
         TNode cnf_assertion = lemmas_cnf_assertion[j];
 
@@ -2284,7 +2295,8 @@ CRef Solver::updateLemmas() {
     // If the lemma is propagating enqueue its literal (or set the conflict)
     if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
       if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
-        if (options::unsatCores() && lemma.size() == 1)
+        if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+            && lemma.size() == 1)
         {
           Node cnf_assertion = lemmas_cnf_assertion[j];
 
@@ -2304,7 +2316,7 @@ CRef Solver::updateLemmas() {
           } else {
             Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
             conflict = CRef_Lazy;
-            if (options::unsatCores())
+            if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
             {
               ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
             }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2eaa3a812..646da84b2 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -122,7 +122,7 @@ PropEngine::PropEngine(TheoryEngine* te,
     d_ppm.reset(
         new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get()));
   }
-  else if (options::unsatCores())
+  else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
   }
@@ -246,8 +246,11 @@ void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn,
   Node node = trn.getNode();
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
   bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
-  Assert(!isProofEnabled() || trn.getGenerator() != nullptr
-         || options::unsatCores() || options::unsatCoresNew());
+  Assert(
+      !isProofEnabled() || trn.getGenerator() != nullptr
+      || options::unsatCores()
+      || (options::unsatCores()
+          && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF));
   assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
 }
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 51ce2ced2..98a76ae1a 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -98,10 +98,11 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   Node theoryExplanation = tte.getNode();
   if (options::produceProofs())
   {
-    Assert(options::unsatCoresNew() || tte.getGenerator());
+    Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
+           || tte.getGenerator());
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }
-  else if (options::unsatCores())
+  else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
   {
     ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
   }