diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 70e575487..0497c2814 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -85,6 +85,8 @@ #include "preprocessing/passes/ite_simp.h" #include "preprocessing/passes/nl_ext_purify.h" #include "preprocessing/passes/pseudo_boolean_processor.h" +#include "preprocessing/passes/quantifier_macros.h" +#include "preprocessing/passes/quantifier_macros.h" #include "preprocessing/passes/quantifiers_preprocess.h" #include "preprocessing/passes/real_to_int.h" #include "preprocessing/passes/rewrite.h" @@ -118,7 +120,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/sygus/ce_guided_instantiation.h" @@ -2686,6 +2687,8 @@ void SmtEnginePrivate::finishInit() std::move(bvAckermann)); d_preprocessingPassRegistry.registerPass("bv-eager-atoms", std::move(bvEagerAtoms)); + std::unique_ptr<QuantifierMacros> quantifierMacros( + new QuantifierMacros(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss)); d_preprocessingPassRegistry.registerPass("bv-intro-pow2", std::move(bvIntroPow2)); @@ -2715,6 +2718,8 @@ void SmtEnginePrivate::finishInit() std::move(sygusInfer)); d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); d_preprocessingPassRegistry.registerPass("synth-rr", std::move(srrProc)); + d_preprocessingPassRegistry.registerPass("quantifier-macros", + std::move(quantifierMacros)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) @@ -4078,13 +4083,8 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-skolem-quant", d_assertions); if( options::macrosQuant() ){ //quantifiers macro expansion - quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() ); - bool success; - do{ - success = qm.simplify( d_assertions.ref(), true ); - }while( success ); - //finalize the definitions - qm.finalizeDefinitions(); + d_preprocessingPassRegistry.getPass("quantifier-macros") + ->apply(&d_assertions); } //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF |