Add the symmetry breaker module (#1847)

5 files changed, 226 insertions, 6 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 411fd363e..22e7daad9 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -78,6 +78,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/bv_to_bool.h \
 	preprocessing/passes/real_to_int.cpp \
 	preprocessing/passes/real_to_int.h \
+	preprocessing/passes/symmetry_breaker.cpp \
+	preprocessing/passes/symmetry_breaker.h \
 	preprocessing/passes/symmetry_detect.cpp \
 	preprocessing/passes/symmetry_detect.h \
 	preprocessing/preprocessing_pass.cpp \
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 73cb87dd4..822f5c022 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -342,15 +342,15 @@ header = "options/smt_options.h"
   type       = "bool"
   default    = "false"
   help       = "calculate sort inference of input problem, convert the input based on monotonic sorts"
-   
+  
 [[option]]
-  name       = "symmetryDetect"
+  name       = "symmetryBreakerExp"
   category   = "regular"
-  long       = "symmetry-detect"
+  long       = "symmetry-breaker-exp"
   type       = "bool"
   default    = "false"
-  help       = "compute symmetries in the input as a preprocessing pass"    
-
+  help       = "generate symmetry breaking constraints after symmetry detection"    
+  
 [[option]]
   name       = "incrementalSolving"
   category   = "common"
diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp
new file mode 100644
index 000000000..2e8c873cd
--- /dev/null
+++ b/src/preprocessing/passes/symmetry_breaker.cpp
@@ -0,0 +1,124 @@
+/*********************                                                        */
+/*! \file symmetry_breaker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Paul Meng, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Symmetry breaker module
+ **/
+
+#include "preprocessing/passes/symmetry_breaker.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+Node SymmetryBreaker::generateSymBkConstraints(const vector<vector<Node>>& parts)
+{
+  vector<Node> constraints;
+  NodeManager* nm = NodeManager::currentNM();
+
+  for (const vector<Node>& part : parts)
+  {
+    if (part.size() >= 2)
+    {
+      Kind kd = getOrderKind(part[0]);
+
+      if (kd != kind::EQUAL)
+      {
+        for (unsigned int i = 0; i < part.size() - 1; ++i)
+        {
+          // Generate less than or equal to constraints: part[i] <= part[i+1]
+          Node constraint = nm->mkNode(kd, part[i], part[i + 1]);
+          constraints.push_back(constraint);
+          Trace("sym-bk")
+              << "[sym-bk] Generate a symmetry breaking constraint: "
+              << constraint << endl;
+        }
+      }
+      else if (part.size() >= 3)
+      {
+        for (unsigned int i = 0; i < part.size(); ++i)
+        {
+          for (unsigned int j = i + 2; j < part.size(); ++i)
+          {
+            // Generate consecutive constraints v_i = v_j => v_i = v_{j-1} for all 0
+            // <= i < j-1 < j < part.size()
+            Node constraint = nm->mkNode(
+                kind::IMPLIES,
+                nm->mkNode(kd, part[i], part[j]),
+                nm->mkNode(kd, part[i], part[j - 1]));
+            constraints.push_back(constraint);
+            Trace("sym-bk")
+                << "[sym-bk] Generate a symmetry breaking constraint: "
+                << constraint << endl;
+          }
+          if (i >= 1)
+          {
+            for (unsigned int j = i + 1; j < part.size(); ++j)
+            {
+              Node lhs = nm->mkNode(kd, part[i], part[j]);
+              Node rhs = nm->mkNode(kd, part[i], part[i - 1]);
+              int prev_seg_start_index = 2*i - j - 1;
+
+              // Since prev_seg_len is always less than i - 1, we just need to make
+              // sure prev_seg_len is greater than or equal to 0
+              if(prev_seg_start_index >= 0)
+              {
+                rhs = nm->mkNode(
+                    kind::OR,
+                    rhs,
+                    nm->mkNode(kd, part[i-1], part[prev_seg_start_index]));
+              }
+              // Generate length order constraints
+              // v_i = v_j => (v_{i} = v_{i-1} OR v_{i-1} = x_{(i-1)-(j-i)})
+              // for all 1 <= i < j < part.size() and (i-1)-(j-i) >= 0
+              Node constraint =
+                  nm->mkNode(kind::IMPLIES, lhs, rhs);
+              constraints.push_back(constraint);
+              Trace("sym-bk")
+                  << "[sym-bk] Generate a symmetry breaking constraint: "
+                  << constraint << endl;
+            }
+          }
+        }
+      }
+    }
+  }
+  if(constraints.empty())
+  {
+    return d_trueNode;
+  }
+  else if(constraints.size() == 1)
+  {
+    return constraints[0];
+  }
+  return nm->mkNode(kind::AND, constraints);;
+}
+
+Kind SymmetryBreaker::getOrderKind(Node node)
+{
+  if (node.getType().isInteger() || node.getType().isReal())
+  {
+    return kind::LEQ;
+  }
+  else if (node.getType().isBitVector())
+  {
+    return kind::BITVECTOR_ULE;
+  }
+  else
+  {
+    return kind::EQUAL;
+  }
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/symmetry_breaker.h b/src/preprocessing/passes/symmetry_breaker.h
new file mode 100644
index 000000000..a89f67a61
--- /dev/null
+++ b/src/preprocessing/passes/symmetry_breaker.h
@@ -0,0 +1,91 @@
+/*********************                                                        */
+/*! \file symmetry_breaker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Paul Meng, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Symmetry breaker for theories
+ **/
+
+#ifndef __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_
+#define __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_
+
+#include <map>
+#include <string>
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/**
+ * Given a vector of partitions {{v_{11}, ... , v_{1n}}, {v_{m1}, ... , v_{mk}}},
+ * the symmetry breaker will generate symmetry breaking constraints for each
+ * partition {v_{i1}, ... , v_{ij}} depending on the type of variables
+ * in each partition.
+ *
+ * For a partition of integer, real and bit-vectors variables {v1, ..., vn},
+ * we generate ordered constraints: {v1 <= v2, ..., v{n-1} <= vn}.
+ * For a partition of variables of other types {v1, ..., vn}, we generate
+ * the following two kinds of constraints.
+ *
+ * 1. Consecutive constraints ensure that equivalence classes over v_1...v_n are
+ *    in consecutive segments
+ *    v_i = v_j => v_i = v_{j-1} for all 0 <= i < j-1 < j < n
+ * 2. Length order constraints ensure that the length of segments occur in
+ *    descending order
+ *    v_i = v_j => (v_{i} = v_{i-1} OR v_{i-1} = x_{(i-1)-(j-i)})
+ *    for all 1 <= i < j < part.size() and (i-1)-(j-i) >= 0
+ * */
+
+class SymmetryBreaker
+{
+ public:
+  /**
+   * Constructor
+   * */
+  SymmetryBreaker()
+  {
+    d_trueNode = NodeManager::currentNM()->mkConst<bool>(true);
+    d_falseNode = NodeManager::currentNM()->mkConst<bool>(false);
+  }
+
+  /**
+   * Destructor
+   * */
+  ~SymmetryBreaker() {}
+
+  /**
+   * This is to generate symmetry breaking constraints for partitions in parts.
+   * Since parts are symmetries of the original assertions C,
+   * the symmetry breaking constraints SB for parts returned by this function
+   * conjuncted with the original assertions SB ^ C is equisatisfiable to C.
+   * */
+  Node generateSymBkConstraints(const std::vector<std::vector<Node> >& parts);
+
+ private:
+
+  /** True and false constant nodes */
+  Node d_trueNode;
+  Node d_falseNode;
+
+  /**
+   * Get the order kind depending on the type of node.
+   * For example, if node is a integer or real, this function would return
+   * the operator less than or equal to (<=) so that we can use it to build
+   * ordered constraints.
+   * */
+  Kind getOrderKind(Node node);
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 113d53507..09a495d1e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -76,6 +76,7 @@
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
 #include "preprocessing/passes/real_to_int.h"
+#include "preprocessing/passes/symmetry_breaker.h"
 #include "preprocessing/passes/symmetry_detect.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
@@ -4195,11 +4196,13 @@ void SmtEnginePrivate::processAssertions() {
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl;
   dumpAssertions("post-simplify", d_assertions);
 
-  if (options::symmetryDetect())
+  if (options::symmetryBreakerExp())
   {
     SymmetryDetect symd;
+    SymmetryBreaker symb;
     vector<vector<Node>> part;
     symd.getPartition(part, d_assertions.ref());
+    Node sbConstraint = symb.generateSymBkConstraints(part);
   }
 
   dumpAssertions("pre-static-learning", d_assertions);