diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-23 17:39:12 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-23 17:39:12 -0500 |
| commit | 3471e731b8538a906e37f8aeb4b0301598b34eff (patch) | |
| tree | e67f70809e791c18aa9ca4800de87a7c707d062b /src/theory/quantifiers/term_util.cpp | |
| parent | 03925b816a0f9aeb079e2c0037a426b5946e2eae (diff) | |
Generalize symmetry detection for 1 symmetry variable mapped to n input variables (#1888)
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 5bf284dff..cf06dfa45 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -817,18 +817,18 @@ bool TermUtil::isNegate(Kind k) } 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 || k == UNION || k == INTERSECTION || k == JOIN - || k == PRODUCT; + 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 + || 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 - || k == UNION || k == INTERSECTION; + 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 + || k == BITVECTOR_XNOR || k == UNION || k == INTERSECTION; } bool TermUtil::isNonAdditive( Kind k ) { |