Make symmetry-breaker-exp into a preprocessing pass (#1890)

8 files changed, 29 insertions, 8 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index b86ee911d..c3de09de2 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1522,6 +1522,7 @@ REG1_TESTS = \
 	regress1/sym/sym4.smt2 \
 	regress1/sym/sym5.smt2 \
 	regress1/sym/sym6.smt2 \
+	regress1/sym/sym7-uf.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
index ac1c0215f..c063f8b8f 100644
--- a/test/regress/regress1/sym/sym1.smt2
+++ b/test/regress/regress1/sym/sym1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --symmetry-detect
+; COMMAND-LINE: --symmetry-breaker-exp
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun x () Int)
diff --git a/test/regress/regress1/sym/sym2.smt2 b/test/regress/regress1/sym/sym2.smt2
index cff424ba9..e2e62cbb6 100644
--- a/test/regress/regress1/sym/sym2.smt2
+++ b/test/regress/regress1/sym/sym2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --symmetry-detect
+; COMMAND-LINE: --symmetry-breaker-exp
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun x () Int)
diff --git a/test/regress/regress1/sym/sym3.smt2 b/test/regress/regress1/sym/sym3.smt2
index 52f9855c9..c6b87adeb 100644
--- a/test/regress/regress1/sym/sym3.smt2
+++ b/test/regress/regress1/sym/sym3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --symmetry-detect
+; COMMAND-LINE: --symmetry-breaker-exp
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun x () Int)
diff --git a/test/regress/regress1/sym/sym4.smt2 b/test/regress/regress1/sym/sym4.smt2
index 5582ef7d0..1cbd6f5b2 100644
--- a/test/regress/regress1/sym/sym4.smt2
+++ b/test/regress/regress1/sym/sym4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --symmetry-detect
+; COMMAND-LINE: --symmetry-breaker-exp
 (set-info :smt-lib-version 2.6)
 (set-logic QF_LIA)
 (set-info :category "crafted")
@@ -45,4 +45,4 @@
 (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
+(exit)
diff --git a/test/regress/regress1/sym/sym5.smt2 b/test/regress/regress1/sym/sym5.smt2
index f5ef1d003..6b16d9d35 100644
--- a/test/regress/regress1/sym/sym5.smt2
+++ b/test/regress/regress1/sym/sym5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --symmetry-detect
+; COMMAND-LINE: --symmetry-breaker-exp
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun A () (Set Int))
@@ -16,4 +16,4 @@
 (assert (subset B A))
 (assert (= C (intersection A B)))
 (assert (member j C))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/sym/sym6.smt2 b/test/regress/regress1/sym/sym6.smt2
index 3da6b4cb4..10218ebc9 100644
--- a/test/regress/regress1/sym/sym6.smt2
+++ b/test/regress/regress1/sym/sym6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --symmetry-detect
+; COMMAND-LINE: --symmetry-breaker-exp
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun x () Int)
diff --git a/test/regress/regress1/sym/sym7-uf.smt2 b/test/regress/regress1/sym/sym7-uf.smt2
new file mode 100644
index 000000000..ee91240d3
--- /dev/null
+++ b/test/regress/regress1/sym/sym7-uf.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --symmetry-breaker-exp
+(set-logic ALL)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
+(declare-fun z () U)
+(declare-fun w () U)
+(declare-fun u () U)
+(declare-fun v () U)
+(declare-fun a () U)
+(declare-fun P (U) Bool)
+
+(assert (distinct w u v a))
+(assert (or (= x y) (= x z) (= y z)))
+(assert (or (P x) (P y) (P z) (P w)))
+
+; should get { x, y, z }, { w }, { u, v, a }
+(check-sat)
+