Make trust substitution map generate proofs lazily (#6379)

This is work towards addressing a bottleneck when generating proofs for substitutions from non-clausal simplification.

This makes the proof generation in trust substitution map lazy.

Further work is required to allow an alternative fixpoint semantics for substitutions in the proof checker instead of the current sequential one.

1 files changed, 35 insertions, 24 deletions

diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index 6d41b1bef..3e5b04d86 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -37,10 +37,10 @@ TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c,
                           pnm, nullptr, c, "TrustSubstitutionMap::applyPg")
                     : nullptr),
       d_helperPf(pnm, c),
-      d_currentSubs(c),
       d_name(name),
       d_trustId(trustId),
-      d_ids(ids)
+      d_ids(ids),
+      d_eqtIndex(c)
 {
 }
 
@@ -53,8 +53,6 @@ void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
   {
     TrustNode tnl = TrustNode::mkTrustRewrite(x, t, pg);
     d_tsubs.push_back(tnl);
-    // current substitution node is no longer valid.
-    d_currentSubs = Node::null();
     // add to lazy proof
     d_subsPg->addLazyStep(tnl.getProven(), pg, d_trustId);
   }
@@ -151,10 +149,18 @@ TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
     // no proofs, use null generator
     return TrustNode::mkTrustRewrite(n, ns, nullptr);
   }
-  Node cs = getCurrentSubstitution();
-  Trace("trust-subs")
-      << "TrustSubstitutionMap::addSubstitution: current substitution is " << cs
-      << std::endl;
+  Node eq = n.eqNode(ns);
+  // remember the index
+  d_eqtIndex[eq] = d_tsubs.size();
+  // this class will provide a proof if asked
+  return TrustNode::mkTrustRewrite(n, ns, this);
+}
+
+std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
+{
+  Assert(eq.getKind() == kind::EQUAL);
+  Node n = eq[0];
+  Node ns = eq[1];
   // Easy case: if n is in the domain of the substitution, maybe it is already
   // a proof in the substitution proof generator. This is moreover required
   // to avoid cyclic proofs below. For example, if { x -> 5 } is a substitution,
@@ -167,11 +173,15 @@ TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
   // ---------- MACRO_SR_EQ_INTRO{x}
   // (= x 5)
   // by taking the premise proof directly.
-  Node eq = n.eqNode(ns);
   if (d_subsPg->hasStep(eq) || d_subsPg->hasGenerator(eq))
   {
-    return TrustNode::mkTrustRewrite(n, ns, d_subsPg.get());
+    return d_subsPg->getProofFor(eq);
   }
+  NodeUIntMap::iterator it = d_eqtIndex.find(eq);
+  Assert(it != d_eqtIndex.end());
+  Trace("trust-subs-pf") << "TrustSubstitutionMap::getProofFor, # assumptions= "
+                         << it->second << std::endl;
+  Node cs = getSubstitution(it->second);
   Assert(eq != cs);
   std::vector<Node> pfChildren;
   if (!cs.isConst())
@@ -193,11 +203,13 @@ TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
       d_applyPg->addLazyStep(cs, d_subsPg.get());
     }
   }
+  Trace("trust-subs-pf") << "...apply eq intro" << std::endl;
   if (!d_tspb->applyEqIntro(n, ns, pfChildren, d_ids))
   {
     // if we fail for any reason, we must use a trusted step instead
     d_tspb->addStep(PfRule::TRUST_SUBS_MAP, pfChildren, {eq}, eq);
   }
+  Trace("trust-subs-pf") << "...made steps" << std::endl;
   // -------        ------- from external proof generators
   // x1 = t1 ...    xn = tn
   // ----------------------- AND_INTRO
@@ -215,9 +227,12 @@ TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
   // notice this proof is reused.
   d_applyPg->addSteps(*d_tspb.get());
   d_tspb->clear();
-  return TrustNode::mkTrustRewrite(n, ns, d_applyPg.get());
+  Trace("trust-subs-pf") << "...finish, make proof" << std::endl;
+  return d_applyPg->getProofFor(eq);
 }
 
+std::string TrustSubstitutionMap::identify() const { return d_name; }
+
 SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; }
 
 bool TrustSubstitutionMap::isProofEnabled() const
@@ -225,25 +240,21 @@ bool TrustSubstitutionMap::isProofEnabled() const
   return d_subsPg != nullptr;
 }
 
-Node TrustSubstitutionMap::getCurrentSubstitution()
+Node TrustSubstitutionMap::getSubstitution(size_t index)
 {
-  Assert(isProofEnabled());
-  if (!d_currentSubs.get().isNull())
-  {
-    return d_currentSubs;
-  }
+  Assert(index <= d_tsubs.size());
   std::vector<Node> csubsChildren;
-  for (const TrustNode& tns : d_tsubs)
+  for (size_t i = 0; i < index; i++)
   {
-    csubsChildren.push_back(tns.getProven());
+    csubsChildren.push_back(d_tsubs[i].getProven());
   }
-  std::reverse(csubsChildren.begin(),csubsChildren.end());
-  d_currentSubs = NodeManager::currentNM()->mkAnd(csubsChildren);
-  if (d_currentSubs.get().getKind() == kind::AND)
+  std::reverse(csubsChildren.begin(), csubsChildren.end());
+  Node cs = NodeManager::currentNM()->mkAnd(csubsChildren);
+  if (cs.getKind() == kind::AND)
   {
-    d_subsPg->addStep(d_currentSubs, PfRule::AND_INTRO, csubsChildren, {});
+    d_subsPg->addStep(cs, PfRule::AND_INTRO, csubsChildren, {});
   }
-  return d_currentSubs;
+  return cs;
 }
 
 }  // namespace theory