From d5ad777c539f5a49e1cdf4e483c2d5d689738b12 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 22 Mar 2019 09:01:13 -0500
Subject: [PATCH] More fixes for PBE with datatypes (#2882)

---
 .../quantifiers/sygus/sygus_unif_io.cpp       | 54 +++++++++++++------
 test/regress/CMakeLists.txt                   |  1 +
 test/regress/regress1/sygus/tester.sy         | 37 +++++++++++++
 3 files changed, 76 insertions(+), 16 deletions(-)
 create mode 100644 test/regress/regress1/sygus/tester.sy

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 8833c0cdf..7e999d3f5 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -448,20 +448,33 @@ void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals,
          ++it)
     {
       int new_status = status;
-      // if the current value is true
+      bool success = true;
+      // if the current value is true, we must consider the value of this child
       if (curr_val_true)
       {
         if (status != 0)
         {
-          Assert(it->first.isConst() && it->first.getType().isBoolean());
-          new_status = (it->first.getConst<bool>() ? 1 : -1);
-          if (status != -2 && new_status != status)
+          if (it->first.isNull())
+          {
+            // The value of this child is unknown on this point, hence we
+            // ignore it.
+            success = false;
+          }
+          else
           {
-            new_status = 0;
+            Assert(it->first.getType().isBoolean());
+            new_status = (it->first.getConst<bool>() ? 1 : -1);
+            if (status != -2 && new_status != status)
+            {
+              new_status = 0;
+            }
           }
         }
       }
-      it->second.getLeavesInternal(vals, pol, v, index + 1, new_status);
+      if (success)
+      {
+        it->second.getLeavesInternal(vals, pol, v, index + 1, new_status);
+      }
     }
   }
 }
@@ -644,17 +657,25 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
         // 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 the result is not constant, then we cannot determine its value
-        // on this point. In this case, resb remains null.
-        if (res.isConst())
+        if (eiv.getRole() == enum_io)
         {
-          if (eiv.getRole() == enum_io)
-          {
-            Node out = d_examples_out[j];
-            Assert(out.isConst());
-            resb = res == out ? d_true : d_false;
-          }
-          else
+          Node out = d_examples_out[j];
+          Assert(out.isConst());
+          // If the result is not constant, then we assume that it does
+          // not satisfy the example. This is a safe underapproximation
+          // of the good behavior of the current term, that is, we only
+          // produce solutions whose values are fully evaluatable on all input
+          // points. Notice that terms may be used as leaves of decision
+          // trees that are fully evaluatable on points in that branch, but
+          // are not evaluatable on others, e.g. (head x) in the solution:
+          //   (ite ((_ is cons) x) (head x) 5)
+          resb = (res.isConst() && res == out) ? d_true : d_false;
+        }
+        else
+        {
+          // We only set resb if it is constant, otherwise it remains null.
+          // This indicates its value cannot be determined.
+          if (res.isConst())
           {
             resb = res;
           }
@@ -687,6 +708,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
           std::vector<Node> subsume;
           if (cond_vals.find(d_false) == cond_vals.end())
           {
+            Assert(cond_vals.size() == 1);
             // it is the entire solution, we are done
             Trace("sygus-sui-enum")
                 << "  ...success, full solution added to PBE pool : "
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 083f8df75..b5bccae23 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1656,6 +1656,7 @@ set(regress_1_tests
   regress1/sygus/sygus-uf-ex.sy
   regress1/sygus/t8.sy
   regress1/sygus/temp_input_to_synth_ic-error-121418.sy
+  regress1/sygus/tester.sy
   regress1/sygus/tl-type-0.sy
   regress1/sygus/tl-type-4x.sy
   regress1/sygus/tl-type.sy
diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy
new file mode 100644
index 000000000..261666dd4
--- /dev/null
+++ b/test/regress/regress1/sygus/tester.sy
@@ -0,0 +1,37 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic SLIA)
+(declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool))))
+
+(define-fun isA ((i DT)) Bool ((_ is A) i) )
+(define-fun isB ((i DT)) Bool ((_ is B) i) )
+
+(synth-fun add ((x1 DT)) DT
+	(
+		(Start DT (ntDT))
+		(ntDT DT
+			( x1 x2
+				(JSBool ntBool)
+				(A ntInt)
+				(ite ntBool ntDT ntDT)
+			)
+		)
+		(ntBool Bool
+			(
+				(isA ntDT)
+				(isB ntDT)
+				(jsBool ntDT)
+			)
+		)
+		(ntInt Int
+			(1
+				(a ntDT)
+				(+ ntInt ntInt)
+			)
+		)
+	)
+)
+(constraint (= (add (A 6)) (A 7)))
+(constraint (= (add (B "j")) (B "j")))
+(check-synth)
-- 
2.30.2