(proof-new) Update add lazy step interface in LazyCDProof (#5299)

Ensuring closed proofs should not be enabled by default, it is actually not used very often as a whole. Moreover, the "trust id" argument is the most useful argument and hence should come as the 3rd argument. This updates all uses of addLazyStep for the change in interface, also changes term conversion generator which had a similar issue with default arguments.

Notice that some calls to addLazyStep were checking closed but without providing a debug string, these I've left alone (they no longer check closed).

3 files changed, 8 insertions, 12 deletions

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 0c2f8ccf8..a7723d265 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -460,8 +460,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
           // add previous rewrite steps
           for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
           {
-            // not necessarily closed, so we pass false to addRewriteStep.
-            tcg.addRewriteStep(vvec[j], svec[j], pgs[j], false);
+            tcg.addRewriteStep(vvec[j], svec[j], pgs[j]);
           }
           // get the proof for the update to the current substitution
           Node seqss = subs.eqNode(ss);
@@ -506,8 +505,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
                                true);
       for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
       {
-        // not necessarily closed, so we pass false to addRewriteStep.
-        tcpg.addRewriteStep(vvec[j], svec[j], pgs[j], false);
+        tcpg.addRewriteStep(vvec[j], svec[j], pgs[j]);
       }
       // add the proof constructed by the term conversion utility
       std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(eq);
@@ -545,10 +543,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     Node eq = args[0].eqNode(ret);
     if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT)
     {
-      // rewrites from theory::Rewriter
       // automatically expand THEORY_REWRITE as well here if set
       bool elimTR =
           (d_elimRules.find(PfRule::THEORY_REWRITE) != d_elimRules.end());
+      // rewrites from theory::Rewriter
       bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT);
       // use rewrite with proof interface
       Rewriter* rr = d_smte->getRewriter();
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index cf7c00e2b..46135f12a 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -334,10 +334,9 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
           ProofGenerator* expg = sm->getProofGenerator(existsAssertion);
           d_lp->addLazyStep(existsAssertion,
                             expg,
+                            PfRule::WITNESS_AXIOM,
                             true,
-                            "RemoveTermFormulas::run:skolem_pf",
-                            false,
-                            PfRule::WITNESS_AXIOM);
+                            "RemoveTermFormulas::run:skolem_pf");
           d_lp->addStep(newAssertion, PfRule::SKOLEMIZE, {existsAssertion}, {});
           newAssertionPg = d_lp.get();
         }
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index e4f0a56dc..9c2c035a8 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -114,12 +114,11 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t)
           d_wintroPf.addLazyStep(
               exists,
               pg,
+              PfRule::WITNESS_AXIOM,
               true,
-              "WitnessFormGenerator::convertToWitnessForm:witness_axiom",
-              false,
-              PfRule::WITNESS_AXIOM);
+              "WitnessFormGenerator::convertToWitnessForm:witness_axiom");
           d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {});
-          d_tcpg.addRewriteStep(cur, curw, &d_wintroPf);
+          d_tcpg.addRewriteStep(cur, curw, &d_wintroPf, PfRule::ASSUME, true);
         }
         else
         {