diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/preprocessing/preprocessing_pass_registry.cpp | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 |
2 files changed, 12 insertions, 0 deletions
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 34bae1224..36b3c6392 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -34,6 +34,7 @@ #include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/passes/extended_rewriter_pass.h" #include "preprocessing/passes/global_negate.h" +#include "preprocessing/passes/ho_elim.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/ite_removal.h" #include "preprocessing/passes/ite_simp.h" @@ -148,6 +149,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("quantifier-macros", callCtor<QuantifierMacros>); registerPassInfo("nl-ext-purify", callCtor<NlExtPurify>); registerPassInfo("bool-to-bv", callCtor<BoolToBV>); + registerPassInfo("ho-elim", callCtor<HoElim>); } } // namespace preprocessing diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 560cb0599..4a8803392 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1838,6 +1838,11 @@ void SmtEngine::setDefaults() { if( options::mbqiMode()!=quantifiers::MBQI_NONE ){ options::mbqiMode.set( quantifiers::MBQI_NONE ); } + if (!options::hoElimStoreAx.wasSetByUser()) + { + // by default, use store axioms only if --ho-elim is set + options::hoElimStoreAx.set(options::hoElim()); + } } if( options::fmfFunWellDefinedRelevant() ){ if( !options::fmfFunWellDefined.wasSetByUser() ){ @@ -3488,6 +3493,11 @@ void SmtEnginePrivate::processAssertions() { d_passes["apply-to-const"]->apply(&d_assertions); } + if (options::ufHo()) + { + d_passes["ho-elim"]->apply(&d_assertions); + } + // begin: INVARIANT to maintain: no reordering of assertions or // introducing new ones #ifdef CVC4_ASSERTIONS |