projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1753106) | patch
Always consider rewritten lemmas for caching. (#5696)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 17 Dec 2020 16:28:10 +0000 (17:28 +0100)
committerGitHub <noreply@github.com>
Thu, 17 Dec 2020 16:28:10 +0000 (17:28 +0100)
commitdb157ade422c4bc16750d2cb6db7643f1fd3dad6
tree0f64ff3b62322f353df0790dce8b19575c546128tree
parent1753106f61bca87513a84493b643e2a7e245e0f5commit | diff
Always consider rewritten lemmas for caching. (#5696)

The TheoryInferenceManager cached lemmas as they came in. This PR always rewrites before consulting the cache, making caching more consistent and robust. This change is coming in from proof-new.
src/theory/arith/inference_manager.cpp diff | blob | history
src/theory/theory_inference_manager.cpp diff | blob | history