diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 22916e354..5d9f08343 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -78,6 +78,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/rewrite.h" #include "preprocessing/passes/static_learning.h" #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" @@ -2716,6 +2717,8 @@ void SmtEnginePrivate::finishInit() new PseudoBooleanProcessor(d_preprocessingPassContext.get())); std::unique_ptr<RealToInt> realToInt( new RealToInt(d_preprocessingPassContext.get())); + std::unique_ptr<Rewrite> rewrite( + new Rewrite(d_preprocessingPassContext.get())); std::unique_ptr<StaticLearning> staticLearning( new StaticLearning(d_preprocessingPassContext.get())); std::unique_ptr<SymBreakerPass> sbProc( @@ -2737,6 +2740,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("rewrite", std::move(rewrite)); d_preprocessingPassRegistry.registerPass("static-learning", std::move(staticLearning)); d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); @@ -4168,10 +4172,7 @@ void SmtEnginePrivate::processAssertions() { if(options::unconstrainedSimp()) { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl; dumpAssertions("pre-unconstrained-simp", d_assertions); - Chat() << "...doing unconstrained simplification..." << endl; - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions.replace(i, Rewriter::rewrite(d_assertions[i])); - } + d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); unconstrainedSimp(); Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl; dumpAssertions("post-unconstrained-simp", d_assertions); @@ -4189,10 +4190,7 @@ void SmtEnginePrivate::processAssertions() { { // special rewriting pass for unsat cores, since many of the passes below // are skipped - for (unsigned i = 0; i < d_assertions.size(); ++i) - { - d_assertions.replace(i, Rewriter::rewrite(d_assertions[i])); - } + d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); } else { |