diff options
author | Tim King <taking@cs.nyu.edu> | 2018-08-16 23:48:17 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-16 23:48:17 -0700 |
commit | 4d303b5e6de8a3b963357a3c0238ffe81d36f766 (patch) | |
tree | 54ef2fbfa6a57dee7753d39522fed89e21affa7f | |
parent | 420f25b1c8103bec7d5fd63a8ade2d9373395e55 (diff) |
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({ ... });
-rw-r--r-- | src/theory/theory_engine.cpp | 65 |
1 files changed, 43 insertions, 22 deletions
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 |