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

11 files changed, 91 insertions, 15 deletions

diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp
index 2e8c873cd..c6ad09e91 100644
--- a/src/preprocessing/passes/symmetry_breaker.cpp
+++ b/src/preprocessing/passes/symmetry_breaker.cpp
@@ -13,6 +13,7 @@
  **/
 
 #include "preprocessing/passes/symmetry_breaker.h"
+#include "preprocessing/passes/symmetry_detect.h"
 
 using namespace std;
 
@@ -47,7 +48,7 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector<vector<Node>>& parts
       {
         for (unsigned int i = 0; i < part.size(); ++i)
         {
-          for (unsigned int j = i + 2; j < part.size(); ++i)
+          for (unsigned int j = i + 2; j < part.size(); ++j)
           {
             // Generate consecutive constraints v_i = v_j => v_i = v_{j-1} for all 0
             // <= i < j-1 < j < part.size()
@@ -100,7 +101,7 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector<vector<Node>>& parts
   {
     return constraints[0];
   }
-  return nm->mkNode(kind::AND, constraints);;
+  return nm->mkNode(kind::AND, constraints);
 }
 
 Kind SymmetryBreaker::getOrderKind(Node node)
@@ -119,6 +120,42 @@ Kind SymmetryBreaker::getOrderKind(Node node)
   }
 }
 
+SymBreakerPass::SymBreakerPass(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "sym-break"){};
+
+PreprocessingPassResult SymBreakerPass::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  Trace("sym-break-pass") << "Apply symmetry breaker pass..." << std::endl;
+  // detect symmetries
+  std::vector<std::vector<Node>> part;
+  SymmetryDetect symd;
+  symd.getPartition(part, assertionsToPreprocess->ref());
+  if (Trace.isOn("sym-break-pass"))
+  {
+    Trace("sym-break-pass") << "Detected symmetry partition:" << std::endl;
+    for (const std::vector<Node>& p : part)
+    {
+      Trace("sym-break-pass") << "  " << p << std::endl;
+    }
+  }
+  // construct the symmetry breaking constraint
+  Trace("sym-break-pass") << "Construct symmetry breaking constraint..."
+                          << std::endl;
+  SymmetryBreaker symb;
+  Node sbConstraint = symb.generateSymBkConstraints(part);
+  // add symmetry breaking constraint to the set of assertions
+  Trace("sym-break-pass") << "...got: " << sbConstraint << std::endl;
+  // if not true
+  if (!sbConstraint.isConst())
+  {
+    // add to assertions
+    assertionsToPreprocess->push_back(sbConstraint);
+  }
+
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/symmetry_breaker.h b/src/preprocessing/passes/symmetry_breaker.h
index a89f67a61..898b7a122 100644
--- a/src/preprocessing/passes/symmetry_breaker.h
+++ b/src/preprocessing/passes/symmetry_breaker.h
@@ -20,6 +20,9 @@
 #include <vector>
 #include "expr/node.h"
 
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
 namespace CVC4 {
 namespace preprocessing {
 namespace passes {
@@ -84,6 +87,21 @@ class SymmetryBreaker
   Kind getOrderKind(Node node);
 };
 
+/**
+ * This class detects symmetries in the input assertions in the form of a
+ * partition (see symmetry_detect.h), and subsequently adds symmetry breaking
+ * constraints that correspond to this partition, using the above class.
+ */
+class SymBreakerPass : public PreprocessingPass
+{
+ public:
+  SymBreakerPass(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+};
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 09a495d1e..c750b8a12 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2600,6 +2600,8 @@ void SmtEnginePrivate::finishInit() {
       new PseudoBooleanProcessor(d_preprocessingPassContext.get()));
   std::unique_ptr<RealToInt> realToInt(
       new RealToInt(d_preprocessingPassContext.get()));
+  std::unique_ptr<SymBreakerPass> sbProc(
+      new SymBreakerPass(d_preprocessingPassContext.get()));
   d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv));
   d_preprocessingPassRegistry.registerPass("bv-abstraction",
                                            std::move(bvAbstract));
@@ -2611,6 +2613,7 @@ void SmtEnginePrivate::finishInit() {
   d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
                                            std::move(pbProc));
   d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt));
+  d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc));
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
@@ -4198,11 +4201,8 @@ void SmtEnginePrivate::processAssertions() {
 
   if (options::symmetryBreakerExp())
   {
-    SymmetryDetect symd;
-    SymmetryBreaker symb;
-    vector<vector<Node>> part;
-    symd.getPartition(part, d_assertions.ref());
-    Node sbConstraint = symb.generateSymBkConstraints(part);
+    // apply symmetry breaking
+    d_preprocessingPassRegistry.getPass("sym-break")->apply(&d_assertions);
   }
 
   dumpAssertions("pre-static-learning", d_assertions);
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)
+