diff options
author | PaulMeng <baolmeng@gmail.com> | 2018-04-20 10:15:00 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-20 10:15:00 -0500 |
commit | adc22697d4c44c54993aa2048dcbd705cbebd466 (patch) | |
tree | 1a4ebb511ac135bc54d35524fc7d6975dfb750b8 /test/regress | |
parent | b384376e687f53bea69b4fdaa11898a52e0f471f (diff) |
Symmetry detection module (#1749)
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/Makefile.tests | 6 | ||||
-rw-r--r-- | test/regress/regress1/sym/sym1.smt2 | 21 | ||||
-rw-r--r-- | test/regress/regress1/sym/sym2.smt2 | 27 | ||||
-rw-r--r-- | test/regress/regress1/sym/sym3.smt2 | 21 | ||||
-rw-r--r-- | test/regress/regress1/sym/sym4.smt2 | 48 | ||||
-rw-r--r-- | test/regress/regress1/sym/sym5.smt2 | 19 | ||||
-rw-r--r-- | test/regress/regress1/sym/sym6.smt2 | 24 |
7 files changed, 166 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 56965f272..a29236914 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1490,6 +1490,12 @@ REG1_TESTS = \ regress1/sygus/twolets2-orig.sy \ regress1/sygus/unbdd_inv_gen_ex7.sy \ regress1/sygus/unbdd_inv_gen_winf1.sy \ + regress1/sym/sym1.smt2 \ + regress1/sym/sym2.smt2 \ + regress1/sym/sym3.smt2 \ + regress1/sym/sym4.smt2 \ + regress1/sym/sym5.smt2 \ + regress1/sym/sym6.smt2 \ regress1/test12.cvc \ regress1/trim.cvc \ regress1/uf2.smt2 \ diff --git a/test/regress/regress1/sym/sym1.smt2 b/test/regress/regress1/sym/sym1.smt2 new file mode 100644 index 000000000..ac1c0215f --- /dev/null +++ b/test/regress/regress1/sym/sym1.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: --symmetry-detect +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) + + +(declare-fun p (Int) Bool) +(declare-fun A () (Set Int)) +(declare-fun F () (Set Int)) + + + +(assert (= F (insert x y (singleton z)))) +(assert (subset F A)) +(assert (= x y)) + + +(check-sat) + diff --git a/test/regress/regress1/sym/sym2.smt2 b/test/regress/regress1/sym/sym2.smt2 new file mode 100644 index 000000000..cff424ba9 --- /dev/null +++ b/test/regress/regress1/sym/sym2.smt2 @@ -0,0 +1,27 @@ +; COMMAND-LINE: --symmetry-detect +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(declare-fun w () Int) +(declare-fun u () Int) +(declare-fun v () Int) + + +(assert (> (- (+ (* 3 x) (* 3 y) (* 3 z)) u v) 0)) +(assert (> (+ u v) 0)) +(assert (> (+ x y) 0)) +(assert (> x 0)) +(assert (> z 0)) +(assert (> u 0)) +(assert (> v 0)) +(assert (< u 10)) +(assert (< v 10)) + + + + + +(check-sat) + diff --git a/test/regress/regress1/sym/sym3.smt2 b/test/regress/regress1/sym/sym3.smt2 new file mode 100644 index 000000000..52f9855c9 --- /dev/null +++ b/test/regress/regress1/sym/sym3.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: --symmetry-detect +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(declare-fun w () Int) +(declare-fun u () Int) +(declare-fun v () Int) + +(declare-fun p (Int Int) Int) +(declare-fun A () (Set Int)) + + +(assert (or (> (+ x y z) 3) (< (p x (+ (* 3 y) (* 3 z))) 5))) +(assert (subset A (insert y (singleton z)))) + + + +(check-sat) + diff --git a/test/regress/regress1/sym/sym4.smt2 b/test/regress/regress1/sym/sym4.smt2 new file mode 100644 index 000000000..5582ef7d0 --- /dev/null +++ b/test/regress/regress1/sym/sym4.smt2 @@ -0,0 +1,48 @@ +; COMMAND-LINE: --symmetry-detect +(set-info :smt-lib-version 2.6) +(set-logic QF_LIA) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x_0 () Int) +(declare-fun x_1 () Int) +(declare-fun x_2 () Int) +(declare-fun x_3 () Int) +(declare-fun x_4 () Int) +(declare-fun x_5 () Int) +(declare-fun x_6 () Int) +(declare-fun x_7 () Int) +(declare-fun x_8 () Int) +(declare-fun x_9 () Int) +(declare-fun x_10 () Int) +(declare-fun x_11 () Int) +(declare-fun x_12 () Int) +(declare-fun x_13 () Int) +(declare-fun x_14 () Int) +(declare-fun x_15 () Int) +(declare-fun x_16 () Int) +(assert (>= x_0 0)) +(assert (>= x_1 0)) +(assert (>= x_2 0)) +(assert (>= x_3 0)) +(assert (>= x_4 0)) +(assert (>= x_5 0)) +(assert (>= x_6 0)) +(assert (>= x_7 0)) +(assert (>= x_8 0)) +(assert (>= x_9 0)) +(assert (>= x_10 0)) +(assert (>= x_11 0)) +(assert (>= x_12 0)) +(assert (>= x_13 0)) +(assert (>= x_14 0)) +(assert (>= x_15 0)) +(assert (>= x_16 0)) +(assert (<= (+ (* 37 x_0) (* 37 x_1) (* 37 x_2) (* 37 x_3) (* 37 x_4) (* 37 x_5) (* 37 x_6) (* 37 x_7) (* 37 x_8) (* 37 x_9) (* 37 x_10) (* (- 404) x_11) (* 37 x_12) (* 37 x_13) (* 37 x_14) (* 37 x_15) (* 37 x_16)) 0)) +(assert (<= (+ (* 41 x_0) (* 41 x_1) (* 41 x_2) (* 41 x_3) (* 41 x_4) (* 41 x_5) (* 41 x_6) (* 41 x_7) (* 41 x_8) (* 41 x_9) (* 41 x_10) (* 41 x_11) (* (- 400) x_12) (* 41 x_13) (* 41 x_14) (* 41 x_15) (* 41 x_16)) 0)) +(assert (<= (+ (* 43 x_0) (* 43 x_1) (* 43 x_2) (* 43 x_3) (* 43 x_4) (* 43 x_5) (* 43 x_6) (* 43 x_7) (* 43 x_8) (* 43 x_9) (* 43 x_10) (* 43 x_11) (* 43 x_12) (* (- 398) x_13) (* 43 x_14) (* 43 x_15) (* 43 x_16)) 0)) +(assert (<= (+ (* 47 x_0) (* 47 x_1) (* 47 x_2) (* 47 x_3) (* 47 x_4) (* 47 x_5) (* 47 x_6) (* 47 x_7) (* 47 x_8) (* 47 x_9) (* 47 x_10) (* 47 x_11) (* 47 x_12) (* 47 x_13) (* (- 394) x_14) (* 47 x_15) (* 47 x_16)) 0)) +(assert (<= (+ (* 53 x_0) (* 53 x_1) (* 53 x_2) (* 53 x_3) (* 53 x_4) (* 53 x_5) (* 53 x_6) (* 53 x_7) (* 53 x_8) (* 53 x_9) (* 53 x_10) (* 53 x_11) (* 53 x_12) (* 53 x_13) (* 53 x_14) (* (- 388) x_15) (* 53 x_16)) 0)) +(assert (<= (+ (* 59 x_0) (* 59 x_1) (* 59 x_2) (* 59 x_3) (* 59 x_4) (* 59 x_5) (* 59 x_6) (* 59 x_7) (* 59 x_8) (* 59 x_9) (* 59 x_10) (* 59 x_11) (* 59 x_12) (* 59 x_13) (* 59 x_14) (* 59 x_15) (* (- 382) x_16)) 0)) +(assert (>= (+ x_0 x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9 x_10 x_11 x_12 x_13 x_14 x_15 x_16) 1)) +(check-sat) +(exit)
\ No newline at end of file diff --git a/test/regress/regress1/sym/sym5.smt2 b/test/regress/regress1/sym/sym5.smt2 new file mode 100644 index 000000000..f5ef1d003 --- /dev/null +++ b/test/regress/regress1/sym/sym5.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --symmetry-detect +(set-logic ALL) +(set-info :status unsat) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun C () (Set Int)) + +(declare-fun f () Int) +(declare-fun g () Int) +(declare-fun h () Int) +(declare-fun i () Int) +(declare-fun j () Int) + +(assert (subset A (insert g h i (singleton f)))) +(assert (= C (setminus A B) )) +(assert (subset B A)) +(assert (= C (intersection A B))) +(assert (member j C)) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/sym/sym6.smt2 b/test/regress/regress1/sym/sym6.smt2 new file mode 100644 index 000000000..3da6b4cb4 --- /dev/null +++ b/test/regress/regress1/sym/sym6.smt2 @@ -0,0 +1,24 @@ +; COMMAND-LINE: --symmetry-detect +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(declare-fun w () Int) +(declare-fun u () Int) +(declare-fun v () Int) + + +(assert (= (+ w y u) (+ v z))) + +(assert (> (+ x (* 2 y)) (+ u v))) + +(assert (= (- x) (- (- y)))) + + + +(assert (or (< (+ x y z) 10) (> (+ v u) 10))) + + +(check-sat) + |