diff options
author | PaulMeng <baolmeng@gmail.com> | 2018-04-20 10:15:00 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-20 10:15:00 -0500 |
commit | adc22697d4c44c54993aa2048dcbd705cbebd466 (patch) | |
tree | 1a4ebb511ac135bc54d35524fc7d6975dfb750b8 /src/theory/quantifiers/term_util.cpp | |
parent | b384376e687f53bea69b4fdaa11898a52e0f471f (diff) |
Symmetry detection module (#1749)
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 ) { |