Towards better symbolic enumeration in SyGuS (#1971)

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index d4a21ea2f3c99c912fb1f2c17091e9e75b3d6c0b..f9a434453a03ee5ff089a6cc3cbd2b524fd42752 100644 (file)
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -594,8 +594,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned
           // if this type admits any constant, then at least one of my children
           // must not be the "any constant" constructor
           unsigned dt_index_nargs = dt[tindex].getNumArgs();
-          int tn_ac = d_tds->getAnyConstantConsNum(tn);
-          if (tn_ac != -1 && dt_index_nargs > 0)
+          if (dt.getSygusAllowConst() && dt_index_nargs > 0)
           {
             std::vector<Node> exp_all_anyc;
             bool success = true;

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 126f011368d6ec5dfc39c34427d04c7e26ba16cd..121ee34f727af922482ec3c01124831872100ae9 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -341,8 +341,10 @@ public:
     }
     return true;
   }
-  bool empty() {
-    return d_req_kind==UNDEFINED_KIND && d_req_const.isNull() && d_req_type.isNull();
+  bool empty()
+  {
+    return d_req_kind == UNDEFINED_KIND && d_req_const.isNull()
+           && d_req_type.isNull() && d_children.empty();
   }
 };
 
@@ -610,10 +612,12 @@ bool TermDbSygus::considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind
     }else if( pk==ITE ){
       if( arg==0 ){
         if( c==max_c ){
-          rt.d_children[2].d_req_type = tnp;
-        }else if( c==zero_c ){
           rt.d_children[1].d_req_type = tnp;
         }
+        else if (c == zero_c)
+        {
+          rt.d_children[2].d_req_type = tnp;
+        }
       }
     }else if( pk==STRING_SUBSTR ){
       if (c == one_c && arg == 2)