Symmetry detection module (#1749)

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)
+