diff options
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 20 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_util.h | 16 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 3 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sets/sets-extr.smt2 | 15 |
6 files changed, 50 insertions, 8 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index b583a55da..ae053930c 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -119,7 +119,8 @@ Node ExtendedRewriter::extendedRewrite(Node n) Kind k = n.getKind(); bool childChanged = false; bool isNonAdditive = TermUtil::isNonAdditive(k); - bool isAssoc = TermUtil::isAssoc(k); + // We flatten associative operators below, which requires k to be n-ary. + bool isAssoc = TermUtil::isAssoc(k, true); for (unsigned i = 0; i < n.getNumChildren(); i++) { Node nc = extendedRewrite(n[i]); diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index f8e8ed5ad..4c9cf2c8d 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -654,7 +654,15 @@ bool TermUtil::isNegate(Kind k) return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS; } -bool TermUtil::isAssoc( Kind k ) { +bool TermUtil::isAssoc(Kind k, bool reqNAry) +{ + if (reqNAry) + { + if (k == UNION || k == INTERSECTION) + { + return false; + } + } return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR @@ -663,7 +671,15 @@ bool TermUtil::isAssoc( Kind k ) { || k == SEP_STAR; } -bool TermUtil::isComm( Kind k ) { +bool TermUtil::isComm(Kind k, bool reqNAry) +{ + if (reqNAry) + { + if (k == UNION || k == INTERSECTION) + { + return false; + } + } return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index dd3e76ee2..820821991 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -270,10 +270,18 @@ public: * double negation if applicable, e.g. mkNegate( ~, ~x ) ---> x. */ static Node mkNegate(Kind notk, Node n); - /** is assoc */ - static bool isAssoc( Kind k ); - /** is k commutative? */ - static bool isComm( Kind k ); + /** is k associative? + * + * If flag reqNAry is true, then we additionally require that k is an + * n-ary operator. + */ + static bool isAssoc(Kind k, bool reqNAry = false); + /** is k commutative? + * + * If flag reqNAry is true, then we additionally require that k is an + * n-ary operator. + */ + static bool isComm(Kind k, bool reqNAry = false); /** is k non-additive? * Returns true if diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index a3f1f9893..2a2015319 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -47,7 +47,7 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm) RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager* nm = NodeManager::currentNM(); Kind kind = node.getKind(); - + Trace("sets-postrewrite") << "Process: " << node << std::endl; if(node.isConst()) { // Dare you touch the const and mangle it to something else. @@ -204,6 +204,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { if( rew!=node ){ Trace("sets-rewrite") << "Sets::rewrite " << node << " -> " << rew << std::endl; } + Trace("sets-rewrite") << "...no rewrite." << std::endl; return RewriteResponse(REWRITE_DONE, rew); } break; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9e942aae1..95e4b8875 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -776,6 +776,7 @@ set(regress_0_tests regress0/sets/pre-proc-univ.smt2 regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 regress0/sets/sets-equal.smt2 + regress0/sets/sets-extr.smt2 regress0/sets/sets-inter.smt2 regress0/sets/sets-of-sets-subtypes.smt2 regress0/sets/sets-poly-int-real.smt2 diff --git a/test/regress/regress0/sets/sets-extr.smt2 b/test/regress/regress0/sets/sets-extr.smt2 new file mode 100644 index 000000000..c497ff189 --- /dev/null +++ b/test/regress/regress0/sets/sets-extr.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg +; EXPECT: sat +(set-logic ALL) +(declare-sort Atom 0) + +(declare-fun a () Atom) +(declare-fun b () Atom) +(declare-fun c () Atom) +(declare-fun S () (Set Atom)) + + +(assert (= S (union (singleton a) (union (singleton c) (singleton b))))) + +(check-sat) + |