From bb816ef2cb29aaacda9d5f21d15b6fb120a64b19 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 Feb 2022 08:36:32 -0600 Subject: [PATCH] [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. --- src/theory/trust_substitutions.cpp | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) 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 TrustSubstitutionMap::getProofFor(Node eq) std::vector 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 -- 2.30.2