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 \
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"
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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_ */
#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"
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);
projects / cvc5.git / commitdiff