Rewrite selectors correctly applied to constructors (#2875)

5 files changed, 96 insertions, 15 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index a2458e2eb..507bbfdd1 100644
--- 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 c9db62735..8833c0cdf 100644
--- 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 21e08f2bf..083f8df75 100644
--- 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
index 000000000..f3fea3122
--- /dev/null
+++ b/test/regress/regress1/sygus/double.sy
@@ -0,0 +1,26 @@
+; EXPECT: unsat

+; COMMAND-LINE: --sygus-out=status

+

+(set-logic SLIA)

+(declare-datatype Ex ((Ex2 (ex Int))))

+

+(synth-fun double ((x1 Ex)) Int

+	(

+		(Start Int (ntInt))

+		(ntInt Int

+			(

+				(ex ntEx)

+				(+ ntInt ntInt)

+			)

+		)

+		(ntEx Ex

+			( 

+				x1

+				(Ex2 ntInt)

+			)

+		)

+	)

+)

+(constraint (= (double (Ex2 1)) 2))

+(constraint (= (double (Ex2 4)) 8))

+(check-synth)

diff --git a/test/regress/regress1/sygus/extract.sy b/test/regress/regress1/sygus/extract.sy
new file mode 100644
index 000000000..d1541fa87
--- /dev/null
+++ b/test/regress/regress1/sygus/extract.sy
@@ -0,0 +1,19 @@
+; EXPECT: unsat

+; COMMAND-LINE: --sygus-out=status

+

+(set-logic ALL_SUPPORTED)

+(declare-datatype Ex ((Ex2 (ex Int))))

+

+(synth-fun ident ((x1 Ex)) Int

+	(

+		(Start Int (ntInt))

+		(ntInt Int

+			(

+				(ex ntEx)

+ 			)

+		)

+		(ntEx Ex ( x1 ) )

+	)

+)

+(constraint (= (ident (Ex2 1)) 1))

+(check-synth)