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/strings/kinds | |
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/strings/kinds')
0 files changed, 0 insertions, 0 deletions