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.

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)