diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-21 13:41:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-21 13:41:46 -0500 |
commit | 6c8a2652605b031182b3c2c25d237719470f5620 (patch) | |
tree | 0061019093bb4a892625acab3b2996381dc0127b /src/theory/quantifiers | |
parent | 91f9355868d01999fd729544ea50ccd745e84d35 (diff) |
Rewrite selectors correctly applied to constructors (#2875)
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index c9db62735..8833c0cdf 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -641,23 +641,33 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) for (unsigned j = 0, size = itsr->second.size(); j < size; j++) { Node res = itsr->second[j]; - Assert(res.isConst()); + // 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 (eiv.getRole() == enum_io) + // If the result is not constant, then we cannot determine its value + // on this point. In this case, resb remains null. + if (res.isConst()) { - Node out = d_examples_out[j]; - Assert(out.isConst()); - resb = res == out ? d_true : d_false; - } - else - { - resb = res; + if (eiv.getRole() == enum_io) + { + Node out = d_examples_out[j]; + Assert(out.isConst()); + resb = res == out ? d_true : d_false; + } + else + { + resb = res; + } } cond_vals[resb] = true; results.push_back(resb); if (Trace.isOn("sygus-sui-enum")) { - if (resb.getType().isBoolean()) + if (resb.isNull()) + { + Trace("sygus-sui-enum") << "_"; + } + else if (resb.getType().isBoolean()) { Trace("sygus-sui-enum") << (resb == d_true ? "1" : "0"); } |