[unsat-cores] Improving new unsat cores (#6356)

This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.

This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.

5 files changed, 82 insertions, 71 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 7a7809eef..8f59ec13b 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -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() && !isProofEnabled())
+  if (options::unsatCores())
   {
     ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
     ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
@@ -344,7 +344,6 @@ CRef Solver::reason(Var x) {
     }
     return vardata[x].d_reason;
   }
-
   // What's the literal we are trying to explain
   Lit l = mkLit(x, value(x) != l_True);
 
@@ -428,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() && !isProofEnabled())
+    if (options::unsatCores())
     {
       ClauseId id = ProofManager::getSatProof()->registerClause(real_reason,
                                                                 THEORY_LEMMA);
@@ -515,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() && !isProofEnabled())
+      if (options::unsatCores())
       {
         // Store the expression being converted to CNF until
         // the clause is actually created
@@ -534,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() && !isProofEnabled())
+            if (options::unsatCores())
             {
               ClauseKind ck =
                   ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -577,7 +576,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
         if (options::unsatCores() || isProofEnabled())
         {
-          if (options::unsatCores() && !isProofEnabled())
+          if (options::unsatCores())
           {
             ClauseKind ck =
                 ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -593,7 +592,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           if (ps.size() == falseLiteralsCount)
           {
-            if (options::unsatCores() && !isProofEnabled())
+            if (options::unsatCores())
             {
               ProofManager::getSatProof()->finalizeProof(cr);
             }
@@ -615,7 +614,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
                          << std::endl;
           if (ps.size() == 1)
           {
-            if (options::unsatCores() && !isProofEnabled())
+            if (options::unsatCores())
             {
               ClauseKind ck =
                   ProofManager::getCnfProof()->getCurrentAssertionKind()
@@ -641,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() && !isProofEnabled())
+            if (options::unsatCores())
             {
               if (ca[confl].size() == 1)
               {
@@ -669,7 +668,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
           }
           return ok;
         } else {
-          if (options::unsatCores() && !isProofEnabled())
+          if (options::unsatCores())
           {
             id = ClauseIdUndef;
           }
@@ -716,7 +715,7 @@ void Solver::detachClause(CRef cr, bool strict) {
       Debug("minisat") << "\n";
     }
     Assert(c.size() > 1);
-    if (options::unsatCores() && !isProofEnabled())
+    if (options::unsatCores())
     {
       ProofManager::getSatProof()->markDeleted(cr);
     }
@@ -998,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() && !isProofEnabled())
+  if (options::unsatCores())
   {
     ProofManager::getSatProof()->startResChain(confl);
     }
@@ -1062,7 +1061,7 @@ 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() && !isProofEnabled())
+              if (options::unsatCores())
               {
                 ProofManager::getSatProof()->resolveOutUnit(q);
               }
@@ -1084,7 +1083,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 
         if (pathC > 0 && confl != CRef_Undef)
         {
-          if (options::unsatCores() && !isProofEnabled())
+          if (options::unsatCores())
           {
             ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
           }
@@ -1124,7 +1123,7 @@ 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() && !isProofEnabled())
+                if (options::unsatCores())
                 {
                   ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
                 }
@@ -1420,7 +1419,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() && !isProofEnabled())
+        if (options::unsatCores())
         {
           ProofManager::getCnfProof()->popCurrentAssertion();
         }
@@ -1564,7 +1563,7 @@ 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() && !isProofEnabled() && locked(c))
+          if (options::unsatCores() && locked(c))
           {
             // store a resolution of the literal c propagated
             ProofManager::getSatProof()->storeUnitResolution(c[0]);
@@ -1671,7 +1670,7 @@ lbool Solver::search(int nof_conflicts)
 
       if (decisionLevel() == 0)
       {
-        if (options::unsatCores() && !isProofEnabled())
+        if (options::unsatCores())
         {
           ProofManager::getSatProof()->finalizeProof(confl);
         }
@@ -1698,7 +1697,7 @@ lbool Solver::search(int nof_conflicts)
       if (learnt_clause.size() == 1)
       {
         uncheckedEnqueue(learnt_clause[0]);
-        if (options::unsatCores() && !isProofEnabled())
+        if (options::unsatCores())
         {
           ProofManager::getSatProof()->endResChain(learnt_clause[0]);
         }
@@ -1716,7 +1715,7 @@ lbool Solver::search(int nof_conflicts)
         attachClause(cr);
         claBumpActivity(ca[cr]);
         uncheckedEnqueue(learnt_clause[0], cr);
-        if (options::unsatCores() && !isProofEnabled())
+        if (options::unsatCores())
         {
           ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
           ProofManager::getSatProof()->endResChain(id);
@@ -2059,9 +2058,8 @@ void Solver::relocAll(ClauseAllocator& to)
             {
               ca.reloc(ws[j].cref,
                        to,
-                       (options::unsatCores() && !isProofEnabled())
-                           ? ProofManager::getSatProof()
-                           : nullptr);
+                       options::unsatCores() ? ProofManager::getSatProof()
+                                             : nullptr);
             }
         }
 
@@ -2073,11 +2071,10 @@ void Solver::relocAll(ClauseAllocator& to)
         if (hasReasonClause(v)
             && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
         {
-          ca.reloc(vardata[v].d_reason,
-                   to,
-                   (options::unsatCores() && !isProofEnabled())
-                       ? ProofManager::getSatProof()
-                       : nullptr);
+          ca.reloc(
+              vardata[v].d_reason,
+              to,
+              options::unsatCores() ? ProofManager::getSatProof() : nullptr);
         }
     }
     // All learnt:
@@ -2086,9 +2083,7 @@ void Solver::relocAll(ClauseAllocator& to)
     {
       ca.reloc(clauses_removable[i],
                to,
-               (options::unsatCores() && !isProofEnabled())
-                   ? ProofManager::getSatProof()
-                   : nullptr);
+               options::unsatCores() ? ProofManager::getSatProof() : nullptr);
     }
     // All original:
     //
@@ -2096,11 +2091,9 @@ void Solver::relocAll(ClauseAllocator& to)
     {
       ca.reloc(clauses_persistent[i],
                to,
-               (options::unsatCores() && !isProofEnabled())
-                   ? ProofManager::getSatProof()
-                   : nullptr);
+               options::unsatCores() ? ProofManager::getSatProof() : nullptr);
     }
-    if (options::unsatCores() && !isProofEnabled())
+    if (options::unsatCores())
     {
       ProofManager::getSatProof()->finishUpdateCRef();
     }
@@ -2270,7 +2263,7 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      if (options::unsatCores() && !isProofEnabled())
+      if (options::unsatCores())
       {
         TNode cnf_assertion = lemmas_cnf_assertion[j];
 
@@ -2291,7 +2284,7 @@ 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() && !isProofEnabled() && lemma.size() == 1)
+        if (options::unsatCores() && lemma.size() == 1)
         {
           Node cnf_assertion = lemmas_cnf_assertion[j];
 
@@ -2311,7 +2304,7 @@ CRef Solver::updateLemmas() {
           } else {
             Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
             conflict = CRef_Lazy;
-            if (options::unsatCores() && !isProofEnabled())
+            if (options::unsatCores())
             {
               ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
             }
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index b7d80da76..a15864ad3 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -519,23 +519,33 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn)
   Node proven = trn.getProven();
   Trace("cnf") << "ProofCnfStream::convertPropagation: proven explanation"
                << proven << "\n";
-  Assert(trn.getGenerator());
-  Assert(trn.getGenerator()->getProofFor(proven)->isClosed());
-  Trace("cnf-steps") << proven << " by explainPropagation "
-                     << trn.identifyGenerator() << std::endl;
-  d_proof.addLazyStep(proven,
-                      trn.getGenerator(),
-                      PfRule::ASSUME,
-                      true,
-                      "ProofCnfStream::convertPropagation");
+  // If we are not producing proofs in the theory engine there is no need to
+  // keep track in d_proof of the clausification. We still need however to let
+  // the SAT proof manager know that this clause is an assumption.
+  bool proofLogging = trn.getGenerator() != nullptr;
+  if (proofLogging)
+  {
+    Assert(trn.getGenerator()->getProofFor(proven)->isClosed());
+    Trace("cnf-steps") << proven << " by explainPropagation "
+                       << trn.identifyGenerator() << std::endl;
+    d_proof.addLazyStep(proven,
+                        trn.getGenerator(),
+                        PfRule::ASSUME,
+                        true,
+                        "ProofCnfStream::convertPropagation");
+  }
   // since the propagation is added directly to the SAT solver via theoryProxy,
   // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here
   NodeManager* nm = NodeManager::currentNM();
-  Node clauseImpliesElim = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]);
-  Trace("cnf") << "ProofCnfStream::convertPropagation: adding "
-               << PfRule::IMPLIES_ELIM << " rule to conclude "
-               << clauseImpliesElim << "\n";
-  d_proof.addStep(clauseImpliesElim, PfRule::IMPLIES_ELIM, {proven}, {});
+  Node clauseImpliesElim;
+  if (proofLogging)
+  {
+    clauseImpliesElim = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]);
+    Trace("cnf") << "ProofCnfStream::convertPropagation: adding "
+                 << PfRule::IMPLIES_ELIM << " rule to conclude "
+                 << clauseImpliesElim << "\n";
+    d_proof.addStep(clauseImpliesElim, PfRule::IMPLIES_ELIM, {proven}, {});
+  }
   Node clauseExp;
   // need to eliminate AND
   if (proven[0].getKind() == kind::AND)
