Fixes for degenerate case of sygus decision tree learning (#4800)

Fixes #4790.

Fixes two bugs in the decision tree learning solver for sygus, one involving evaluation of "templated" enumerators, and one involving ITE strategies where child types are different than the root.

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index ce13b6744d65ebe52d8c3af1177af3afb740ffb6..61916ce4c28e3c3b397c253c84ffd03a9e1e535a 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -47,11 +47,18 @@ bool UnifContextIo::updateContext(SygusUnifIo* sui,
   Assert(d_vals.size() == vals.size());
   bool changed = false;
   Node poln = pol ? d_true : d_false;
-  for (unsigned i = 0; i < vals.size(); i++)
+  for (size_t i = 0, vsize = vals.size(); i < vsize; i++)
   {
-    if (vals[i] != poln)
+    Node v = vals[i];
+    if (v.isNull())
+    {
+      // nothing can be inferred if the evaluation is unknown, e.g. if using
+      // partial functions.
+      continue;
+    }
+    if (v != poln)
     {
-      if (d_vals[i] == d_true)
+      if (v == d_true)
       {
         d_vals[i] = d_false;
         changed = true;
@@ -571,8 +578,6 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   eec->evaluateVec(bv, base_results);
   // get the results for each slave enumerator
   std::map<Node, std::vector<Node>> srmap;
-  Evaluator* ev = d_tds->getEvaluator();
-  bool tryEval = options::sygusEvalOpt();
   for (const Node& xs : ei.d_enum_slave)
   {
     Assert(srmap.find(xs) == srmap.end());
@@ -580,34 +585,15 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
     Node templ = eiv.d_template;
     if (!templ.isNull())
     {
-      TNode templ_var = eiv.d_template_arg;
-      std::vector<Node> args;
-      args.push_back(templ_var);
+      // Substitute and evaluate, notice that the template skeleton may
+      // involve the sygus variables e.g. (>= x _) where x is a sygus
+      // variable, hence we must compute the substituted template before
+      // calling the evaluator.
+      TNode targ = eiv.d_template_arg;
+      TNode tbv = bv;
+      Node stempl = templ.substitute(targ, tbv);
       std::vector<Node> sresults;
-      for (const Node& res : base_results)
-      {
-        TNode tres = res;
-        Node sres;
-        // 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())
-        {
-          std::vector<Node> vals;
-          vals.push_back(tres);
-          if (tryEval)
-          {
-            sres = ev->eval(templ, args, vals);
-          }
-        }
-        if (sres.isNull())
-        {
-          // fall back on rewriter
-          sres = templ.substitute(templ_var, tres);
-          sres = Rewriter::rewrite(sres);
-        }
-        sresults.push_back(sres);
-      }
+      eec->evaluateVec(stempl, sresults);
       srmap[xs] = sresults;
     }
     else
@@ -658,6 +644,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
       std::vector<Node> results;
       std::map<Node, bool> cond_vals;
       std::map<Node, std::vector<Node>>::iterator itsr = srmap.find(xs);
+      Trace("sygus-sui-debug") << " {" << itsr->second << "} ";
       Assert(itsr != srmap.end());
       for (unsigned j = 0, size = itsr->second.size(); j < size; j++)
       {
@@ -1003,6 +990,8 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude(
 
 void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector<Node>& results)
 {
+  Trace("sygus-sui-debug") << "Add enum value " << this << " " << v << " : "
+                           << results << std::endl;
   // should not have been enumerated before
   Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end());
   d_enum_val_to_index[v] = d_enum_vals.size();
@@ -1080,7 +1069,7 @@ Node SygusUnifIo::constructSol(
         {
           ret_dt = constructBestSolvedTerm(e, subsumed_by);
           indent("sygus-sui-dt", ind);
-          Trace("sygus-sui-dt") << "return PBE: success : conditionally solved"
+          Trace("sygus-sui-dt") << "return PBE: success : conditionally solved "
                                 << d_tds->sygusToBuiltin(ret_dt) << std::endl;
         }
         else
@@ -1442,12 +1431,30 @@ Node SygusUnifIo::constructSol(
           }
           else
           {
-            // TODO (#1250) : degenerate case where children have different
-            // types?
-            indent("sygus-sui-dt", ind);
-            Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, "
-                                      "cannot find a distinguishable condition"
-                                  << std::endl;
+            // if the child types are different, it could still make a
+            // difference to recurse, for instance see issue #4790.
+            bool childTypesEqual = ce.getType() == etn;
+            if (!childTypesEqual)
+            {
+              if (!ecache_child.d_enum_vals.empty())
+              {
+                // take arbitrary
+                rec_c = constructBestConditional(ce, ecache_child.d_enum_vals);
+                indent("sygus-sui-dt", ind);
+                Trace("sygus-sui-dt")
+                    << "PBE: ITE strategy : choose arbitrary conditional due "
+                       "to disequal child types "
+                    << d_tds->sygusToBuiltin(rec_c) << std::endl;
+              }
+            }
+            if (rec_c.isNull())
+            {
+              indent("sygus-sui-dt", ind);
+              Trace("sygus-sui-dt")
+                  << "return PBE: failed ITE strategy, "
+                     "cannot find a distinguishable condition, childTypesEqual="
+                  << childTypesEqual << std::endl;
+            }
           }
           if (!rec_c.isNull())
           {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0b0da8e93a15954d4a7fcba7b24db5cd5917e059..a21b76b0cd37c8c70cdab167a6376f3ec21d6d27 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1043,6 +1043,7 @@ set(regress_0_tests
   regress0/sygus/issue3624.sy
   regress0/sygus/issue3645-grammar-sets.smt2
   regress0/sygus/issue4383-cache-fv-id.sy
+  regress0/sygus/issue4790-dtd.sy
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
   regress0/sygus/no-logic.sy

diff --git a/test/regress/regress0/sygus/issue4790-dtd.sy b/test/regress/regress0/sygus/issue4790-dtd.sy
new file mode 100644 (file)
index 0000000..55f4723
--- /dev/null
+++ b/test/regress/regress0/sygus/issue4790-dtd.sy
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic NIA)
+(synth-fun patternGen ((i Int)) Int
+((ITE Int) (CONST Int) (I Int)  (B Bool))
+( (ITE Int (
+    (ite (<= i CONST) I I)
+    
+  ))
+  (CONST Int (0))
+  (I Int (i 1
+    (+ I I) (- I I) (* I I)
+  ))
+  (B Bool (
+    (<= I I)
+  ))
+)
+)
+(declare-var i Int)
+(constraint (= (patternGen 0) 1))
+(constraint (= (patternGen 1) 1))
+(constraint (= (patternGen 2) 1))
+(check-synth)