From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Aug 2020 19:15:17 +0000 (-0500)
Subject: Fixes for corner case of decision tree learning with different types (#4887)
X-Git-Tag: cvc5-1.0.0~3005
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ddf6526f9f3ac2410849fbf8ebf0eac09ff2a28a;p=cvc5.git

Fixes for corner case of decision tree learning with different types (#4887)

There was a last minute change was a typo when merging 103b5ea .
Also the fix in that commit needed to be slightly more robust to the case when either branch of an ITE had a different sygus type.

Fixes regress1.
---

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 61916ce4c..e330a8476 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -58,7 +58,7 @@ bool UnifContextIo::updateContext(SygusUnifIo* sui,
     }
     if (v != poln)
     {
-      if (v == d_true)
+      if (d_vals[i] == d_true)
       {
         d_vals[i] = d_false;
         changed = true;
@@ -1431,9 +1431,12 @@ Node SygusUnifIo::constructSol(
           }
           else
           {
-            // if the child types are different, it could still make a
-            // difference to recurse, for instance see issue #4790.
-            bool childTypesEqual = ce.getType() == etn;
+            // if the branch types are different, it could still make a
+            // difference to recurse, for instance see issue #4790. We do this
+            // if either branch is a different type from the current type.
+            TypeNode branchType1 = etis->d_cenum[1].first.getType();
+            TypeNode branchType2 = etis->d_cenum[2].first.getType();
+            bool childTypesEqual = branchType1 == etn && branchType2 == etn;
             if (!childTypesEqual)
             {
               if (!ecache_child.d_enum_vals.empty())