Rewrite selectors correctly applied to constructors (#2875)

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index a2458e2eb77eb9dcb6e7ce7a544a132bda82ff97..507bbfdd178addcbeee42b62774a084cd182826c 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -32,7 +32,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
   {
     return rewriteConstructor(in);
   }
-  else if (k == kind::APPLY_SELECTOR_TOTAL)
+  else if (k == kind::APPLY_SELECTOR_TOTAL || k == kind::APPLY_SELECTOR)
   {
     return rewriteSelector(in);
   }
@@ -331,6 +331,7 @@ RewriteResponse DatatypesRewriter::rewriteConstructor(TNode in)
 
 RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
 {
+  Kind k = in.getKind();
   if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
   {
     // Have to be careful not to rewrite well-typed expressions
@@ -338,17 +339,40 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
     // e.g. "pred(zero)".
     TypeNode tn = in.getType();
     TypeNode argType = in[0].getType();
-    TNode selector = in.getOperator();
+    Expr selector = in.getOperator().toExpr();
     TNode constructor = in[0].getOperator();
     size_t constructorIndex = indexOf(constructor);
-    const Datatype& dt = Datatype::datatypeOf(selector.toExpr());
+    const Datatype& dt = Datatype::datatypeOf(selector);
     const DatatypeConstructor& c = dt[constructorIndex];
     Trace("datatypes-rewrite-debug") << "Rewriting collapsable selector : "
                                      << in;
     Trace("datatypes-rewrite-debug") << ", cindex = " << constructorIndex
                                      << ", selector is " << selector
                                      << std::endl;
-    int selectorIndex = c.getSelectorIndexInternal(selector.toExpr());
+    // The argument that the selector extracts, or -1 if the selector is
+    // is wrongly applied.
+    int selectorIndex = -1;
+    if (k == kind::APPLY_SELECTOR_TOTAL)
+    {
+      // The argument index of internal selectors is obtained by
+      // getSelectorIndexInternal.
+      selectorIndex = c.getSelectorIndexInternal(selector);
+    }
+    else
+    {
+      // The argument index of external selectors (applications of
+      // APPLY_SELECTOR) is given by an attribute and obtained via indexOf below
+      // The argument is only valid if it is the proper constructor.
+      selectorIndex = Datatype::indexOf(selector);
+      if (selectorIndex < 0 || selectorIndex >= c.getNumArgs())
+      {
+        selectorIndex = -1;
+      }
+      else if (c[selectorIndex].getSelector() != selector)
+      {
+        selectorIndex = -1;
+      }
+    }
     Trace("datatypes-rewrite-debug") << "Internal selector index is "
                                      << selectorIndex << std::endl;
     if (selectorIndex >= 0)
@@ -374,7 +398,7 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
         return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
       }
     }
-    else
+    else if (k == kind::APPLY_SELECTOR_TOTAL)
     {
       Node gt;
       bool useTe = true;

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index c9db6273584176ac4c9f740a7c6bde818e76daf0..8833c0cdf26e0eaf984740859920f51800b6524d 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -641,23 +641,33 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
       for (unsigned j = 0, size = itsr->second.size(); j < size; j++)
       {
         Node res = itsr->second[j];
-        Assert(res.isConst());
+        // The value of this term for this example, or the truth value of
+        // the I/O pair if the role of this enumerator is enum_io.
         Node resb;
-        if (eiv.getRole() == enum_io)
+        // If the result is not constant, then we cannot determine its value
+        // on this point. In this case, resb remains null.
+        if (res.isConst())
         {
-          Node out = d_examples_out[j];
-          Assert(out.isConst());
-          resb = res == out ? d_true : d_false;
-        }
-        else
-        {
-          resb = res;
+          if (eiv.getRole() == enum_io)
+          {
+            Node out = d_examples_out[j];
+            Assert(out.isConst());
+            resb = res == out ? d_true : d_false;
+          }
+          else
+          {
+            resb = res;
+          }
         }
         cond_vals[resb] = true;
         results.push_back(resb);
         if (Trace.isOn("sygus-sui-enum"))
         {
-          if (resb.getType().isBoolean())
+          if (resb.isNull())
+          {
+            Trace("sygus-sui-enum") << "_";
+          }
+          else if (resb.getType().isBoolean())
           {
             Trace("sygus-sui-enum") << (resb == d_true ? "1" : "0");
           }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 21e08f2bfd526f00891ac04eb9208147c3f0bd82..083f8df75da1a069bd690fa38c25b7d14babe69c 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1605,8 +1605,10 @@ set(regress_1_tests
   regress1/sygus/crcy-si-rcons.sy
   regress1/sygus/crcy-si.sy
   regress1/sygus/cube-nia.sy
+  regress1/sygus/double.sy
   regress1/sygus/dt-test-ns.sy
   regress1/sygus/dup-op.sy
+  regress1/sygus/extract.sy
   regress1/sygus/fg_polynomial3.sy
   regress1/sygus/find_sc_bvult_bvnot.sy
   regress1/sygus/hd-01-d1-prog.sy

diff --git a/test/regress/regress1/sygus/double.sy b/test/regress/regress1/sygus/double.sy
new file mode 100644 (file)
index 0000000..f3fea31
--- /dev/null
+++ b/test/regress/regress1/sygus/double.sy
@@ -0,0 +1,26 @@
+; EXPECT: unsat\r
+; COMMAND-LINE: --sygus-out=status\r
+\r
+(set-logic SLIA)\r
+(declare-datatype Ex ((Ex2 (ex Int))))\r
+\r
+(synth-fun double ((x1 Ex)) Int\r
+       (\r
+               (Start Int (ntInt))\r
+               (ntInt Int\r
+                       (\r
+                               (ex ntEx)\r
+                               (+ ntInt ntInt)\r
+                       )\r
+               )\r
+               (ntEx Ex\r
+                       ( \r
+                               x1\r
+                               (Ex2 ntInt)\r
+                       )\r
+               )\r
+       )\r
+)\r
+(constraint (= (double (Ex2 1)) 2))\r
+(constraint (= (double (Ex2 4)) 8))\r
+(check-synth)\r

diff --git a/test/regress/regress1/sygus/extract.sy b/test/regress/regress1/sygus/extract.sy
new file mode 100644 (file)
index 0000000..d1541fa
--- /dev/null
+++ b/test/regress/regress1/sygus/extract.sy
@@ -0,0 +1,19 @@
+; EXPECT: unsat\r
+; COMMAND-LINE: --sygus-out=status\r
+\r
+(set-logic ALL_SUPPORTED)\r
+(declare-datatype Ex ((Ex2 (ex Int))))\r
+\r
+(synth-fun ident ((x1 Ex)) Int\r
+       (\r
+               (Start Int (ntInt))\r
+               (ntInt Int\r
+                       (\r
+                               (ex ntEx)\r
+                       )\r
+               )\r
+               (ntEx Ex ( x1 ) )\r
+       )\r
+)\r
+(constraint (= (ident (Ex2 1)) 1))\r
+(check-synth)\r