Fix fairness issue with fast sygus enumerator (#2873)

1 files changed, 23 insertions, 1 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 9981b5141..fb16e274f 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -476,6 +476,13 @@ bool SygusEnumerator::TermEnumSlave::validateIndex()
   {
     Assert(d_index == tc.getNumTerms());
     Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n";
+    // if the size of the master is larger than the size limit, then
+    // there is no use continuing, since there are no more terms that this
+    // slave enumerator can return.
+    if (d_master->getCurrentSize() > d_sizeLim)
+    {
+      return false;
+    }
     // must push the master index
     if (!d_master->increment())
     {
@@ -655,9 +662,14 @@ bool SygusEnumerator::TermEnumMaster::increment()
   {
     return false;
   }
+  Trace("sygus-enum-summary") << "SygusEnumerator::TermEnumMaster: increment "
+                              << d_tn << "..." << std::endl;
   d_isIncrementing = true;
   bool ret = incrementInternal();
   d_isIncrementing = false;
+  Trace("sygus-enum-summary")
+      << "SygusEnumerator::TermEnumMaster: finished increment " << d_tn
+      << std::endl;
   return ret;
 }
 
@@ -789,7 +801,15 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal()
 
     // restart with constructor class one (skip nullary constructors)
     d_consClassNum = 1;
-    return incrementInternal();
+
+    // We break for a round: return the null term when we cross a size
+    // boundary. This ensures that the necessary breaks are taken, e.g.
+    // in slave enumerators who may instead want to abandon this call to
+    // increment master when the size of the master makes their increment
+    // infeasible.
+    d_currTermSet = true;
+    d_currTerm = Node::null();
+    return true;
   }
 
   bool incSuccess = false;
@@ -819,6 +839,8 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal()
           // the term was not unique based on rewriting
           Trace("sygus-enum-debug2") << "master(" << d_tn
                                      << "): failed addTerm\n";
+          // we will return null (d_currTermSet is true at this point)
+          Assert(d_currTermSet);
           d_currTerm = Node::null();
         }
       }