diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 38f6a2d5e..cc6f09801 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -80,6 +80,7 @@ #include "preprocessing/passes/real_to_int.h" #include "preprocessing/passes/rewrite.h" #include "preprocessing/passes/sep_skolem_emp.h" +#include "preprocessing/passes/sort_infer.h" #include "preprocessing/passes/static_learning.h" #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" @@ -2735,15 +2736,18 @@ void SmtEnginePrivate::finishInit() new RealToInt(d_preprocessingPassContext.get())); std::unique_ptr<Rewrite> rewrite( new Rewrite(d_preprocessingPassContext.get())); + std::unique_ptr<SortInferencePass> sortInfer( + new SortInferencePass(d_preprocessingPassContext.get(), + d_smt.d_theoryEngine->getSortInference())); std::unique_ptr<StaticLearning> staticLearning( new StaticLearning(d_preprocessingPassContext.get())); std::unique_ptr<SymBreakerPass> sbProc( new SymBreakerPass(d_preprocessingPassContext.get())); std::unique_ptr<SynthRewRulesPass> srrProc( new SynthRewRulesPass(d_preprocessingPassContext.get())); - std::unique_ptr<SepSkolemEmp> sepSkolemEmp( + std::unique_ptr<SepSkolemEmp> sepSkolemEmp( new SepSkolemEmp(d_preprocessingPassContext.get())); - d_preprocessingPassRegistry.registerPass("apply-substs", + d_preprocessingPassRegistry.registerPass("apply-substs", std::move(applySubsts)); d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); d_preprocessingPassRegistry.registerPass("bv-abstraction", @@ -2761,6 +2765,8 @@ void SmtEnginePrivate::finishInit() d_preprocessingPassRegistry.registerPass("rewrite", std::move(rewrite)); d_preprocessingPassRegistry.registerPass("sep-skolem-emp", std::move(sepSkolemEmp)); + d_preprocessingPassRegistry.registerPass("sort-inference", + std::move(sortInfer)); d_preprocessingPassRegistry.registerPass("static-learning", std::move(staticLearning)); d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); @@ -4332,13 +4338,7 @@ void SmtEnginePrivate::processAssertions() { } if( options::sortInference() || options::ufssFairnessMonotone() ){ - //sort inference technique - SortInference * si = d_smt.d_theoryEngine->getSortInference(); - si->simplify( d_assertions.ref(), options::sortInference(), options::ufssFairnessMonotone() ); - for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){ - d_smt.setPrintFuncInModel( it->first.toExpr(), false ); - d_smt.setPrintFuncInModel( it->second.toExpr(), true ); - } + d_preprocessingPassRegistry.getPass("sort-inference")->apply(&d_assertions); } if( options::pbRewrites() ){ |