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/theory_quantifiers.cpp | |
| 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/theory_quantifiers.cpp')
0 files changed, 0 insertions, 0 deletions