(proof-new) Improve interfaces to proof generators (#4803)

This includes configurable naming and a caching policy for term conversion proof generator.

Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.

1 files changed, 43 insertions, 23 deletions

diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index df0258af7..dc984438c 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -20,8 +20,9 @@ namespace CVC4 {
 
 LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
                          ProofGenerator* dpg,
-                         context::Context* c)
-    : CDProof(pnm, c), d_gens(c ? c : &d_context), d_defaultGen(dpg)
+                         context::Context* c,
+                         std::string name)
+    : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg)
 {
 }
 
@@ -56,36 +57,47 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
     if (it == visited.end())
     {
       visited.insert(cur);
-      if (cur->getRule() == PfRule::ASSUME)
+      Node cfact = cur->getResult();
+      if (getProof(cfact).get() != cur)
+      {
+        // We don't own this proof, skip it. This is to ensure that this method
+        // is idempotent, since it may be the case that a previous call to
+        // getProofFor connected a proof from a proof generator as a child of
+        // a ProofNode in the range of the map in CDProof. Thus, this ensures
+        // we don't touch such proofs.
+        Trace("lazy-cdproof") << "...skip unowned proof" << std::endl;
+      }
+      else if (cur->getRule() == PfRule::ASSUME)
       {
-        Node afact = cur->getResult();
         bool isSym = false;
-        ProofGenerator* pg = getGeneratorFor(afact, isSym);
+        ProofGenerator* pg = getGeneratorFor(cfact, isSym);
         if (pg != nullptr)
         {
-          Trace("lazy-cdproof") << "LazyCDProof: Call generator for assumption "
-                                << afact << std::endl;
-          Node afactGen = isSym ? CDProof::getSymmFact(afact) : afact;
-          Assert(!afactGen.isNull());
-          // use the addProofTo interface
-          if (!pg->addProofTo(afactGen, this))
+          Trace("lazy-cdproof")
+              << "LazyCDProof: Call generator " << pg->identify()
+              << " for assumption " << cfact << std::endl;
+          Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact;
+          Assert(!cfactGen.isNull());
+          // Do not use the addProofTo interface, instead use the update node
+          // interface, since this ensures that we don't take ownership for
+          // the current proof. Instead, it is only linked, and ignored on
+          // future calls to getProofFor due to the check above.
+          std::shared_ptr<ProofNode> pgc = pg->getProofFor(cfactGen);
+          if (isSym)
           {
-            Trace("lazy-cdproof") << "LazyCDProof: Failed added fact for "
-                                  << afactGen << std::endl;
-            Assert(false) << "Proof generator " << pg->identify()
-                          << " could not add proof for fact " << afactGen
-                          << std::endl;
+            d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {});
           }
           else
           {
-            Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
-                                  << afactGen << std::endl;
+            d_manager->updateNode(cur, pgc.get());
           }
+          Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
+                                << cfactGen << std::endl;
         }
         else
         {
-          Trace("lazy-cdproof")
-              << "LazyCDProof: No generator for " << afact << std::endl;
+          Trace("lazy-cdproof") << "LazyCDProof: " << identify()
+                                << " : No generator for " << cfact << std::endl;
         }
         // Notice that we do not traverse the proofs that have been generated
         // lazily by the proof generators here.  In other words, we assume that
@@ -104,11 +116,14 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
   } while (!visit.empty());
   // we have now updated the ASSUME leafs of opf, return it
   Trace("lazy-cdproof") << "...finished" << std::endl;
+  Assert(opf->getResult() == fact);
   return opf;
 }
 
 void LazyCDProof::addLazyStep(Node expected,
                               ProofGenerator* pg,
+                              bool isClosed,
+                              const char* ctx,
                               bool forceOverwrite,
                               PfRule idNull)
 {
@@ -117,7 +132,8 @@ void LazyCDProof::addLazyStep(Node expected,
     // null generator, should have given a proof rule
     if (idNull == PfRule::ASSUME)
     {
-      Assert(false);
+      Unreachable() << "LazyCDProof::addLazyStep: " << identify()
+                    << ": failed to provide proof generator for " << expected;
       return;
     }
     Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
@@ -138,6 +154,12 @@ void LazyCDProof::addLazyStep(Node expected,
   }
   // just store now
   d_gens.insert(expected, pg);
+  // debug checking
+  if (isClosed)
+  {
+    Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl;
+    pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx);
+  }
 }
 
 ProofGenerator* LazyCDProof::getGeneratorFor(Node fact,
@@ -191,6 +213,4 @@ bool LazyCDProof::hasGenerator(Node fact) const
   return it != d_gens.end();
 }
 
-std::string LazyCDProof::identify() const { return "LazyCDProof"; }
-
 }  // namespace CVC4