(proof-new) Implementation of trust substitution (#5276)

Trust substitution is a data structure that is used throughout preprocessing for proofs.

This adds its implementation.

5 files changed, 276 insertions, 14 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index e4719ff30..9448e1939 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -43,6 +43,7 @@ const char* toString(PfRule id)
     case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM";
     case PfRule::TRUST_REWRITE: return "TRUST_REWRITE";
     case PfRule::TRUST_SUBS: return "TRUST_SUBS";
+    case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP";
     //================================================= Boolean rules
     case PfRule::RESOLUTION: return "RESOLUTION";
     case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 340b636ae..4000d4df7 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -234,11 +234,14 @@ enum class PfRule : uint32_t
   // a witness term (witness ((x T)) (P x)).
   WITNESS_AXIOM,
   // where F is an equality (= t t') that holds by a form of rewriting that
-  // could not be replayed.
+  // could not be replayed during proof postprocessing.
   TRUST_REWRITE,
   // where F is an equality (= t t') that holds by a form of substitution that
-  // could not be replayed.
+  // could not be replayed during proof postprocessing.
   TRUST_SUBS,
+  // where F is an equality (= t t') that holds by a form of substitution that
+  // could not be determined by the TrustSubstitutionMap.
+  TRUST_SUBS_MAP,
 
   //================================================= Boolean rules
   // ======== Resolution
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 6fc4671ee..e59f48fff 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -76,6 +76,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
   pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
   pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
+  pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
 }
 
 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
@@ -397,7 +398,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   else if (id == PfRule::PREPROCESS || id == PfRule::THEORY_PREPROCESS
            || id == PfRule::WITNESS_AXIOM || id == PfRule::THEORY_LEMMA
            || id == PfRule::PREPROCESS_LEMMA || id == PfRule::THEORY_REWRITE
-           || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS)
+           || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS
+           || id == PfRule::TRUST_SUBS_MAP)
   {
     // "trusted" rules
     Assert(children.empty());
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index de8fc2ceb..482c487eb 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -20,41 +20,235 @@ namespace CVC4 {
 namespace theory {
 
 TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c,
-                                           ProofNodeManager* pnm)
-    : d_subs(c)
+                                           ProofNodeManager* pnm,
+                                           std::string name,
+                                           PfRule trustId,
+                                           MethodId ids)
+    : d_subs(c),
+      d_pnm(pnm),
+      d_tsubs(c),
+      d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr),
+      d_subsPg(
+          pnm ? new LazyCDProof(pnm, nullptr, c, "TrustSubstitutionMap::subsPg")
+              : nullptr),
+      d_applyPg(pnm ? new LazyCDProof(
+                          pnm, nullptr, c, "TrustSubstitutionMap::applyPg")
+                    : nullptr),
+      d_helperPf(pnm, c),
+      d_currentSubs(c),
+      d_name(name),
+      d_trustId(trustId),
+      d_ids(ids)
 {
 }
 
 void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
 {
+  Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: add " << x
+                      << " -> " << t << std::endl;
   d_subs.addSubstitution(x, t);
+  if (isProofEnabled())
+  {
+    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,
+                          false,
+                          "TrustSubstitutionMap::addSubstitution",
+                          false,
+                          d_trustId);
+  }
 }
 
-TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
+void TrustSubstitutionMap::addSubstitution(TNode x,
+                                           TNode t,
+                                           PfRule id,
+                                           const std::vector<Node>& args)
 {
-  Node ns = d_subs.apply(n);
-  if (doRewrite)
+  if (!isProofEnabled())
   {
-    ns = Rewriter::rewrite(ns);
+    addSubstitution(x, t, nullptr);
+    return;
   }
-  return TrustNode::mkTrustRewrite(n, ns, nullptr);
+  LazyCDProof* stepPg = d_helperPf.allocateProof();
+  Node eq = x.eqNode(t);
+  stepPg->addStep(eq, id, {}, args);
+  addSubstitution(x, t, stepPg);
 }
 
 void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
 {
+  Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add "
+                      << x << " -> " << t << " from " << tn.getProven()
+                      << std::endl;
   if (!isProofEnabled() || tn.getGenerator() == nullptr)
   {
     // no generator or not proof enabled, nothing to do
     addSubstitution(x, t, nullptr);
+    Trace("trust-subs") << "...no proof" << std::endl;
+    return;
+  }
+  Node eq = x.eqNode(t);
+  Node proven = tn.getProven();
+  // notice that this checks syntactic equality, not CDProof::isSame since
+  // tn.getGenerator() is not necessarily robust to symmetry.
+  if (eq == proven)
+  {
+    // no rewrite required, just use the generator
+    addSubstitution(x, t, tn.getGenerator());
+    Trace("trust-subs") << "...use generator directly" << std::endl;
     return;
   }
-  // NOTE: can try to transform tn.getProven() to (= x t) here
-  addSubstitution(x, t, nullptr);
+  LazyCDProof* solvePg = d_helperPf.allocateProof();
+  // Try to transform tn.getProven() to (= x t) here, if necessary
+  if (!d_tspb->applyPredTransform(proven, eq, {}))
+  {
+    // failed to rewrite
+    addSubstitution(x, t, nullptr);
+    Trace("trust-subs") << "...failed to rewrite" << std::endl;
+    return;
+  }
+  Trace("trust-subs") << "...successful rewrite" << std::endl;
+  solvePg->addSteps(*d_tspb.get());
+  d_tspb->clear();
+  // link the given generator
+  solvePg->addLazyStep(proven, tn.getGenerator());
+  addSubstitution(x, t, solvePg);
+}
+
+void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
+{
+  if (!isProofEnabled())
+  {
+    // just use the basic utility
+    d_subs.addSubstitutions(t.get());
+    return;
+  }
+  // call addSubstitution above in sequence
+  for (const TrustNode& tns : t.d_tsubs)
+  {
+    Node proven = tns.getProven();
+    addSubstitution(proven[0], proven[1], tns.getGenerator());
+  }
+}
+
+TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
+{
+  Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
+                      << std::endl;
+  Node ns = d_subs.apply(n);
+  Trace("trust-subs") << "...subs " << ns << std::endl;
+  // rewrite if indicated
+  if (doRewrite)
+  {
+    ns = Rewriter::rewrite(ns);
+    Trace("trust-subs") << "...rewrite " << ns << std::endl;
+  }
+  if (n == ns)
+  {
+    // no change
+    return TrustNode::null();
+  }
+  if (!isProofEnabled())
+  {
+    // 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;
+  // 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,
+  // and we are asked to transform x, resulting in 5, we hence must provide
+  // a proof of (= x 5) based on the substitution. However, it must be the
+  // case that (= x 5) is a proven fact of the substitution generator. Hence
+  // we avoid a proof that looks like:
+  // ---------- from d_subsPg
+  // (= x 5)
+  // ---------- 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());
+  }
+  Assert(eq != cs);
+  std::vector<Node> pfChildren;
+  if (!cs.isConst())
+  {
+    // note we will get more proof reuse if we do not special case AND here.
+    if (cs.getKind() == kind::AND)
+    {
+      for (const Node& csc : cs)
+      {
+        pfChildren.push_back(csc);
+        // connect substitution generator into apply generator
+        d_applyPg->addLazyStep(csc, d_subsPg.get());
+      }
+    }
+    else
+    {
+      pfChildren.push_back(cs);
+      // connect substitution generator into apply generator
+      d_applyPg->addLazyStep(cs, d_subsPg.get());
+    }
+  }
+  if (!d_tspb->applyEqIntro(n, ns, pfChildren, d_ids))
+  {
+    return TrustNode::mkTrustRewrite(n, ns, nullptr);
+  }
+  // -------        ------- from external proof generators
+  // x1 = t1 ...    xn = tn
+  // ----------------------- AND_INTRO
+  //   ...
+  // --------- MACRO_SR_EQ_INTRO
+  // n == ns
+  // add it to the apply proof generator.
+  //
+  // Notice that we use a single child to MACRO_SR_EQ_INTRO here. This is an
+  // optimization motivated by the fact that n may be large and reused many
+  // time. For instance, if this class is being used to track substitutions
+  // derived during non-clausal simplification during preprocessing, it is
+  // a fixed (possibly) large substitution applied to many terms. Having
+  // a single child saves us from creating many proofs with n children, where
+  // notice this proof is reused.
+  d_applyPg->addSteps(*d_tspb.get());
+  d_tspb->clear();
+  return TrustNode::mkTrustRewrite(n, ns, d_applyPg.get());
 }
 
 SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; }
 
