From 943a02def30dca73a6e9ac2eb744bcf87372e920 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 3 May 2022 09:55:43 -0500 Subject: [PATCH] Change option name for mbqi in fmf (#8701) In preparation for a new basic implementation of MBQI. --- src/options/quantifiers_options.toml | 6 +++--- src/smt/set_defaults.cpp | 12 ++++++------ src/theory/quantifiers/fmf/full_model_check.cpp | 2 +- src/theory/quantifiers/fmf/model_builder.cpp | 2 +- src/theory/quantifiers/fmf/model_engine.cpp | 9 ++++----- src/theory/quantifiers/term_registry.cpp | 3 --- src/theory/quantifiers_engine.cpp | 9 +++++---- 7 files changed, 20 insertions(+), 23 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index bbd26f702..a4c33c946 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -602,10 +602,10 @@ name = "Quantifiers" help = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant" [[option]] - name = "mbqiMode" + name = "fmfMbqiMode" category = "expert" - long = "mbqi=MODE" - type = "MbqiMode" + long = "fmf-mbqi=MODE" + type = "FmfMbqiMode" default = "FMC" help = "choose mode for model-based quantifier instantiation" help_mode = "Model-based quantifier instantiation modes." diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 32fd86f24..4f54310e7 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1416,12 +1416,12 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, // apply fmfBound options if (opts.quantifiers.fmfBound) { - if (!opts.quantifiers.mbqiModeWasSetByUser - || (opts.quantifiers.mbqiMode != options::MbqiMode::NONE - && opts.quantifiers.mbqiMode != options::MbqiMode::FMC)) + if (!opts.quantifiers.fmfMbqiModeWasSetByUser + || (opts.quantifiers.fmfMbqiMode != options::FmfMbqiMode::NONE + && opts.quantifiers.fmfMbqiMode != options::FmfMbqiMode::FMC)) { // if bounded integers are set, use no MBQI by default - opts.quantifiers.mbqiMode = options::MbqiMode::NONE; + opts.quantifiers.fmfMbqiMode = options::FmfMbqiMode::NONE; } if (!opts.quantifiers.prenexQuantUserWasSetByUser) { @@ -1432,9 +1432,9 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, { // if higher-order, then current variants of model-based instantiation // cannot be used - if (opts.quantifiers.mbqiMode != options::MbqiMode::NONE) + if (opts.quantifiers.fmfMbqiMode != options::FmfMbqiMode::NONE) { - opts.quantifiers.mbqiMode = options::MbqiMode::NONE; + opts.quantifiers.fmfMbqiMode = options::FmfMbqiMode::NONE; } if (!opts.quantifiers.hoElimStoreAxWasSetByUser) { diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 503ee4c2c..0304043e9 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -646,7 +646,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i FirstOrderModelFmc* fmfmc = static_cast(fm); if (effort == 0) { - if (options().quantifiers.mbqiMode == options::MbqiMode::NONE) + if (options().quantifiers.fmfMbqiMode == options::FmfMbqiMode::NONE) { // just exhaustive instantiate Node c = mkCondDefault(fmfmc, f); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index b52f7178d..34054e366 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -54,7 +54,7 @@ void QModelBuilder::finishInit() } bool QModelBuilder::optUseModel() { - return options().quantifiers.mbqiMode != options::MbqiMode::NONE + return options().quantifiers.fmfMbqiMode != options::FmfMbqiMode::NONE || options().quantifiers.fmfBound || options().strings.stringExp; } diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index a295c3005..641ac836f 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -219,11 +219,10 @@ int ModelEngine::checkModel(){ Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; // FMC uses two sub-effort levels - int e_max = - options().quantifiers.mbqiMode == options::MbqiMode::FMC - ? 2 - : (options().quantifiers.mbqiMode == options::MbqiMode::TRUST ? 0 - : 1); + options::FmfMbqiMode mode = options().quantifiers.fmfMbqiMode; + int e_max = mode == options::FmfMbqiMode::FMC + ? 2 + : (mode == options::FmfMbqiMode::TRUST ? 0 : 1); for( int e=0; egetNumAssertedQuantifiers(); i++ ){ diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index c08815c43..06b3f318a 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -57,9 +57,6 @@ TermRegistry::TermRegistry(Env& env, d_sygusTdb.reset(new TermDbSygus(env, qs, d_ochecker.get())); } Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; - Trace("quant-engine-debug") - << "Initialize model, mbqi : " << options().quantifiers.mbqiMode - << std::endl; } void TermRegistry::finishInit(FirstOrderModel* fm, diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0eaea7fe7..08d68a95f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -63,16 +63,17 @@ QuantifiersEngine::QuantifiersEngine( d_quants_red(userContext()), d_numInstRoundsLemma(0) { + options::FmfMbqiMode mmode = options().quantifiers.fmfMbqiMode; Trace("quant-init-debug") - << "Initialize model engine, mbqi : " << options().quantifiers.mbqiMode - << " " << options().quantifiers.fmfBound << std::endl; + << "Initialize model engine, mbqi : " << mmode << " " + << options().quantifiers.fmfBound << std::endl; // Finite model finding requires specialized ways of building the model. // We require constructing the model here, since it is required for // initializing the CombinationEngine and the rest of quantifiers engine. if (options().quantifiers.fmfBound || options().strings.stringExp || (options().quantifiers.finiteModelFind - && (options().quantifiers.mbqiMode == options::MbqiMode::FMC - || options().quantifiers.mbqiMode == options::MbqiMode::TRUST))) + && (mmode == options::FmfMbqiMode::FMC + || mmode == options::FmfMbqiMode::TRUST))) { Trace("quant-init-debug") << "...make fmc builder." << std::endl; d_builder.reset( -- 2.30.2