(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)

Previously, strings on proof-new used a ProofStepBuffer for deriving the final conclusion of lemmas in proof equality engine (assertLemma). This was recently changed to use the more standard ProofGenerator interface of assertLemma. However, there was a bug in this method: the steps from this proof need to be deep copied into the proof we are generating or otherwise the explanation of these literals are not connected in the CDProof. This updates the proof equality engine so that it instructs the proof generator to do a deep copy in this case. Notice this is very rarely more than a single step.

3 files changed, 18 insertions, 6 deletions

diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index 2d114acd6..93f291e9a 100644
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -43,7 +43,10 @@ std::shared_ptr<ProofNode> ProofGenerator::getProofFor(Node f)
   return nullptr;
 }
 
-bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy)
+bool ProofGenerator::addProofTo(Node f,
+                                CDProof* pf,
+                                CDPOverwrite opolicy,
+                                bool doCopy)
 {
   Trace("pfgen") << "ProofGenerator::addProofTo: " << f << "..." << std::endl;
   Assert(pf != nullptr);
@@ -52,8 +55,7 @@ bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy)
   if (apf != nullptr)
   {
     Trace("pfgen") << "...got proof " << *apf.get() << std::endl;
-    // Add the proof, without deep copying.
-    if (pf->addProof(apf, opolicy, false))
+    if (pf->addProof(apf, opolicy, doCopy))
     {
       Trace("pfgen") << "...success!" << std::endl;
       return true;
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index c53b7ff23..f2ce6c74b 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -82,11 +82,13 @@ class ProofGenerator
    * @param f The fact to get the proof for.
    * @param pf The CDProof object to add the proof to.
    * @param opolicy The overwrite policy for adding to pf.
+   * @param doCopy Whether to do a deep copy of the proof steps into pf.
    * @return True if this call was sucessful.
    */
   virtual bool addProofTo(Node f,
                           CDProof* pf,
-                          CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY);
+                          CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY,
+                          bool doCopy = false);
   /**
    * Can we give the proof for formula f? This is used for debugging. This
    * returns false if the generator cannot provide a proof of formula f.
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 66c36ed95..323f8c6a2 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -376,8 +376,16 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
     {
       curr = &tmpProof;
     }
-    // Register the proof step.
-    if (!pg->addProofTo(conc, curr))
+    // Register the proof. Notice we do a deep copy here because the CDProof
+    // curr should take ownership of the proof steps that pg provided for conc.
+    // In other words, this sets up the "skeleton" of proof that is the base
+    // of the proof we are constructing. The call to assertLemmaInternal below
+    // will expand the leaves of this proof. If we used a shallow copy, then
+    // the connection to these leaves would be lost since they would not be
+    // owned by curr. Notice this is very rarely more than a single step, but
+    // may be multiple steps if e.g. a theory inference corresponds to a
+    // sequence of more than one PfRule steps.
+    if (!pg->addProofTo(conc, curr, CDPOverwrite::ASSUME_ONLY, true))
     {
       // a step went wrong, e.g. during checking
       Assert(false) << "pfee::assertConflict: register proof step";