More fixes for PBE with datatypes (#2882)

1 files changed, 38 insertions, 16 deletions

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 : "