From: PaulMeng Date: Wed, 9 May 2018 12:41:52 +0000 (-0500) Subject: Add the symmetry breaker module (#1847) X-Git-Tag: cvc5-1.0.0~5074 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8cc1e7e409d5691a6ba29dd369461ff02ef265f;p=cvc5.git Add the symmetry breaker module (#1847) --- 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>& parts) +{ + vector constraints; + NodeManager* nm = NodeManager::currentNM(); + + for (const vector& 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 +#include +#include +#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(true); + d_falseNode = NodeManager::currentNM()->mkConst(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 >& 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> part; symd.getPartition(part, d_assertions.ref()); + Node sbConstraint = symb.generateSymBkConstraints(part); } dumpAssertions("pre-static-learning", d_assertions);