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.

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index e22be81e319fe6ab5c96afbeb11b10e1e68ef2a5..e79c12155e8ca1d8e4d4e514c671e15563c39a7c 100644 (file)
--- 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 16ccc45ecb549afcc75db737611f00d330bced56..83c7d212d0b95001e79cf54e30f8a9432b8d49c9 100644 (file)
--- 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;
 }