diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2018-08-22 21:13:46 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-22 23:13:46 -0500 |
| commit | ac7db6796f2255678d3b2e2e87940211f162223e (patch) | |
| tree | c5857619f46843e8d77093e5b1f468ff2d340535 /src/smt/smt_engine.cpp | |
| parent | 83d07f5d7662557f2087136563606872b217511a (diff) | |
global-negate preprocessing pass (#2317)
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f9ea2f1ac..33ca6eb3d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -79,6 +79,7 @@ #include "preprocessing/passes/bv_intro_pow2.h" #include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/passes/extended_rewriter_pass.h" +#include "preprocessing/passes/global_negate.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/ite_removal.h" #include "preprocessing/passes/pseudo_boolean_processor.h" @@ -115,7 +116,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/global_negate.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" @@ -2660,6 +2660,8 @@ void SmtEnginePrivate::finishInit() new BVToBool(d_preprocessingPassContext.get())); std::unique_ptr<ExtRewPre> extRewPre( new ExtRewPre(d_preprocessingPassContext.get())); + std::unique_ptr<GlobalNegate> globalNegate( + new GlobalNegate(d_preprocessingPassContext.get())); std::unique_ptr<IntToBV> intToBV( new IntToBV(d_preprocessingPassContext.get())); std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess( @@ -2701,6 +2703,8 @@ void SmtEnginePrivate::finishInit() std::move(bvIntroPow2)); d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool)); d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre)); + d_preprocessingPassRegistry.registerPass("global-negate", + std::move(globalNegate)); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); d_preprocessingPassRegistry.registerPass("quantifiers-preprocess", std::move(quantifiersPreprocess)); @@ -4085,8 +4089,7 @@ void SmtEnginePrivate::processAssertions() { if (options::globalNegate()) { // global negation of the formula - quantifiers::GlobalNegate gn; - gn.simplify(d_assertions.ref()); + d_preprocessingPassRegistry.getPass("global-negate")->apply(&d_assertions); d_smt.d_globalNegation = !d_smt.d_globalNegation; } |