Fix combination of datatypes + strings in PBE (#2930)

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 47fd41300be1420d4d36777c0b135562ffac2bc0..7d51ec43a0e0d6c2f46037ee215b4c866a4cf212 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -161,7 +161,12 @@ bool UnifContextIo::getStringIncrement(SygusUnifIo* sui,
     if (d_vals[j] == sui->d_true)
     {
       // example is active in this context
-      Assert(vals[j].isConst());
+      if (!vals[j].isConst())
+      {
+        // the value is unknown, thus we cannot use it to increment the strings
+        // position
+        return false;
+      }
       String mystr = vals[j].getConst<String>();
       ival = mystr.size();
       if (mystr.size() <= ex_vals[j].size())
@@ -199,7 +204,11 @@ bool UnifContextIo::isStringSolved(SygusUnifIo* sui,
     if (d_vals[j] == sui->d_true)
     {
       // example is active in this context
-      Assert(vals[j].isConst());
+      if (!vals[j].isConst())
+      {
+        // value is unknown, thus it does not solve
+        return false;
+      }
       String mystr = vals[j].getConst<String>();
       if (ex_vals[j] != mystr)
       {
@@ -949,23 +958,27 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude(
     std::vector<unsigned> cmp_indices;
     for (unsigned i = 0, size = results.size(); i < size; i++)
     {
-      Assert(results[i].isConst());
-      Assert(d_examples_out[i].isConst());
-      Trace("sygus-sui-cterm-debug")
-          << "  " << results[i] << " <> " << d_examples_out[i];
-      Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]);
-      Node contr = Rewriter::rewrite(cont);
-      if (contr == d_false)
+      // If the result is not constant, then it is worthless. It does not
+      // impact whether the term is excluded.
+      if (results[i].isConst())
       {
-        cmp_indices.push_back(i);
-        Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl;
-      }
-      else
-      {
-        Trace("sygus-sui-cterm-debug") << "...contained." << std::endl;
-        if (isConditional)
+        Assert(d_examples_out[i].isConst());
+        Trace("sygus-sui-cterm-debug")
+            << "  " << results[i] << " <> " << d_examples_out[i];
+        Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]);
+        Node contr = Rewriter::rewrite(cont);
+        if (contr == d_false)
         {
-          return false;
+          cmp_indices.push_back(i);
+          Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl;
+        }
+        else
+        {
+          Trace("sygus-sui-cterm-debug") << "...contained." << std::endl;
+          if (isConditional)
+          {
+            return false;
+          }
         }
       }
     }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 13d1540f66b65ce191b0fbaac47e12422152cd62..a9b807e82533f3a9c336c742e51b45b67d7b8f85 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1624,6 +1624,7 @@ set(regress_1_tests
   regress1/sygus/inv-example.sy
   regress1/sygus/inv-missed-sol-true.sy
   regress1/sygus/inv-unused.sy
+  regress1/sygus/issue2914.sy
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy

diff --git a/test/regress/regress1/sygus/issue2914.sy b/test/regress/regress1/sygus/issue2914.sy
new file mode 100644 (file)
index 0000000..0f125a8
--- /dev/null
+++ b/test/regress/regress1/sygus/issue2914.sy
@@ -0,0 +1,26 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic SLIA)
+(declare-datatype JSIdentifier ((JSString (jsString String)) (Error )))
+
+(synth-fun substring ((x1 String) (x3 Int))String
+       ((Start String (ntString))
+               (ntInt Int
+                       (0 x3)
+               )
+               (ntJSIdentifier JSIdentifier
+                       ( 
+                               Error
+                       )
+               )
+               (ntString String
+                       (x1
+                               (str.substr ntString ntInt ntInt)
+                               (jsString ntJSIdentifier)
+                               (str.++ ntString ntString)
+                       )
+               )
+       )
+)
+(constraint (= (substring "ey" 1) "e"))
+(check-synth)