From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 2 Jun 2022 18:49:41 +0000 (-0300)
Subject: [proofs] [sat] [cores] Fix unsat cores based on the SAT proof (#8850)
X-Git-Tag: cvc5-1.0.1~76
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=65a77c3d7715af4fe44b81c0e3f9c17c6f154886;p=cvc5.git

[proofs] [sat] [cores] Fix unsat cores based on the SAT proof (#8850)

The justifications for the theory lemmas (i.e., THEORY_LEMMA steps) sometimes was not being properly connected with the actual clause inserted into the SAT solver, leading to open proofs. The issue was triggered by a regression being added in ##8819, so we don't need to add one here.
---

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index aca156316..939e78f34 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -598,7 +598,8 @@ void ProofCnfStream::convertPropagation(TrustNode trn)
   d_currPropagationProccessed = normalizeAndRegister(clauseExp);
   // consume steps if clausification being recorded. If we are not logging it,
   // we need to add the clause as a closed step to the proof so that the SAT
-  // proof does not have non-input formulas as assumptions.
+  // proof does not have non-input formulas as assumptions. That clause is the
+  // result of normalizeAndRegister, stored in d_currPropagationProccessed
   if (proofLogging)
   {
     const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
@@ -610,7 +611,10 @@ void ProofCnfStream::convertPropagation(TrustNode trn)
   }
   else
   {
-    d_proof.addStep(clauseExp, PfRule::THEORY_LEMMA, {}, {clauseExp});
+    d_proof.addStep(d_currPropagationProccessed,
+                    PfRule::THEORY_LEMMA,
+                    {},
+                    {d_currPropagationProccessed});
   }
 }
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 1e7267064..91f1aaf76 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -74,7 +74,9 @@ PropEngine::PropEngine(Env& env, TheoryEngine* te)
       d_satSolver(nullptr),
       d_cnfStream(nullptr),
       d_pfCnfStream(nullptr),
-      d_theoryLemmaPg(d_env.getProofNodeManager(), d_env.getUserContext()),
+      d_theoryLemmaPg(d_env.getProofNodeManager(),
+                      d_env.getUserContext(),
+                      "PropEngine::ThLemmaPg"),
       d_ppm(nullptr),
       d_interrupted(false),
       d_assumptions(d_env.getUserContext())
@@ -240,7 +242,8 @@ void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable)
   if (isProofEnabled() && !d_env.isTheoryProofProducing()
       && !trn.getGenerator())
   {
-    d_theoryLemmaPg.addStep(node, PfRule::THEORY_LEMMA, {}, {node});
+    Node actualNode = negated ? node.notNode() : node;
+    d_theoryLemmaPg.addStep(actualNode, PfRule::THEORY_LEMMA, {}, {actualNode});
     trn = TrustNode::mkReplaceGenTrustNode(trn, &d_theoryLemmaPg);
   }
   assertInternal(node, negated, removable, false, trn.getGenerator());
@@ -337,7 +340,7 @@ bool PropEngine::isDecision(Node lit) const {
 
 std::vector<Node> PropEngine::getPropDecisions() const
 {
-  std::vector<Node> decisions; 
+  std::vector<Node> decisions;
   std::vector<SatLiteral> miniDecisions = d_satSolver->getDecisions();
   for (SatLiteral d : miniDecisions)
   {