From: Tim King <taking@cs.nyu.edu>
Date: Fri, 17 Aug 2018 06:48:17 +0000 (-0700)
Subject:  Initialize inputAssertions only when proofRecipe is non-null (#2325)
X-Git-Tag: cvc5-1.0.0~4767
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d303b5e6de8a3b963357a3c0238ffe81d36f766;p=cvc5.git

 Initialize inputAssertions only when proofRecipe is non-null (#2325)

Most of the PR is clang-format cruft from picking up the contents of a PROOF({ ... });
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index cedeb640f..0ccce95c9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -19,6 +19,7 @@
 #include <list>
 #include <vector>
 
+#include "base/map_util.h"
 #include "decision/decision_engine.h"
 #include "expr/attribute.h"
 #include "expr/node.h"
@@ -2110,8 +2111,14 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
   unsigned i = 0; // Index of the current literal we are processing
   unsigned j = 0; // Index of the last literal we are keeping
 
-  std::set<Node> inputAssertions;
-  PROOF(inputAssertions = proofRecipe->getStep(0)->getAssertions(););
+  std::unique_ptr<std::set<Node>> inputAssertions = nullptr;
+  PROOF({
+    if (proofRecipe)
+    {
+      inputAssertions.reset(
+          new std::set<Node>(proofRecipe->getStep(0)->getAssertions()));
+    }
+  });
 
   while (i < explanationVector.size()) {
     // Get the current literal to explain
@@ -2196,30 +2203,44 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     ++ i;
 
     PROOF({
-        if (proofRecipe) {
-          // If we're expanding the target node of the explanation (this is the first expansion...),
-          // we don't want to add it as a separate proof step. It is already part of the assertions.
-          if (inputAssertions.find(toExplain.node) == inputAssertions.end()) {
-            LemmaProofRecipe::ProofStep proofStep(toExplain.theory, toExplain.node);
-            if (explanation.getKind() == kind::AND) {
-              Node flat = flattenAnd(explanation);
-              for (unsigned k = 0; k < flat.getNumChildren(); ++ k) {
-                // If a true constant or a negation of a false constant we can ignore it
-                if (! ((flat[k].isConst() && flat[k].getConst<bool>()) ||
-                       (flat[k].getKind() == kind::NOT && flat[k][0].isConst() && !flat[k][0].getConst<bool>()))) {
-                  proofStep.addAssertion(flat[k].negate());
-                }
+      if (proofRecipe && inputAssertions)
+      {
+        // If we're expanding the target node of the explanation (this is the
+        // first expansion...), we don't want to add it as a separate proof
+        // step. It is already part of the assertions.
+        if (!ContainsKey(*inputAssertions, toExplain.node))
+        {
+          LemmaProofRecipe::ProofStep proofStep(toExplain.theory,
+                                                toExplain.node);
+          if (explanation.getKind() == kind::AND)
+          {
+            Node flat = flattenAnd(explanation);
+            for (unsigned k = 0; k < flat.getNumChildren(); ++k)
+            {
+              // If a true constant or a negation of a false constant we can
+              // ignore it
+              if (!((flat[k].isConst() && flat[k].getConst<bool>())
+                    || (flat[k].getKind() == kind::NOT && flat[k][0].isConst()
+                        && !flat[k][0].getConst<bool>())))
+              {
+                proofStep.addAssertion(flat[k].negate());
               }
-            } else {
-             if (! ((explanation.isConst() && explanation.getConst<bool>()) ||
-                    (explanation.getKind() == kind::NOT && explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
-               proofStep.addAssertion(explanation.negate());
-             }
             }
-            proofRecipe->addStep(proofStep);
           }
+          else
+          {
+            if (!((explanation.isConst() && explanation.getConst<bool>())
+                  || (explanation.getKind() == kind::NOT
+                      && explanation[0].isConst()
+                      && !explanation[0].getConst<bool>())))
+            {
+              proofStep.addAssertion(explanation.negate());
+            }
+          }
+          proofRecipe->addStep(proofStep);
         }
-      });
+      }
+    });
   }
 
   // Keep only the relevant literals