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

3 files changed, 45 insertions, 14 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index bf514ada7..fa8f07dac 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1076,6 +1076,22 @@ header = "options/quantifiers_options.h"
   help       = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
 
 [[option]]
+  name       = "sygusPbeMultiFair"
+  category   = "regular"
+  long       = "sygus-pbe-multi-fair"
+  type       = "bool"
+  default    = "true"
+  help       = "when using multiple enumerators, ensure that we only register value of minimial term size"
+
+[[option]]
+  name       = "sygusPbeMultiFairDiff"
+  category   = "regular"
+  long       = "sygus-pbe-multi-fair-diff=N"
+  type       = "int"
+  default    = "0"
+  help       = "when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)"
+
+[[option]]
   name       = "sygusEvalUnfold"
   category   = "regular"
   long       = "sygus-eval-unfold"
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index c9b3a17f4..49132dc46 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -383,9 +383,8 @@ Node SygusSymBreakNew::getRelevancyCondition( Node n ) {
         }
         Assert( !disj.empty() );
         if( excl ){
-          cond = disj.size() == 1
-                     ? disj[0]
-                     : NodeManager::currentNM()->mkNode(kind::AND, disj);
+          cond = disj.size() == 1 ? disj[0] : NodeManager::currentNM()->mkNode(
+                                                  kind::AND, disj);
         }
       }else{
         int sindex = Datatype::cindexOf( selExpr );
@@ -802,8 +801,8 @@ Node SygusSymBreakNew::registerSearchValue(
     Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end());
     quantifiers::CegConjecture* aconj = d_anchor_to_conj[a];
     Assert(aconj != NULL);
-    Trace("sygus-sb-debug")
-        << "  ...register search value " << cnv << ", type=" << tn << std::endl;
+    Trace("sygus-sb-debug") << "  ...register search value " << cnv
+                            << ", type=" << tn << std::endl;
     Node bv = d_tds->sygusToBuiltin(cnv, tn);
     Trace("sygus-sb-debug") << "  ......builtin is " << bv << std::endl;
     Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv);
@@ -812,8 +811,8 @@ Node SygusSymBreakNew::registerSearchValue(
     unsigned sz = d_tds->getSygusTermSize( nv );      
     if( d_tds->involvesDivByZero( bvr ) ){
       quantifiers::DivByZeroSygusInvarianceTest dbzet;
-      Trace("sygus-sb-mexp-debug")
-          << "Minimize explanation for div-by-zero in " << bv << std::endl;
+      Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in "
+                                   << bv << std::endl;
       registerSymBreakLemmaForValue(
           a, nv, dbzet, Node::null(), var_count, lemmas);
       return Node::null();
@@ -1055,7 +1054,6 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No
   Trace("sygus-sb-debug2") << "...finished." << std::endl;
 }
 
-
 void SygusSymBreakNew::preRegisterTerm( TNode n, std::vector< Node >& lemmas  ) {
   if( n.isVar() ){
     Trace("sygus-sb-debug") << "Pre-register variable : " << n << std::endl;
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();