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 a2507d6cf15385cad2bee01dea1d446e4b7f4745..595dd16c33d791abb659e1e386073cdbb07bf371 100644 (file)
--- 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 30bb4bad0cab79f1ec0fb26b7819a352eaf37636..d6eec382197a29eab72ea23ee379fcef69d5180f 100644 (file)
--- 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;