Fixes for SyGuS PBE + templated string concatenations + datatypes (#3492)

3 files changed, 20 insertions, 5 deletions

diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index 5c0e9b944..ce19a1f67 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -88,6 +88,9 @@ class Evaluator
    * `args` and the corresponding values `vals`. The function returns a null
    * node if there is a subterm that is not constant under the substitution or
    * if an operator is not supported by the evaluator.
+   *
+   * The nodes in the vals must be constant values, that is, they must return
+   * true for isConst().
    */
   Node eval(TNode n,
             const std::vector<Node>& args,
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 72091c0cf..d423b1777 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -594,12 +594,18 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
       for (const Node& res : base_results)
       {
         TNode tres = res;
-        std::vector<Node> vals;
-        vals.push_back(tres);
         Node sres;
-        if (tryEval)
+        // It may not be constant, e.g. if we involve a partial operator
+        // like datatype selectors. In this case, we avoid using the evaluator,
+        // which expects a constant substitution.
+        if (tres.isConst())
         {
-          sres = ev->eval(templ, args, vals);
+          std::vector<Node> vals;
+          vals.push_back(tres);
+          if (tryEval)
+          {
+            sres = ev->eval(templ, args, vals);
+          }
         }
         if (sres.isNull())
         {
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 07997221f..f87b906e1 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -101,6 +101,8 @@ void SygusUnifStrategy::initialize(QuantifiersEngine* qe,
 
 void SygusUnifStrategy::initializeType(TypeNode tn)
 {
+  Trace("sygus-unif") << "SygusUnifStrategy: initialize : " << tn << " for "
+                      << d_candidate << std::endl;
   d_tinfo[tn].d_this_type = tn;
 }
 
@@ -123,6 +125,8 @@ EnumInfo& SygusUnifStrategy::getEnumInfo(Node e)
 
 EnumTypeInfo& SygusUnifStrategy::getEnumTypeInfo(TypeNode tn)
 {
+  Trace("sygus-unif") << "SygusUnifStrategy: get : " << tn << " for "
+                      << d_candidate << std::endl;
   std::map<TypeNode, EnumTypeInfo>::iterator it = d_tinfo.find(tn);
   Assert(it != d_tinfo.end());
   return it->second;
@@ -567,6 +571,9 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
           EnumRole erole_c = getEnumeratorRoleForNodeRole(nrole_c);
           // make the enumerator
           Node et;
+          // Build the strategy recursively, regardless of whether the
+          // enumerator is templated.
+          buildStrategyGraph(ct, nrole_c);
           if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end())
           {
             // it is templated, allocate a fresh variable
@@ -591,7 +598,6 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
                 << "...child type enumerate "
                 << ((DatatypeType)ct.toType()).getDatatype().getName()
                 << ", node role = " << nrole_c << std::endl;
-            buildStrategyGraph(ct, nrole_c);
             // otherwise use the previous
             Assert(d_tinfo[ct].d_enum.find(erole_c)
                    != d_tinfo[ct].d_enum.end());