Minor refactor for theory of sets (#3924)

Flattens a block of code and refactors the main check loop, will make it easier to incorporate new extensions.

It also avoids a needless call to check() for Relations when there are no relations constraints.

1 files changed, 69 insertions, 50 deletions

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 866c80863..b949be76c 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -373,6 +373,8 @@ void TheorySetsPrivate::fullEffortCheck()
   Trace("sets") << "----- Full effort check ------" << std::endl;
   do
   {
+    Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
+
     Trace("sets") << "...iterate full effort check..." << std::endl;
     fullEffortReset();
 
@@ -476,71 +478,88 @@ void TheorySetsPrivate::fullEffortCheck()
 
     // We may have sent lemmas while registering the terms in the loop above,
     // e.g. the cardinality solver.
-    if (!d_im.hasProcessed())
+    if (d_im.hasProcessed())
     {
-      if (Trace.isOn("sets-mem"))
+      continue;
+    }
+    if (Trace.isOn("sets-mem"))
+    {
+      const std::vector<Node>& sec = d_state.getSetsEqClasses();
+      for (const Node& s : sec)
       {
-        const std::vector<Node>& sec = d_state.getSetsEqClasses();
-        for (const Node& s : sec)
+        Trace("sets-mem") << "Eqc " << s << " : ";
+        const std::map<Node, Node>& smem = d_state.getMembers(s);
+        if (!smem.empty())
         {
-          Trace("sets-mem") << "Eqc " << s << " : ";
-          const std::map<Node, Node>& smem = d_state.getMembers(s);
-          if (!smem.empty())
-          {
-            Trace("sets-mem") << "Memberships : ";
-            for (const std::pair<const Node, Node>& it2 : smem)
-            {
-              Trace("sets-mem") << it2.first << " ";
-            }
-          }
-          Node ss = d_state.getSingletonEqClass(s);
-          if (!ss.isNull())
+          Trace("sets-mem") << "Memberships : ";
+          for (const std::pair<const Node, Node>& it2 : smem)
           {
-            Trace("sets-mem") << " : Singleton : " << ss;
+            Trace("sets-mem") << it2.first << " ";
           }
-          Trace("sets-mem") << std::endl;
         }
-      }
-      checkSubtypes();
-      d_im.flushPendingLemmas(true);
-      if (!d_im.hasProcessed())
-      {
-        checkDownwardsClosure();
-        if (options::setsInferAsLemmas())
+        Node ss = d_state.getSingletonEqClass(s);
+        if (!ss.isNull())
         {
-          d_im.flushPendingLemmas();
-        }
-        if (!d_im.hasProcessed())
-        {
-          checkUpwardsClosure();
-          d_im.flushPendingLemmas();
-          if (!d_im.hasProcessed())
-          {
-            checkDisequalities();
-            d_im.flushPendingLemmas();
-            if (!d_im.hasProcessed())
-            {
-              checkReduceComprehensions();
-              d_im.flushPendingLemmas();
-
-              if (!d_im.hasProcessed() && d_card_enabled)
-              {
-                // call the check method of the cardinality solver
-                d_cardSolver->check();
-              }
-            }
-          }
+          Trace("sets-mem") << " : Singleton : " << ss;
         }
+        Trace("sets-mem") << std::endl;
+      }
+    }
+    // check subtypes
+    checkSubtypes();
+    d_im.flushPendingLemmas(true);
+    if (d_im.hasProcessed())
+    {
+      continue;
+    }
+    // check downwards closure
+    checkDownwardsClosure();
+    if (options::setsInferAsLemmas())
+    {
+      d_im.flushPendingLemmas();
+    }
+    if (d_im.hasProcessed())
+    {
+      continue;
+    }
+    // check upwards closure
+    checkUpwardsClosure();
+    d_im.flushPendingLemmas();
+    if (d_im.hasProcessed())
+    {
+      continue;
+    }
+    // check disequalities
+    checkDisequalities();
+    d_im.flushPendingLemmas();
+    if (d_im.hasProcessed())
+    {
+      continue;
+    }
+    // check reduce comprehensions
+    checkReduceComprehensions();
+    d_im.flushPendingLemmas();
+    if (d_im.hasProcessed())
+    {
+      continue;
+    }
+    if (d_card_enabled)
+    {
+      // call the check method of the cardinality solver
+      d_cardSolver->check();
+      if (d_im.hasProcessed())
+      {
+        continue;
       }
     }
-    if (!d_im.hasProcessed())
+    if (d_rels_enabled)
     {
-      // invoke relations solver
+      // call the check method of the relations solver
       d_rels->check(Theory::EFFORT_FULL);
     }
-    Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
   } while (!d_im.hasSentLemma() && !d_state.isInConflict()
            && d_im.hasAddedFact());
+  Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
   Trace("sets") << "----- End full effort check, conflict="
                 << d_state.isInConflict() << ", lemma=" << d_im.hasSentLemma()
                 << std::endl;