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 .

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 851ae414e82848bb7cdbb195ad65f0eb0bc54b7e..2bbdcceb311bbea1ebec6daaff94b79bc6035999 100644 (file)
--- 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)