From df974e62c34f3e1b4f57feb64e439e1e791e87ce Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 May 2018 10:50:55 -0500
Subject: Make symmetry-breaker-exp into a preprocessing pass (#1890)

---
 src/preprocessing/passes/symmetry_breaker.cpp | 41 +++++++++++++++++++++++++--
 src/preprocessing/passes/symmetry_breaker.h   | 18 ++++++++++++
 src/smt/smt_engine.cpp                        | 10 +++----
 3 files changed, 62 insertions(+), 7 deletions(-)

(limited to 'src')

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);
-- 
cgit v1.2.3