From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 23 May 2018 23:18:51 +0000 (-0500)
Subject: Towards better symbolic enumeration in SyGuS (#1971)
X-Git-Tag: cvc5-1.0.0~5017
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=55fd4152498a87aed3ddf220c91e3fc2f560e281;p=cvc5.git

Towards better symbolic enumeration in SyGuS (#1971)
---

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)