diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2020-12-17 17:28:10 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-17 17:28:10 +0100 |
commit | db157ade422c4bc16750d2cb6db7643f1fd3dad6 (patch) | |
tree | 0f64ff3b62322f353df0790dce8b19575c546128 /src | |
parent | 1753106f61bca87513a84493b643e2a7e245e0f5 (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.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/inference_manager.cpp | 13 | ||||
-rw-r--r-- | src/theory/theory_inference_manager.cpp | 8 |
2 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index e22be81e3..e79c12155 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -34,7 +34,6 @@ void InferenceManager::addPendingArithLemma(std::unique_ptr<ArithLemma> lemma, { Trace("arith::infman") << "Add " << lemma->d_inference << " " << lemma->d_node << (isWaiting ? " as waiting" : "") << std::endl; - lemma->d_node = Rewriter::rewrite(lemma->d_node); if (hasCachedLemma(lemma->d_node, lemma->d_property)) { return; @@ -110,25 +109,27 @@ std::size_t InferenceManager::numWaitingLemmas() const bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p) { + Node rewritten = Rewriter::rewrite(lem); if (isLemmaPropertyPreprocess(p)) { - return d_lemmasPp.find(lem) != d_lemmasPp.end(); + return d_lemmasPp.find(rewritten) != d_lemmasPp.end(); } - return TheoryInferenceManager::hasCachedLemma(lem, p); + return TheoryInferenceManager::hasCachedLemma(rewritten, p); } bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p) { + Node rewritten = Rewriter::rewrite(lem); if (isLemmaPropertyPreprocess(p)) { - if (d_lemmasPp.find(lem) != d_lemmasPp.end()) + if (d_lemmasPp.find(rewritten) != d_lemmasPp.end()) { return false; } - d_lemmasPp.insert(lem); + d_lemmasPp.insert(rewritten); return true; } - return TheoryInferenceManager::cacheLemma(lem, p); + return TheoryInferenceManager::cacheLemma(rewritten, p); } bool InferenceManager::isEntailedFalse(const ArithLemma& lem) diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 16ccc45ec..83c7d212d 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -287,7 +287,8 @@ TrustNode TheoryInferenceManager::mkLemmaExp(Node conc, bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p) { - return d_lemmasSent.find(lem) != d_lemmasSent.end(); + Node rewritten = Rewriter::rewrite(lem); + return d_lemmasSent.find(rewritten) != d_lemmasSent.end(); } uint32_t TheoryInferenceManager::numSentLemmas() const @@ -445,11 +446,12 @@ bool TheoryInferenceManager::hasSentFact() const bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p) { - if (d_lemmasSent.find(lem) != d_lemmasSent.end()) + Node rewritten = Rewriter::rewrite(lem); + if (d_lemmasSent.find(rewritten) != d_lemmasSent.end()) { return false; } - d_lemmasSent.insert(lem); + d_lemmasSent.insert(rewritten); return true; } |