From ddf6526f9f3ac2410849fbf8ebf0eac09ff2a28a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 13 Aug 2020 14:15:17 -0500 Subject: [PATCH] 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. --- src/theory/quantifiers/sygus/sygus_unif_io.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) 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()) -- 2.30.2