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/regress1/sym | |
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/regress1/sym')
-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 |
5 files changed, 66 insertions, 0 deletions
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) |