diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-13 14:15:17 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-13 14:15:17 -0500 |
commit | ddf6526f9f3ac2410849fbf8ebf0eac09ff2a28a (patch) | |
tree | fa6355c317248c1e8ac1601f98533fb1d95c4f6b /src/theory/quantifiers | |
parent | fb2a0d9aa09aa21f465aa8d62eab8492610052c3 (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 11 |
1 files 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()) |