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

diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 77ee1effd..184584aa9 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -68,7 +68,7 @@ bool ProofEqEngine::assertFact(Node lit,
   ps.d_args = args;
   d_factPg.addStep(lit, ps);
   // add lazy step to proof
-  d_proof.addLazyStep(lit, &d_factPg, false);
+  d_proof.addLazyStep(lit, &d_factPg);
   // second, assert it to the equality engine
   Node reason = NodeManager::currentNM()->mkAnd(exp);
   return assertFactInternal(atom, polarity, reason);
@@ -116,7 +116,7 @@ bool ProofEqEngine::assertFact(Node lit,
   ps.d_args = args;
   d_factPg.addStep(lit, ps);
   // add lazy step to proof
-  d_proof.addLazyStep(lit, &d_factPg, false);
+  d_proof.addLazyStep(lit, &d_factPg);
   // second, assert it to the equality engine
   return assertFactInternal(atom, polarity, exp);
 }
@@ -140,7 +140,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
     d_factPg.addStep(step.first, step.second);
   }
   // add lazy step to proof
-  d_proof.addLazyStep(lit, &d_factPg, false);
+  d_proof.addLazyStep(lit, &d_factPg);
   // second, assert it to the equality engine
   return assertFactInternal(atom, polarity, exp);
 }
@@ -157,7 +157,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg)
     return false;
   }
   // note the proof generator is responsible for remembering the explanation
-  d_proof.addLazyStep(lit, pg, false);
+  d_proof.addLazyStep(lit, pg);
   // second, assert it to the equality engine
   return assertFactInternal(atom, polarity, exp);
 }