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

15 files changed, 64 insertions, 58 deletions

diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index a96e30fde..267da2607 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -133,10 +133,10 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
 
 void LazyCDProof::addLazyStep(Node expected,
                               ProofGenerator* pg,
+                              PfRule idNull,
                               bool isClosed,
                               const char* ctx,
-                              bool forceOverwrite,
-                              PfRule idNull)
+                              bool forceOverwrite)
 {
   if (pg == nullptr)
   {
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.
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index 11e8eb054..02613345f 100644
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -62,13 +62,17 @@ TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
 
 TConvProofGenerator::~TConvProofGenerator() {}
 
-void TConvProofGenerator::addRewriteStep(
-    Node t, Node s, ProofGenerator* pg, bool isClosed, uint32_t tctx)
+void TConvProofGenerator::addRewriteStep(Node t,
+                                         Node s,
+                                         ProofGenerator* pg,
+                                         PfRule trustId,
+                                         bool isClosed,
+                                         uint32_t tctx)
 {
   Node eq = registerRewriteStep(t, s, tctx);
   if (!eq.isNull())
   {
-    d_proof.addLazyStep(eq, pg, isClosed);
+    d_proof.addLazyStep(eq, pg, trustId, isClosed);
   }
 }
 
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index 184f24e13..0a1f4e70a 100644
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -144,6 +144,8 @@ class TConvProofGenerator : public ProofGenerator
   /**
    * Add rewrite step t --> s based on proof generator.
    *
+   * @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.
    * @param isClosed whether to expect that pg can provide a closed proof for
    * this fact.
    * @param tctx The term context identifier for the rewrite step. This
@@ -154,7 +156,8 @@ class TConvProofGenerator : public ProofGenerator
   void addRewriteStep(Node t,
                       Node s,
                       ProofGenerator* pg,
-                      bool isClosed = true,
+                      PfRule trustId = PfRule::ASSUME,
+                      bool isClosed = false,
                       uint32_t tctx = 0);
   /** Same as above, for a single step */
   void addRewriteStep(Node t, Node s, ProofStep ps, uint32_t tctx = 0);
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 78c459cb7..cd7aadf9a 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -177,7 +177,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
       //   rewrite( d_nodes[i] ^ n )
       // allocate a fresh proof which will act as the proof generator
       LazyCDProof* lcp = d_pppg->allocateHelperProof();
-      lcp->addLazyStep(n, pg, false);
+      lcp->addLazyStep(n, pg, PfRule::PREPROCESS);
       if (d_nodes[i].isConst() && d_nodes[i].getConst<bool>())
       {
         // skip the AND_INTRO if the previous d_nodes[i] was true
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index b2d33a61d..790e5aeb2 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -81,8 +81,11 @@ void ProofCnfStream::convertAndAssert(TNode node,
     Trace("cnf") << "ProofCnfStream::convertAndAssert: pg: " << pg->identify()
                  << "\n";
     Node toJustify = negated ? node.notNode() : static_cast<Node>(node);
-    d_proof.addLazyStep(
-        toJustify, pg, true, "ProofCnfStream::convertAndAssert:cnf");
+    d_proof.addLazyStep(toJustify,
+                        pg,
+                        PfRule::ASSUME,
+                        true,
+                        "ProofCnfStream::convertAndAssert:cnf");
   }
   convertAndAssert(node, negated);
   // process saved steps in buffer
@@ -519,8 +522,11 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn)
   Assert(trn.getGenerator()->getProofFor(proven)->isClosed());
   Trace("cnf-steps") << proven << " by explainPropagation "
                      << trn.identifyGenerator() << std::endl;
-  d_proof.addLazyStep(
-      proven, trn.getGenerator(), true, "ProofCnfStream::convertPropagation");
+  d_proof.addLazyStep(proven,
+                      trn.getGenerator(),
+                      PfRule::ASSUME,
+                      true,
+                      "ProofCnfStream::convertPropagation");
   // since the propagation is added directly to the SAT solver via theoryProxy,
   // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here
   NodeManager* nm = NodeManager::currentNM();
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
         {
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index f88c2e7a0..8549b1eae 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -268,10 +268,9 @@ bool Instantiate::addInstantiation(
       // add the transformation proof, or THEORY_PREPROCESS if none provided
       pfTmp->addLazyStep(proven,
                          tpBody.getGenerator(),
+                         PfRule::THEORY_PREPROCESS,
                          true,
-                         "Instantiate::getInstantiation:qpreprocess",
-                         false,
-                         PfRule::THEORY_PREPROCESS);
+                         "Instantiate::getInstantiation:qpreprocess");
       pfTmp->addStep(body, PfRule::EQ_RESOLVE, {orig_body, proven}, {});
     }
   }
@@ -477,10 +476,9 @@ Node Instantiate::getInstantiation(Node q,
         Node proven = trn.getProven();
         pf->addLazyStep(proven,
                         trn.getGenerator(),
+                        PfRule::THEORY_PREPROCESS,
                         true,
-                        "Instantiate::getInstantiation:rewrite_inst",
-                        false,
-                        PfRule::THEORY_PREPROCESS);
+                        "Instantiate::getInstantiation:rewrite_inst");
         pf->addStep(newBody, PfRule::EQ_RESOLVE, {body, proven}, {});
       }
       body = newBody;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index aaa010148..924d045da 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1462,10 +1462,9 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
         {
           d_lazyProof->addLazyStep(tplemma.getProven(),
                                    tplemma.getGenerator(),
+                                   PfRule::PREPROCESS_LEMMA,
                                    true,
-                                   "TheoryEngine::lemma_pp",
-                                   false,
-                                   PfRule::PREPROCESS_LEMMA);
+                                   "TheoryEngine::lemma_pp");
           // ---------- from d_lazyProof -------------- from theory preprocess
           // lemma                       lemma = lemmap
           // ------------------------------------------ EQ_RESOLVE
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index e7cdb8f2c..b37a45967 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -213,10 +213,9 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
         // store in the lazy proof
         d_lp->addLazyStep(assertion,
                           trn.getGenerator(),
+                          PfRule::THEORY_PREPROCESS_LEMMA,
                           true,
-                          "TheoryPreprocessor::rewrite_lemma_new",
-                          false,
-                          PfRule::THEORY_PREPROCESS_LEMMA);
+                          "TheoryPreprocessor::rewrite_lemma_new");
         d_lp->addStep(rewritten,
                       PfRule::MACRO_SR_PRED_TRANSFORM,
                       {assertion},
@@ -433,7 +432,8 @@ Node TheoryPreprocessor::preprocessWithProof(Node term)
       trn.debugCheckClosed("tpp-proof-debug",
                            "TheoryPreprocessor::preprocessWithProof");
       // always use term context hash 0 (default)
-      d_tpg->addRewriteStep(term, termr, trn.getGenerator());
+      d_tpg->addRewriteStep(
+          term, termr, trn.getGenerator(), PfRule::ASSUME, true);
     }
     else
     {
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index 482c487eb..27159f964 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -54,12 +54,7 @@ void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
     // current substitution node is no longer valid.
     d_currentSubs = Node::null();
     // add to lazy proof
-    d_subsPg->addLazyStep(tnl.getProven(),
-                          pg,
-                          false,
-                          "TrustSubstitutionMap::addSubstitution",
-                          false,
-                          d_trustId);
+    d_subsPg->addLazyStep(tnl.getProven(), pg, d_trustId);
   }
 }
 
