From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 17 Feb 2022 14:36:32 +0000 (-0600)
Subject: [proofs] Consolidate multiple substitutions to single AND proof in trust substitution... 
X-Git-Tag: cvc5-1.0.0~421
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bb816ef2cb29aaacda9d5f21d15b6fb120a64b19;p=cvc5.git

[proofs] Consolidate multiple substitutions to single AND proof in trust substitution map (#8109)

This ensures that a common proof node is used for a substitution instead of copying its children. This optimization had been noted in a comment but had not yet been enabled.

This should speed up proof reconstruction for substitutions.
---

diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index ea87829a9..57681688b 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -212,22 +212,11 @@ std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
   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());
-    }
+    // note that cs may be an AND node, in which case it specifies multiple
+    // substitutions
+    pfChildren.push_back(cs);
+    // connect substitution generator into apply generator
+    d_applyPg->addLazyStep(cs, d_subsPg.get());
   }
   Trace("trust-subs-pf") << "...apply eq intro" << std::endl;
   // We use fixpoint as the substitution-apply identifier. Notice that it