[proofs] Consolidate multiple substitutions to single AND proof in trust substitution...

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 ea87829a9ffc0debe096d17d34b57e41008313aa..57681688be2ec80a0e9e5ede2bd3886e65001078 100644 (file)
--- 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