From 6c8a2652605b031182b3c2c25d237719470f5620 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 21 Mar 2019 13:41:46 -0500 Subject: [PATCH] Rewrite selectors correctly applied to constructors (#2875) --- src/theory/datatypes/datatypes_rewriter.cpp | 34 ++++++++++++++++--- .../quantifiers/sygus/sygus_unif_io.cpp | 30 ++++++++++------ test/regress/CMakeLists.txt | 2 ++ test/regress/regress1/sygus/double.sy | 26 ++++++++++++++ test/regress/regress1/sygus/extract.sy | 19 +++++++++++ 5 files changed, 96 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress1/sygus/double.sy create mode 100644 test/regress/regress1/sygus/extract.sy 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& 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"); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 21e08f2bf..083f8df75 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1605,8 +1605,10 @@ set(regress_1_tests regress1/sygus/crcy-si-rcons.sy regress1/sygus/crcy-si.sy regress1/sygus/cube-nia.sy + regress1/sygus/double.sy regress1/sygus/dt-test-ns.sy regress1/sygus/dup-op.sy + regress1/sygus/extract.sy regress1/sygus/fg_polynomial3.sy regress1/sygus/find_sc_bvult_bvnot.sy regress1/sygus/hd-01-d1-prog.sy diff --git a/test/regress/regress1/sygus/double.sy b/test/regress/regress1/sygus/double.sy new file mode 100644 index 000000000..f3fea3122 --- /dev/null +++ b/test/regress/regress1/sygus/double.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic SLIA) +(declare-datatype Ex ((Ex2 (ex Int)))) + +(synth-fun double ((x1 Ex)) Int + ( + (Start Int (ntInt)) + (ntInt Int + ( + (ex ntEx) + (+ ntInt ntInt) + ) + ) + (ntEx Ex + ( + x1 + (Ex2 ntInt) + ) + ) + ) +) +(constraint (= (double (Ex2 1)) 2)) +(constraint (= (double (Ex2 4)) 8)) +(check-synth) diff --git a/test/regress/regress1/sygus/extract.sy b/test/regress/regress1/sygus/extract.sy new file mode 100644 index 000000000..d1541fa87 --- /dev/null +++ b/test/regress/regress1/sygus/extract.sy @@ -0,0 +1,19 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic ALL_SUPPORTED) +(declare-datatype Ex ((Ex2 (ex Int)))) + +(synth-fun ident ((x1 Ex)) Int + ( + (Start Int (ntInt)) + (ntInt Int + ( + (ex ntEx) + ) + ) + (ntEx Ex ( x1 ) ) + ) +) +(constraint (= (ident (Ex2 1)) 1)) +(check-synth) -- 2.30.2