Fix fairness issue with fast sygus enumerator (#2873)

3 files changed, 51 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();
         }
       }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fb0e358e2..0b4a4bdc7 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1603,6 +1603,7 @@ set(regress_1_tests
   regress1/sygus/crci-ssb-unk.sy
   regress1/sygus/crcy-si-rcons.sy
   regress1/sygus/crcy-si.sy
+  regress1/sygus/cube-nia.sy
   regress1/sygus/dt-test-ns.sy
   regress1/sygus/dup-op.sy
   regress1/sygus/fg_polynomial3.sy
diff --git a/test/regress/regress1/sygus/cube-nia.sy b/test/regress/regress1/sygus/cube-nia.sy
new file mode 100644
index 000000000..da7d98e66
--- /dev/null
+++ b/test/regress/regress1/sygus/cube-nia.sy
@@ -0,0 +1,27 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic NIA)
+
+(synth-fun cube ((x Int)) Int
+  (
+    (Start Int (ntInt))
+  
+    (ntBool Bool
+      ( 
+        (> ntInt ntInt)
+        (= ntInt ntInt)
+      )
+    )
+    (ntInt Int
+      (1 x
+        (* ntInt ntInt)
+        (ite ntBool ntInt ntInt)
+      )
+    )
+  )
+)
+
+(constraint (= (cube 1) 1))
+(constraint (= (cube 2) 8))
+(check-synth)