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 | |
parent | 91f9355868d01999fd729544ea50ccd745e84d35 (diff) |
Rewrite selectors correctly applied to constructors (#2875)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.cpp | 34 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 30 |
2 files changed, 49 insertions, 15 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index a2458e2eb..507bbfdd1 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -32,7 +32,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) { return rewriteConstructor(in); } - else if (k == kind::APPLY_SELECTOR_TOTAL) + else if (k == kind::APPLY_SELECTOR_TOTAL || k == kind::APPLY_SELECTOR) { return rewriteSelector(in); } @@ -331,6 +331,7 @@ RewriteResponse DatatypesRewriter::rewriteConstructor(TNode in) RewriteResponse DatatypesRewriter::rewriteSelector(TNode in) { + Kind k = in.getKind(); if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions @@ -338,17 +339,40 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in) // e.g. "pred(zero)". TypeNode tn = in.getType(); TypeNode argType = in[0].getType(); - TNode selector = in.getOperator(); + Expr selector = in.getOperator().toExpr(); TNode constructor = in[0].getOperator(); size_t constructorIndex = indexOf(constructor); - const Datatype& dt = Datatype::datatypeOf(selector.toExpr()); + const Datatype& dt = Datatype::datatypeOf(selector); const DatatypeConstructor& c = dt[constructorIndex]; Trace("datatypes-rewrite-debug") << "Rewriting collapsable selector : " << in; Trace("datatypes-rewrite-debug") << ", cindex = " << constructorIndex << ", selector is " << selector << std::endl; - int selectorIndex = c.getSelectorIndexInternal(selector.toExpr()); + // The argument that the selector extracts, or -1 if the selector is + // is wrongly applied. + int selectorIndex = -1; + if (k == kind::APPLY_SELECTOR_TOTAL) + { + // The argument index of internal selectors is obtained by + // getSelectorIndexInternal. + selectorIndex = c.getSelectorIndexInternal(selector); + } + else + { + // The argument index of external selectors (applications of + // APPLY_SELECTOR) is given by an attribute and obtained via indexOf below + // The argument is only valid if it is the proper constructor. + selectorIndex = Datatype::indexOf(selector); + if (selectorIndex < 0 || selectorIndex >= c.getNumArgs()) + { + selectorIndex = -1; + } + else if (c[selectorIndex].getSelector() != selector) + { + selectorIndex = -1; + } + } Trace("datatypes-rewrite-debug") << "Internal selector index is " << selectorIndex << std::endl; if (selectorIndex >= 0) @@ -374,7 +398,7 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in) return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); } } - else + else if (k == kind::APPLY_SELECTOR_TOTAL) { Node gt; bool useTe = true; 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"); } |