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 | |
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')
-rw-r--r-- | test/regress/Makefile.tests | 5 | ||||
-rw-r--r-- | test/regress/regress1/sym/q-constant.smt2 | 17 | ||||
-rw-r--r-- | test/regress/regress1/sym/q-function.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress1/sym/qf-function.smt2 | 13 | ||||
-rw-r--r-- | test/regress/regress1/sym/sb-wrong.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress1/sym/sym-setAB.smt2 | 12 |
6 files changed, 71 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 \ diff --git a/test/regress/regress1/sym/q-constant.smt2 b/test/regress/regress1/sym/q-constant.smt2 new file mode 100644 index 000000000..b8fee6c8d --- /dev/null +++ b/test/regress/regress1/sym/q-constant.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic ALL) +(set-info :status unsat) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun P (Int) Bool) +(declare-fun Q (Int) Bool) +(declare-fun R (Int Int) Bool) + +(assert (or (forall ((x Int)) (R x a)) (forall ((x Int)) (R x b)))) +(assert (not (R c a))) +(assert (not (R c b))) + +(check-sat) diff --git a/test/regress/regress1/sym/q-function.smt2 b/test/regress/regress1/sym/q-function.smt2 new file mode 100644 index 000000000..3e303106e --- /dev/null +++ b/test/regress/regress1/sym/q-function.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic ALL) +(set-info :status unsat) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun P (Int) Bool) +(declare-fun Q (Int) Bool) + +(assert (or (forall ((x Int)) (P x)) (forall ((x Int)) (Q x)))) +(assert (not (P a))) +(assert (not (Q a))) +(check-sat) diff --git a/test/regress/regress1/sym/qf-function.smt2 b/test/regress/regress1/sym/qf-function.smt2 new file mode 100644 index 000000000..697f9e1f0 --- /dev/null +++ b/test/regress/regress1/sym/qf-function.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic QF_UFLIA) +(set-info :status sat) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun P (Int) Int) +(declare-fun Q (Int) Int) + +(assert (or (= (f a) 0) (= (g a) 0))) + +(check-sat) diff --git a/test/regress/regress1/sym/sb-wrong.smt2 b/test/regress/regress1/sym/sb-wrong.smt2 new file mode 100644 index 000000000..5f5e6bb34 --- /dev/null +++ b/test/regress/regress1/sym/sb-wrong.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic QF_UFLIA) +(set-info :status sat) +(declare-fun f (Int) Int) +(declare-fun c () Int) +(declare-fun d () Int) +(assert +(or (= c (f d)) (= d (f d))) +) +(check-sat) diff --git a/test/regress/regress1/sym/sym-setAB.smt2 b/test/regress/regress1/sym/sym-setAB.smt2 new file mode 100644 index 000000000..9d613c3b6 --- /dev/null +++ b/test/regress/regress1/sym/sym-setAB.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun C () (Set Int)) + +(assert (and (member x A) (member x B) (member x C))) +(assert (member y C)) +(check-sat) |