diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-08-16 16:15:07 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-16 16:15:07 -0500 |
commit | 0e77d62ac116c00bcb0bccdb1f48f87067529d56 (patch) | |
tree | f28ee420eef68eff771446c246829ee4acb0c15e /src/smt | |
parent | 80be200c84494a4f82ab30cb743b7758c67db5b5 (diff) |
Refactor extended rewriter preprocessing pass (#2324)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 41b113b94..b5d758bca 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -77,6 +77,7 @@ #include "preprocessing/passes/bv_gauss.h" #include "preprocessing/passes/bv_intro_pow2.h" #include "preprocessing/passes/bv_to_bool.h" +#include "preprocessing/passes/extended_rewriter_pass.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/pseudo_boolean_processor.h" #include "preprocessing/passes/real_to_int.h" @@ -2672,6 +2673,8 @@ void SmtEnginePrivate::finishInit() new BvIntroPow2(d_preprocessingPassContext.get())); std::unique_ptr<BVToBool> bvToBool( new BVToBool(d_preprocessingPassContext.get())); + std::unique_ptr<ExtRewPre> extRewPre( + new ExtRewPre(d_preprocessingPassContext.get())); std::unique_ptr<IntToBV> intToBV( new IntToBV(d_preprocessingPassContext.get())); std::unique_ptr<PseudoBooleanProcessor> pbProc( @@ -2704,6 +2707,7 @@ void SmtEnginePrivate::finishInit() d_preprocessingPassRegistry.registerPass("bv-intro-pow2", std::move(bvIntroPow2)); d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool)); + d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre)); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", std::move(pbProc)); @@ -4156,19 +4160,14 @@ void SmtEnginePrivate::processAssertions() { if (options::extRewPrep()) { - theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg()); - for (unsigned i = 0; i < d_assertions.size(); ++i) - { - Node a = d_assertions[i]; - d_assertions.replace(i, extr.extendedRewrite(a)); - } + d_preprocessingPassRegistry.getPass("ext-rew-pre")->apply(&d_assertions); } // Unconstrained simplification if(options::unconstrainedSimp()) { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl; dumpAssertions("pre-unconstrained-simp", d_assertions); - d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); + d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); unconstrainedSimp(); Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl; dumpAssertions("post-unconstrained-simp", d_assertions); |