diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-12-13 20:17:50 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-14 02:17:50 +0000 |
| commit | 075e3d97974c89dcbd4cf6c7a1c3b37cbb27403d (patch) | |
| tree | cb1466de550072e4a11d0a67816e6e23ef5770cb /src/theory/quantifiers/term_util.cpp | |
| parent | 000feaeb02292d7a2873198664022801b12e5151 (diff) | |
Fix extended rewriter for binary associative operators. (#2751)
This was causing assertion failures when using Sets + Sygus.
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 20 |
1 files changed, 18 insertions, 2 deletions
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 |