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.

2 files changed, 59 insertions, 39 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
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index c875eca2f..2082a5dae 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__THEORY__TRUST_SUBSTITUTIONS_H
 #define CVC5__THEORY__TRUST_SUBSTITUTIONS_H
 
+#include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/lazy_proof.h"
@@ -35,8 +36,10 @@ namespace theory {
 /**
  * A layer on top of SubstitutionMap that tracks proofs.
  */
-class TrustSubstitutionMap
+class TrustSubstitutionMap : public ProofGenerator
 {
+  using NodeUIntMap = context::CDHashMap<Node, size_t, NodeHashFunction>;
+
  public:
   TrustSubstitutionMap(context::Context* c,
                        ProofNodeManager* pnm,
@@ -85,16 +88,18 @@ class TrustSubstitutionMap
    */
   TrustNode apply(Node n, bool doRewrite = true);
 
+  /** Get the proof for formula f */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** Identify */
+  std::string identify() const override;
+
  private:
   /** Are proofs enabled? */
   bool isProofEnabled() const;
   /**
-   * Get current substitution. This returns a node of the form:
-   *   (and (= x1 t1) ... (= xn tn))
-   * where (x1, t1) ... (xn, tn) have been registered via addSubstitution above.
-   * Moreover, it ensures that d_subsPg has a proof of the returned value.
+   * Get the substitution up to index
    */
-  Node getCurrentSubstitution();
+  Node getSubstitution(size_t index);
   /** The context used here */
   context::Context* d_ctx;
   /** The substitution map */
@@ -113,15 +118,6 @@ class TrustSubstitutionMap
    * A context-dependent list of LazyCDProof, allocated for internal steps.
    */
   CDProofSet<LazyCDProof> d_helperPf;
-  /**
-   * The formula corresponding to the current substitution. This is of the form
-   *   (and (= x1 t1) ... (= xn tn))
-   * when the substitution map contains { x1 -> t1, ... xn -> tn }. This field
-   * is updated on demand. When this class applies a substitution to a node,
-   * this formula is computed and recorded as the premise of a
-   * MACRO_SR_EQ_INTRO step.
-   */
-  context::CDO<Node> d_currentSubs;
   /** Name for debugging */
   std::string d_name;
   /**
@@ -131,6 +127,19 @@ class TrustSubstitutionMap
   PfRule d_trustId;
   /** The method id for which form of substitution to apply */
   MethodId d_ids;
+  /**
+   * Map from solved equalities to the size of d_tsubs at the time they
+   * were concluded. Notice this is required so that we can reconstruct
+   * proofs for substitutions after they have become invalidated by later
+   * calls to addSubstitution. For example, if we call:
+   *   addSubstitution x -> y
+   *   addSubstitution z -> w
+   *   apply f(x), returns f(y)
+   *   addSubstitution y -> w
+   * We map (= (f x) (f y)) to index 2, since we only should apply the first
+   * two substitutions but not the third when asked to prove this equality.
+   */
+  NodeUIntMap d_eqtIndex;
 };
 
 }  // namespace theory