(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, 13 insertions, 2 deletions

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);
         }