diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 35 |
1 files changed, 8 insertions, 27 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 565f99ec5..113d53507 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -69,6 +69,7 @@ #include "options/theory_options.h" #include "options/uf_options.h" #include "preprocessing/passes/bool_to_bv.h" +#include "preprocessing/passes/bv_abstraction.h" #include "preprocessing/passes/bv_gauss.h" #include "preprocessing/passes/bv_intro_pow2.h" #include "preprocessing/passes/bv_to_bool.h" @@ -613,10 +614,6 @@ public: */ bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache); - // Abstract common structure over small domains to UF - // return true if changes were made. - void bvAbstraction(); - // Simplify ITE structure bool simpITE(); @@ -2588,6 +2585,8 @@ void SmtEnginePrivate::finishInit() { // actually assembling preprocessing pipelines). std::unique_ptr<BoolToBV> boolToBv( new BoolToBV(d_preprocessingPassContext.get())); + std::unique_ptr<BvAbstraction> bvAbstract( + new BvAbstraction(d_preprocessingPassContext.get())); std::unique_ptr<BVGauss> bvGauss( new BVGauss(d_preprocessingPassContext.get())); std::unique_ptr<BvIntroPow2> bvIntroPow2( @@ -2601,6 +2600,8 @@ void SmtEnginePrivate::finishInit() { std::unique_ptr<RealToInt> realToInt( new RealToInt(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); + d_preprocessingPassRegistry.registerPass("bv-abstraction", + std::move(bvAbstract)); d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss)); d_preprocessingPassRegistry.registerPass("bv-intro-pow2", std::move(bvIntroPow2)); @@ -3184,24 +3185,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { return true; } -void SmtEnginePrivate::bvAbstraction() { - Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl; - std::vector<Node> new_assertions; - bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertions.ref(), new_assertions); - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions.replace(i, Rewriter::rewrite(new_assertions[i])); - } - // if we are using the lazy solver and the abstraction - // applies, then UF symbols were introduced - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY && - changed) { - LogicRequest req(d_smt); - req.widenLogic(THEORY_UF); - } -} - - - bool SmtEnginePrivate::simpITE() { TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); @@ -4042,11 +4025,9 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_theoryEngine->mkAckermanizationAssertions(d_assertions.ref()); } - if ( options::bvAbstraction() && - !options::incrementalSolving()) { - dumpAssertions("pre-bv-abstraction", d_assertions); - bvAbstraction(); - dumpAssertions("post-bv-abstraction", d_assertions); + if (options::bvAbstraction() && !options::incrementalSolving()) + { + d_preprocessingPassRegistry.getPass("bv-abstraction")->apply(&d_assertions); } Debug("smt") << " d_assertions : " << d_assertions.size() << endl; |