-bool TrustSubstitutionMap::isProofEnabled() const { return false; }
+bool TrustSubstitutionMap::isProofEnabled() const
+{
+  return d_subsPg != nullptr;
+}
+
+Node TrustSubstitutionMap::getCurrentSubstitution()
+{
+  Assert(isProofEnabled());
+  if (!d_currentSubs.get().isNull())
+  {
+    return d_currentSubs;
+  }
+  std::vector<Node> csubsChildren;
+  for (const TrustNode& tns : d_tsubs)
+  {
+    csubsChildren.push_back(tns.getProven());
+  }
+  d_currentSubs = NodeManager::currentNM()->mkAnd(csubsChildren);
+  if (d_currentSubs.get().getKind() == kind::AND)
+  {
+    d_subsPg->addStep(d_currentSubs, PfRule::AND_INTRO, csubsChildren, {});
+  }
+  return d_currentSubs;
+}
 
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index 0eacc50f5..91555ee56 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -17,9 +17,15 @@
 #ifndef CVC4__THEORY__TRUST_SUBSTITUTIONS_H
 #define CVC4__THEORY__TRUST_SUBSTITUTIONS_H
 
+#include "context/cdlist.h"
 #include "context/context.h"
+#include "expr/lazy_proof.h"
+#include "expr/lazy_proof_set.h"
 #include "expr/proof_node_manager.h"
+#include "expr/term_conversion_proof_generator.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/substitutions.h"
+#include "theory/theory_proof_step_buffer.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
@@ -31,7 +37,11 @@ namespace theory {
 class TrustSubstitutionMap
 {
  public:
-  TrustSubstitutionMap(context::Context* c, ProofNodeManager* pnm);
+  TrustSubstitutionMap(context::Context* c,
+                       ProofNodeManager* pnm,
+                       std::string name = "TrustSubstitutionMap",
+                       PfRule trustId = PfRule::TRUST_SUBS_MAP,
+                       MethodId ids = MethodId::SB_DEFAULT);
   /** Gets a reference to the underlying substitution map */
   SubstitutionMap& get();
   /**
@@ -40,6 +50,14 @@ class TrustSubstitutionMap
    */
   void addSubstitution(TNode x, TNode t, ProofGenerator* pg = nullptr);
   /**
+   * Add substitution x -> t from a single proof step with rule id, no children
+   * and arguments args.
+   */
+  void addSubstitution(TNode x,
+                       TNode t,
+                       PfRule id,
+                       const std::vector<Node>& args);
+  /**
    * Add substitution x -> t, which was derived from the proven field of
    * trust node tn. In other words, (= x t) is the solved form of
    * tn.getProven(). This method is a helper function for methods (e.g.
@@ -53,6 +71,11 @@ class TrustSubstitutionMap
    */
   void 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.
+   */
+  void addSubstitutions(TrustSubstitutionMap& t);
+  /**
    * Apply substitutions in this class to node n. Returns a trust node
    * proving n = n*sigma, where the proof generator is provided by this class
    * (when proofs are enabled).
@@ -62,8 +85,47 @@ class TrustSubstitutionMap
  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.
+   */
+  Node getCurrentSubstitution();
   /** The substitution map */
   SubstitutionMap d_subs;
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** A context-dependent list of trust nodes */
+  context::CDList<TrustNode> d_tsubs;
+  /** Theory proof step buffer */
+  std::unique_ptr<TheoryProofStepBuffer> d_tspb;
+  /** A lazy proof for substitution steps */
+  std::unique_ptr<LazyCDProof> d_subsPg;
+  /** A lazy proof for apply steps */
+  std::unique_ptr<LazyCDProof> d_applyPg;
+  /**
+   * A context-dependent list of LazyCDProof, allocated for internal steps.
+   */
+  LazyCDProofSet 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;
+  /**
+   * The placeholder trusted PfRule identifier for calls to addSubstitution
+   * that are not given proof generators.
+   */
+  PfRule d_trustId;
+  /** The method id for which form of substitution to apply */
+  MethodId d_ids;
 };
 
 }  // namespace theory