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

1 files changed, 7 insertions, 7 deletions

diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index 691902945..e2bba3015 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -67,23 +67,23 @@ class LazyCDProof : public CDProof
    *
    * @param expected The fact that can be proven.
    * @param pg The generator that can proof expected.
+   * @param trustId If a null proof generator is provided, we add a step to
+   * the proof that has trustId as the rule and expected as the sole argument.
+   * We do this only if trustId is not PfRule::ASSUME. This is primarily used
+   * for identifying the kind of hole when a proof generator is not given.
    * @param isClosed Whether to expect that pg can provide a closed proof for
    * this fact.
    * @param ctx The context we are in (for debugging).
    * @param forceOverwrite If this flag is true, then this call overwrites
    * an existing proof generator provided for expected, if one was provided
    * via a previous call to addLazyStep in the current context.
-   * @param trustId If a null proof generator is provided, we add a step to
-   * the proof that has trustId as the rule and expected as the sole argument.
-   * We do this only if trustId is not PfRule::ASSUME. This is primarily used
-   * for identifying the kind of hole when a proof generator is not given.
    */
   void addLazyStep(Node expected,
                    ProofGenerator* pg,
-                   bool isClosed = true,
+                   PfRule trustId = PfRule::ASSUME,
+                   bool isClosed = false,
                    const char* ctx = "LazyCDProof::addLazyStep",
-                   bool forceOverwrite = false,
-                   PfRule trustId = PfRule::ASSUME);
+                   bool forceOverwrite = false);
   /**
    * Does this have any proof generators? This method always returns true
    * if the default is non-null.