diff options
author | PaulMeng <baolmeng@gmail.com> | 2018-05-09 07:41:52 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-09 07:41:52 -0500 |
commit | b8cc1e7e409d5691a6ba29dd369461ff02ef265f (patch) | |
tree | 4c92a8908d4660a10ebe93b064c632226d111002 /src/preprocessing | |
parent | 08ddea9c91fc5c481642c4911d4af562ac2a88e1 (diff) |
Add the symmetry breaker module (#1847)
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/symmetry_breaker.cpp | 124 | ||||
-rw-r--r-- | src/preprocessing/passes/symmetry_breaker.h | 91 |
2 files changed, 215 insertions, 0 deletions
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_ */ |