Cache explanations in TheoryEngine::getExplanation (#4722)

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 .