More fixes for PBE with datatypes (#2882)

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 8833c0cdf26e0eaf984740859920f51800b6524d..7e999d3f592edb99bc73b4fc5fd8ef081c860c0c 100644 (file)
--- 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 083f8df75da1a069bd690fa38c25b7d14babe69c..b5bccae237b34bad0e0aee3703865a437d72133b 100644 (file)
--- 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 (file)
index 0000000..261666d
--- /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)