Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-03-11 | Remove experimental symmetry breaker (#4005) | Andrew Reynolds | |
This never impacted performance positively. Fixes #3997 and fixes #4015. There was a folder that the symmetry breaker was used on regress1/sym. These are simple examples that show when it is possible to find symmetries in SMT; the symmetry breaker is not critical for solving these. For now I'm leaving them as regressions documenting possible benchmarks to target if we revisit this technique. | |||
2018-09-17 | Improvements and fixes for symmetry detection and breaking (#2459) | Andrew Reynolds | |
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. |