Towards better symbolic enumeration in SyGuS (#1971)

2 files changed, 9 insertions, 6 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index d4a21ea2f..f9a434453 100644
--- 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 126f01136..121ee34f7 100644
--- 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)