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

2 files changed, 57 insertions, 2 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