From: Gereon Kremer <gkremer@stanford.edu>
Date: Thu, 17 Dec 2020 16:28:10 +0000 (+0100)
Subject: Always consider rewritten lemmas for caching. (#5696)
X-Git-Tag: cvc5-1.0.0~2427
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=db157ade422c4bc16750d2cb6db7643f1fd3dad6;p=cvc5.git

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 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;
 }