diff options
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 |