diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-17 19:51:06 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-17 17:51:06 -0700 |
| commit | 83be77ff113cbc0357796fb8121091eed2c95ab1 (patch) | |
| tree | da64946f41e6e4ce24ef589ebc7dcd40c1469413 /src/theory/quantifiers | |
| parent | 603c0ccc4614024dfcd34333cd427ac56e229a47 (diff) | |
Improvements and fixes for symmetry detection and breaking (#2459)
This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index d2b7688ec..f8e8ed5ad 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -659,14 +659,16 @@ bool TermUtil::isAssoc( Kind k ) { || 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; + || k == UNION || k == INTERSECTION || k == JOIN || k == PRODUCT + || k == SEP_STAR; } bool TermUtil::isComm( Kind k ) { 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; + || k == BITVECTOR_XNOR || k == UNION || k == INTERSECTION + || k == SEP_STAR; } bool TermUtil::isNonAdditive( Kind k ) { |