@@ -548,27 +558,33 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn)
       disjunctsRes.push_back(proven[0][i].notNode());
     }
     disjunctsRes.push_back(proven[1]);
-    Node clauseAndNeg = nm->mkNode(kind::OR, disjunctsAndNeg);
-    // add proof steps to convert into clause
-    d_proof.addStep(clauseAndNeg, PfRule::CNF_AND_NEG, {}, {proven[0]});
     clauseExp = nm->mkNode(kind::OR, disjunctsRes);
-    d_proof.addStep(clauseExp,
-                    PfRule::RESOLUTION,
-                    {clauseAndNeg, clauseImpliesElim},
-                    {nm->mkConst(true), proven[0]});
+    if (proofLogging)
+    {
+      // add proof steps to convert into clause
+      Node clauseAndNeg = nm->mkNode(kind::OR, disjunctsAndNeg);
+      d_proof.addStep(clauseAndNeg, PfRule::CNF_AND_NEG, {}, {proven[0]});
+      d_proof.addStep(clauseExp,
+                      PfRule::RESOLUTION,
+                      {clauseAndNeg, clauseImpliesElim},
+                      {nm->mkConst(true), proven[0]});
+    }
   }
   else
   {
-    clauseExp = clauseImpliesElim;
+    clauseExp = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]);
   }
   normalizeAndRegister(clauseExp);
   // consume steps
