From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 Apr 2020 05:52:33 +0000 (-0500)
Subject: Always flush lemmas from downwards closure in sets (#4297)
X-Git-Tag: cvc5-1.0.0~3369
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=617f1b0fe93e077d6e76e03dcf1a75730740fe27;p=cvc5.git

Always flush lemmas from downwards closure in sets (#4297)

Fixes #4283.

This also makes a few minor improvements to how lemmas are sent in sets. In particular, lemmas are not sent if we are already in conflict.
---

diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index a2507d6cf..595dd16c3 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -189,15 +189,22 @@ void InferenceManager::split(Node n, int reqPol)
 }
 void InferenceManager::flushLemmas(std::vector<Node>& lemmas, bool preprocess)
 {
-  for (const Node& l : lemmas)
+  if (!d_state.isInConflict())
   {
-    flushLemma(l, preprocess);
+    for (const Node& l : lemmas)
+    {
+      flushLemma(l, preprocess);
+    }
   }
   lemmas.clear();
 }
 
 void InferenceManager::flushLemma(Node lem, bool preprocess)
 {
+  if (d_state.isInConflict())
+  {
+    return;
+  }
   if (d_lemmas_produced.find(lem) != d_lemmas_produced.end())
   {
     Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
@@ -211,11 +218,7 @@ void InferenceManager::flushLemma(Node lem, bool preprocess)
 
 void InferenceManager::flushPendingLemmas(bool preprocess)
 {
-  for (const Node& l : d_pendingLemmas)
-  {
-    flushLemma(l, preprocess);
-  }
-  d_pendingLemmas.clear();
+  flushLemmas(d_pendingLemmas, preprocess);
 }
 
 bool InferenceManager::hasLemmaCached(Node lem) const
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 30bb4bad0..d6eec3821 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -514,10 +514,7 @@ void TheorySetsPrivate::fullEffortCheck()
     }
     // check downwards closure
     checkDownwardsClosure();
-    if (options::setsInferAsLemmas())
-    {
-      d_im.flushPendingLemmas();
-    }
+    d_im.flushPendingLemmas();
     if (d_im.hasProcessed())
     {
       continue;