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

3 files changed, 26 insertions, 9 deletions

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 3f44e592e..5da190a3d 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -422,13 +422,19 @@ Node RemoveTermFormulas::getAxiomFor(Node n)
   return Node::null();
 }
 
-void RemoveTermFormulas::setProofChecker(ProofChecker* pc)
+void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm)
 {
   if (d_tpg == nullptr)
   {
-    d_pnm.reset(new ProofNodeManager(pc));
-    d_tpg.reset(new TConvProofGenerator(d_pnm.get()));
-    d_lp.reset(new LazyCDProof(d_pnm.get()));
+    d_pnm = pnm;
+    d_tpg.reset(
+        new TConvProofGenerator(d_pnm,
+                                nullptr,
+                                TConvPolicy::FIXPOINT,
+                                TConvCachePolicy::NEVER,
+                                "RemoveTermFormulas::TConvProofGenerator"));
+    d_lp.reset(new LazyCDProof(
+        d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
   }
 }
 
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index d4c22b78b..78d5899d0 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -106,10 +106,10 @@ class RemoveTermFormulas {
   void garbageCollect();
 
   /**
-   * Set proof checker, which signals this class to enable proofs using the
+   * Set proof node manager, which signals this class to enable proofs using the
    * given checker.
    */
-  void setProofChecker(ProofChecker* pc);
+  void setProofNodeManager(ProofNodeManager* pnm);
 
   /**
    * Get axiom for term n. This returns the axiom that this class uses to
@@ -166,7 +166,7 @@ class RemoveTermFormulas {
   static bool hasNestedTermChildren( TNode node );
 
   /** A proof node manager */
-  std::unique_ptr<ProofNodeManager> d_pnm;
+  ProofNodeManager* d_pnm;
   /**
    * A proof generator for the term conversion.
    */
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index 891c0f731..19795119d 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -21,7 +21,12 @@ namespace CVC4 {
 namespace smt {
 
 WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm)
-    : d_tcpg(pnm), d_wintroPf(pnm)
+    : d_tcpg(pnm,
+             nullptr,
+             TConvPolicy::FIXPOINT,
+             TConvCachePolicy::NEVER,
+             "WfGenerator::TConvProofGenerator"),
+      d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof")
 {
 }
 
@@ -89,7 +94,13 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t)
           // (exists ((x T)) (P x))
           // --------------------------- WITNESS_INTRO
           // k = (witness ((x T)) (P x))
-          d_wintroPf.addLazyStep(exists, pg, false, PfRule::WITNESS_AXIOM);
+          d_wintroPf.addLazyStep(
+              exists,
+              pg,
+              true,
+              "WitnessFormGenerator::convertToWitnessForm:witness_axiom",
+              false,
+              PfRule::WITNESS_AXIOM);
           d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {});
           d_tcpg.addRewriteStep(cur, curw, &d_wintroPf);
         }