-  const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
-  for (const std::pair<Node, ProofStep>& step : steps)
+  if (proofLogging)
   {
-    d_proof.addStep(step.first, step.second);
+    const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
+    for (const std::pair<Node, ProofStep>& step : steps)
+    {
+      d_proof.addStep(step.first, step.second);
+    }
+    d_psb.clear();
   }
-  d_psb.clear();
 }
 
 void ProofCnfStream::ensureLiteral(TNode n)
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index d696db580..6299471dd 100644
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -79,12 +79,11 @@ class ProofCnfStream : public ProofGenerator
                         ProofGenerator* pg);
 
   /**
-   * Clausifies the given propagation lemma *without* registering the
-   * resoluting clause in the SAT solver, as this is handled internally by the
-   * SAT solver. The clausification steps and the generator within the trust
-   * node are saved in d_proof. */
+   * Clausifies the given propagation lemma *without* registering the resoluting
+   * clause in the SAT solver, as this is handled internally by the SAT
+   * solver. The clausification steps and the generator within the trust node
+   * are saved in d_proof if we are producing proofs in the theory engine. */
   void convertPropagation(theory::TrustNode ttn);
-
   /**
    * Ensure that the given node will have a designated SAT literal that is
    * definitionally equal to it.  The result of this function is that the Node
@@ -152,6 +151,7 @@ class ProofCnfStream : public ProofGenerator
    * above normalizations on all added clauses.
    */
   void normalizeAndRegister(TNode clauseNode);
+
   /** Reference to the underlying cnf stream. */
   CnfStream& d_cnfStream;
   /** The proof manager of underlying SAT solver associated with this stream. */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 4af943537..2eaa3a812 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -246,7 +246,8 @@ 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);
+  Assert(!isProofEnabled() || trn.getGenerator() != nullptr
+         || options::unsatCores() || options::unsatCoresNew());
   assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
 }
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index bf386fc0e..6ff2af527 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -96,8 +96,9 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
 
   theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
   Node theoryExplanation = tte.getNode();
-  if (cvc5::options::produceProofs())
+  if (options::produceProofs())
   {
+    Assert(options::unsatCoresNew() || tte.getGenerator());
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }
   else if (options::unsatCores())