@@ -79,7 +74,9 @@ void TrustSubstitutionMap::addSubstitution(TNode x,
   addSubstitution(x, t, stepPg);
 }
 
-void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
+ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x,
+                                                            TNode t,
+                                                            TrustNode tn)
 {
   Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add "
                       << x << " -> " << t << " from " << tn.getProven()
@@ -89,7 +86,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
     // no generator or not proof enabled, nothing to do
     addSubstitution(x, t, nullptr);
     Trace("trust-subs") << "...no proof" << std::endl;
-    return;
+    return nullptr;
   }
   Node eq = x.eqNode(t);
   Node proven = tn.getProven();
@@ -100,7 +97,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
     // no rewrite required, just use the generator
     addSubstitution(x, t, tn.getGenerator());
     Trace("trust-subs") << "...use generator directly" << std::endl;
-    return;
+    return tn.getGenerator();
   }
   LazyCDProof* solvePg = d_helperPf.allocateProof();
   // Try to transform tn.getProven() to (= x t) here, if necessary
@@ -109,7 +106,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
     // failed to rewrite
     addSubstitution(x, t, nullptr);
     Trace("trust-subs") << "...failed to rewrite" << std::endl;
-    return;
+    return nullptr;
   }
   Trace("trust-subs") << "...successful rewrite" << std::endl;
   solvePg->addSteps(*d_tspb.get());
@@ -117,6 +114,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
   // link the given generator
   solvePg->addLazyStep(proven, tn.getGenerator());
   addSubstitution(x, t, solvePg);
+  return solvePg;
 }
 
 void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index 91555ee56..d7f48d054 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -68,8 +68,10 @@ class TrustSubstitutionMap
    * based on transforming the tn.getProven() to (= x t) if tn has a
    * non-null proof generator; otherwise if tn has no proof generator
    * we simply add the substitution.
+   *
+   * @return The proof generator that can prove (= x t).
    */
-  void addSubstitutionSolved(TNode x, TNode t, TrustNode tn);
+  ProofGenerator* addSubstitutionSolved(TNode x, TNode t, TrustNode tn);
   /**
    * Add substitutions from trust substitution map t. This adds all
    * substitutions from the map t and carries over its information about proofs.
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);
 }