diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-11 07:45:35 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-11 07:45:35 -0500 |
commit | 64a7db86206aa0993f75446a3e7f77f3c0c023c6 (patch) | |
tree | e9d10dfdda8f17a73c0c6ed8620072bd52cd8ff8 /src/theory/theory_engine.cpp | |
parent | c481454a4b05a78ea99e835ec7427a719a2d5c77 (diff) |
Cache explanations in TheoryEngine::getExplanation (#4722)
For some hard verification benchmarks from Facebook, TheoryEngine::getExplanation was found to be the bottleneck, where the main loop of TheoryEngine::getExplanation would be run regularly 30k times, sometimes over 1 million times for a single conflict.
This caches explanations in this loop, where now the loop is executed roughly 1k times at max for the same benchmark.
One challenging benchmark that previously solved in 8 min 45 sec now solves in 2 min 45 sec.
FYI @barrettcw .
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 851ae414e..2bbdcceb3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1787,6 +1787,8 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector new std::set<Node>(proofRecipe->getStep(0)->getAssertions())); } }); + // cache of nodes we have already explained by some theory + std::unordered_set<Node, NodeHashFunction> cache; while (i < explanationVector.size()) { // Get the current literal to explain @@ -1868,7 +1870,15 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector continue; } } - + // We must cache after checking the timestamp in the block of code above. + // Afterwards, we can ignore this timestamp, as well as caching the Node, + // since any theory's explanation will suffice. + if (cache.find(toExplain.d_node) != cache.end()) + { + ++i; + continue; + } + cache.insert(toExplain.d_node); // It was produced by the theory, so ask for an explanation Node explanation; if (toExplain.d_theory == THEORY_BUILTIN) |