(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.

diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index 2d114acd6dd74af5d362ec9c46f82685967f47b7..93f291e9a71b67f6e6d0ec63f8698079d9e68af5 100644 (file)
--- 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 c53b7ff2381f1b61ed8fbc193e076899f55b8db3..f2ce6c74b7fb6d36ed4bba6f9b867f498b8eab77 100644 (file)
--- 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 66c36ed95b30ef8ec33bd0a3366a6916e5e1357e..323f8c6a20c4dcf705f816ce5c98af912a142971 100644 (file)
--- 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";