diff options
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index b3915bd5d..76d95bf5e 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -811,14 +811,18 @@ Node TermUtil::mkNegate(Kind notk, Node n) } bool TermUtil::isAssoc( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT || - k==STRING_CONCAT; + return k == PLUS || k == MULT || k == AND || k == OR || k == BITVECTOR_PLUS + || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR + || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT + || k == STRING_CONCAT || k == UNION || k == INTERSECTION || k == JOIN + || k == PRODUCT; } bool TermUtil::isComm( Kind k ) { - return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; + return k == EQUAL || k == PLUS || k == MULT || k == AND || k == OR || k == XOR + || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_AND + || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR + || k == UNION || k == INTERSECTION; } bool TermUtil::isNonAdditive( Kind k ) { |