From 64a7db86206aa0993f75446a3e7f77f3c0c023c6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 11 Jul 2020 07:45:35 -0500 Subject: [PATCH] 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 . --- src/theory/theory_engine.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) 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& explanationVector new std::set(proofRecipe->getStep(0)->getAssertions())); } }); + // cache of nodes we have already explained by some theory + std::unordered_set cache; while (i < explanationVector.size()) { // Get the current literal to explain @@ -1868,7 +1870,15 @@ void TheoryEngine::getExplanation(std::vector& 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) -- 2.30.2