sygusComp2018: pbe multi-enumerator fairness option (#2178)

1 files changed, 23 insertions, 6 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 3eace0e89..1a8721530 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -410,19 +410,36 @@ bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums,
   Assert( enums.size()==enum_values.size() );
   if( !enums.empty() ){
     unsigned min_term_size = 0;
-    std::vector< unsigned > enum_consider;
     Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl;
-    for( unsigned i=0; i<enums.size(); i++ ){
-      Trace("sygus-pbe-enum") << "  " << enums[i] << " -> " << enum_values[i] << std::endl;
+    std::vector<unsigned> szs;
+    for (unsigned i = 0, esize = enums.size(); i < esize; i++)
+    {
+      Trace("sygus-pbe-enum") << "  " << enums[i] << " -> ";
+      TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]);
+      Trace("sygus-pbe-enum") << std::endl;
       unsigned sz = d_tds->getSygusTermSize( enum_values[i] );
+      szs.push_back(sz);
       if( i==0 || sz<min_term_size ){
-        enum_consider.clear();
         min_term_size = sz;
-        enum_consider.push_back( i );
-      }else if( sz==min_term_size ){
+      }
+    }
+    // Assume two enumerators of types T1 and T2.
+    // If options::sygusPbeMultiFair() is true,
+    // we ensure that all values of type T1 and size n are enumerated before
+    // any term of type T2 of size n+d, and vice versa, where d is
+    // set by options::sygusPbeMultiFairDiff(). If d is zero, then our
+    // enumeration is such that all terms of T1 or T2 of size n are considered
+    // before any term of size n+1.
+    std::vector<unsigned> enum_consider;
+    for (unsigned i = 0, esize = enums.size(); i < esize; i++)
+    {
+      if (!options::sygusPbeMultiFair()
+          || szs[i] - min_term_size <= options::sygusPbeMultiFairDiff())
+      {
         enum_consider.push_back( i );
       }
     }
+
     // only consider the enumerators that are at minimum size (for fairness)
     Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl;
     NodeManager* nm = NodeManager::currentNM();