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 /test/regress/Makefile.tests | |
| 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 'test/regress/Makefile.tests')
| -rw-r--r-- | test/regress/Makefile.tests | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index b4f920ca4..a1cba3b55 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1618,6 +1618,10 @@ REG1_TESTS = \ regress1/sygus/unbdd_inv_gen_ex7.sy \ regress1/sygus/unbdd_inv_gen_winf1.sy \ regress1/sygus/univ_2-long-repeat.sy \ + regress1/sym/qf-function.smt2 \ + regress1/sym/q-constant.smt2 \ + regress1/sym/q-function.smt2 \ + regress1/sym/sb-wrong.smt2 \ regress1/sym/sym1.smt2 \ regress1/sym/sym2.smt2 \ regress1/sym/sym3.smt2 \ @@ -1625,6 +1629,7 @@ REG1_TESTS = \ regress1/sym/sym5.smt2 \ regress1/sym/sym6.smt2 \ regress1/sym/sym7-uf.smt2 \ + regress1/sym/sym-setAB.smt2 \ regress1/test12.cvc \ regress1/trim.cvc \ regress1/uf2.smt2 \ |