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/smt | |
parent | b8cc1e7e409d5691a6ba29dd369461ff02ef265f (diff) |
Make symmetry-breaker-exp into a preprocessing pass (#1890)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 09a495d1e..c750b8a12 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2600,6 +2600,8 @@ void SmtEnginePrivate::finishInit() { new PseudoBooleanProcessor(d_preprocessingPassContext.get())); std::unique_ptr<RealToInt> realToInt( new RealToInt(d_preprocessingPassContext.get())); + std::unique_ptr<SymBreakerPass> sbProc( + new SymBreakerPass(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); d_preprocessingPassRegistry.registerPass("bv-abstraction", std::move(bvAbstract)); @@ -2611,6 +2613,7 @@ void SmtEnginePrivate::finishInit() { d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", std::move(pbProc)); d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt)); + d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) @@ -4198,11 +4201,8 @@ void SmtEnginePrivate::processAssertions() { if (options::symmetryBreakerExp()) { - SymmetryDetect symd; - SymmetryBreaker symb; - vector<vector<Node>> part; - symd.getPartition(part, d_assertions.ref()); - Node sbConstraint = symb.generateSymBkConstraints(part); + // apply symmetry breaking + d_preprocessingPassRegistry.getPass("sym-break")->apply(&d_assertions); } dumpAssertions("pre-static-learning", d_assertions); |