diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-09 10:50:55 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-09 10:50:55 -0500 |
commit | df974e62c34f3e1b4f57feb64e439e1e791e87ce (patch) | |
tree | 6cc4cf7410f131745ef6779769160855e3f62eaf /src/preprocessing | |
parent | b8cc1e7e409d5691a6ba29dd369461ff02ef265f (diff) |
Make symmetry-breaker-exp into a preprocessing pass (#1890)
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/symmetry_breaker.cpp | 41 | ||||
-rw-r--r-- | src/preprocessing/passes/symmetry_breaker.h | 18 |
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 |