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/base/modal_exception.h | |
| 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/base/modal_exception.h')
0 files changed, 0 insertions, 0 deletions