From 1015442ffc16dc8214c10ad3bcfab4fb3759db86 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 23 Apr 2024 08:55:39 -0500 Subject: [PATCH] Add `-o options-auto` (#10620) Used for debugging which options are automatically configured by cvc5 before solving. --- src/api/cpp/cvc5.cpp | 2 +- src/options/base_options.toml | 5 + src/options/mkoptions.py | 12 +- src/options/options_handler.cpp | 22 +- src/smt/abduction_solver.cpp | 6 +- src/smt/interpolation_solver.cpp | 2 +- src/smt/set_defaults.cpp | 523 +++++++++--------- src/smt/solver_engine.cpp | 12 +- src/smt/sygus_solver.cpp | 4 +- .../inst_strategy_sub_conflict.cpp | 8 +- .../quantifiers/query_generator_unsat.cpp | 10 +- .../quantifiers/sygus/sygus_interpol.cpp | 2 +- src/theory/quantifiers/sygus/synth_verify.cpp | 12 +- test/regress/cli/CMakeLists.txt | 1 + .../regress0/printer/print_options_auto.smt2 | 6 + .../theory/theory_arith_coverings_white.cpp | 4 +- 16 files changed, 331 insertions(+), 300 deletions(-) create mode 100644 test/regress/cli/regress0/printer/print_options_auto.smt2 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 48fa89ca39e..b3d3d8f1c65 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -8316,7 +8316,7 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const if (keyword == "filename") { // only the Solver object has non-const access to the original options - d_originalOptions->writeDriver().filename = value; + d_originalOptions->write_driver().filename = value; } d_slv->setInfo(keyword, value); //////// diff --git a/src/options/base_options.toml b/src/options/base_options.toml index e1a5d68c30e..71c739f485d 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -255,6 +255,11 @@ name = "Base" help = "prints the formulas used when block-model is run." description = "With ``-o block-model``, cvc5 prints the formulas used when block-model is run." example-file = "regress0/printer/block_model_out.smt2" +[[option.mode.OPTIONS_AUTO]] + name = "options-auto" + help = "prints the options set during automatic configuration." + description = "With ``-o options-auto``, cvc5 prints the options set during automatic configuration." + example-file = "regress0/printer/print_options_auto.smt2" # Stores then enabled output tags. [[option]] diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 3c3c9167696..f27fbba0120 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -233,7 +233,7 @@ def generate_holder_mem_decls(modules): def generate_holder_ref_decls(modules): """Render reference declarations for holder members of the Option class""" return concat_format(''' const options::Holder{id_cap}& {id}; - options::Holder{id_cap}& write{id_capitalized}();''', modules) + options::Holder{id_cap}& write_{id}();''', modules) ################################################################################ @@ -259,7 +259,7 @@ def generate_holder_ref_inits(modules): def generate_write_functions(modules): """Render write functions for holders within the Option class""" - return concat_format(''' options::Holder{id_cap}& Options::write{id_capitalized}() + return concat_format(''' options::Holder{id_cap}& Options::write_{id}() {{ return *d_{id}; }} @@ -401,10 +401,10 @@ def generate_set_impl(modules): for pred in _set_predicates(module, option): res.append(' {}'.format(pred)) if option.name: - res.append(' opts.write{module}().{name} = value;'.format( - module=module.id_capitalized, name=option.name)) - res.append(' opts.write{module}().{name}WasSetByUser = true;'.format( - module=module.id_capitalized, name=option.name)) + res.append(' opts.write_{module}().{name} = value;'.format( + module=module.id, name=option.name)) + res.append(' opts.write_{module}().{name}WasSetByUser = true;'.format( + module=module.id, name=option.name)) res.append(' break;') res.append(' }') res.append('}') diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index a3f97d8d97a..e22fb78a911 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -152,7 +152,7 @@ void OptionsHandler::setInputLanguage(const std::string& flag, Language lang) } if (!d_options->printer.outputLanguageWasSetByUser) { - d_options->writePrinter().outputLanguage = lang; + d_options->write_printer().outputLanguage = lang; ioutils::setDefaultOutputLanguage(lang); } } @@ -173,13 +173,13 @@ void OptionsHandler::setVerbosity(const std::string& flag, int value) void OptionsHandler::decreaseVerbosity(const std::string& flag, bool value) { - d_options->writeBase().verbosity -= 1; + d_options->write_base().verbosity -= 1; setVerbosity(flag, d_options->base.verbosity); } void OptionsHandler::increaseVerbosity(const std::string& flag, bool value) { - d_options->writeBase().verbosity += 1; + d_options->write_base().verbosity += 1; setVerbosity(flag, d_options->base.verbosity); } @@ -197,9 +197,9 @@ void OptionsHandler::setStats(const std::string& flag, bool value) #endif /* CVC5_STATISTICS_ON */ if (!value) { - d_options->writeBase().statisticsAll = false; - d_options->writeBase().statisticsEveryQuery = false; - d_options->writeBase().statisticsInternal = false; + d_options->write_base().statisticsAll = false; + d_options->write_base().statisticsEveryQuery = false; + d_options->write_base().statisticsInternal = false; } } @@ -217,7 +217,7 @@ void OptionsHandler::setStatsDetail(const std::string& flag, bool value) #endif /* CVC5_STATISTICS_ON */ if (value) { - d_options->writeBase().statistics = true; + d_options->write_base().statistics = true; } } @@ -233,7 +233,7 @@ void OptionsHandler::enableTraceTag(const std::string& flag, { if (optarg == "help") { - d_options->writeDriver().showTraceTags = true; + d_options->write_driver().showTraceTags = true; showTraceTags("", true); return; } @@ -254,13 +254,13 @@ void OptionsHandler::enableOutputTag(const std::string& flag, size_t tagid = static_cast(optarg); Assert(d_options->base.outputTagHolder.size() > tagid) << "Output tag is larger than the bitset that holds it."; - d_options->writeBase().outputTagHolder.set(tagid); + d_options->write_base().outputTagHolder.set(tagid); } void OptionsHandler::setResourceWeight(const std::string& flag, const std::string& optarg) { - d_options->writeBase().resourceWeightHolder.emplace_back(optarg); + d_options->write_base().resourceWeightHolder.emplace_back(optarg); } void OptionsHandler::checkBvSatSolver(const std::string& flag, @@ -312,7 +312,7 @@ void OptionsHandler::checkBvSatSolver(const std::string& flag, } if (!d_options->bv.bitvectorToBoolWasSetByUser) { - d_options->writeBv().bitvectorToBool = true; + d_options->write_bv().bitvectorToBool = true; } } } diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 2797629b6b8..6fb422596fd 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -70,11 +70,11 @@ bool AbductionSolver::getAbduct(const std::vector& axioms, Options subOptions; subOptions.copyValues(d_env.getOptions()); - subOptions.writeQuantifiers().sygus = true; + subOptions.write_quantifiers().sygus = true; // by default, we don't want disjunctive terms (ITE, OR) in abducts if (!d_env.getOptions().quantifiers.sygusGrammarUseDisjWasSetByUser) { - subOptions.writeQuantifiers().sygusGrammarUseDisj = false; + subOptions.write_quantifiers().sygusGrammarUseDisj = false; } SetDefaults::disableChecking(subOptions); SubsolverSetupInfo ssi(d_env, subOptions); @@ -180,7 +180,7 @@ void AbductionSolver::checkAbduct(Node a) Options subOptions; subOptions.copyValues(d_env.getOptions()); - subOptions.writeSmt().produceAbducts = false; + subOptions.write_smt().produceAbducts = false; SetDefaults::disableChecking(subOptions); SubsolverSetupInfo ssi(d_env, subOptions); // two checks: first, consistent with assertions, second, implies negated goal diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 070a6db362c..8101de430c8 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -93,7 +93,7 @@ void InterpolationSolver::checkInterpol(Node interpol, Options subOptions; subOptions.copyValues(d_env.getOptions()); - subOptions.writeSmt().produceInterpolants = false; + subOptions.write_smt().produceInterpolants = false; SetDefaults::disableChecking(subOptions); SubsolverSetupInfo ssi(d_env, subOptions); // two checks: first, axioms imply interpol, second, interpol implies conj. diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 1fd68f8d191..45c402d250e 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -50,11 +50,11 @@ namespace smt { * Set domain.optName to value due to reason. Notify if value changes. * Note this macro should be used if the value is concrete. */ -#define SET_AND_NOTIFY(domain, optName, value, reason) \ - if (opts.write##domain().optName != value) \ - { \ - notifyModifyOption(#optName, #value, reason); \ - opts.write##domain().optName = value; \ +#define SET_AND_NOTIFY(domain, optName, value, reason) \ + if (opts.write_##domain().optName != value) \ + { \ + notifyModifyOption(options::domain::longName::optName, #value, reason); \ + opts.write_##domain().optName = value; \ } /** * Set domain.optName to value due to reason. Notify if value changes. @@ -62,38 +62,40 @@ namespace smt { * Note this macro should be used if the value passed to the macro is not * concrete (i.e., stored in a variable). */ -#define SET_AND_NOTIFY_VAL_SYM(domain, optName, value, reason) \ - if (opts.write##domain().optName != value) \ - { \ - std::stringstream sstmp; \ - sstmp << value; \ - notifyModifyOption(#optName, sstmp.str(), reason); \ - opts.write##domain().optName = value; \ +#define SET_AND_NOTIFY_VAL_SYM(domain, optName, value, reason) \ + if (opts.write_##domain().optName != value) \ + { \ + std::stringstream sstmp; \ + sstmp << value; \ + notifyModifyOption( \ + options::domain::longName::optName, sstmp.str(), reason); \ + opts.write_##domain().optName = value; \ } /** * Set domain.optName to value due to reason if the option was not already set * by the user. Notify if value changes. * Note this macro should be used if the value is concrete. */ -#define SET_AND_NOTIFY_IF_NOT_USER(domain, optName, value, reason) \ - if (!opts.write##domain().optName##WasSetByUser \ - && opts.write##domain().optName != value) \ - { \ - notifyModifyOption(#optName, #value, reason); \ - opts.write##domain().optName = value; \ +#define SET_AND_NOTIFY_IF_NOT_USER(domain, optName, value, reason) \ + if (!opts.write_##domain().optName##WasSetByUser \ + && opts.write_##domain().optName != value) \ + { \ + notifyModifyOption(options::domain::longName::optName, #value, reason); \ + opts.write_##domain().optName = value; \ } /** * Set domain.optName to value due to reason if the option was not already set * by the user. Notify if value changes. */ #define SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(domain, optName, value, reason) \ - if (!opts.write##domain().optName##WasSetByUser \ - && opts.write##domain().optName != value) \ + if (!opts.write_##domain().optName##WasSetByUser \ + && opts.write_##domain().optName != value) \ { \ std::stringstream sstmp; \ sstmp << value; \ - notifyModifyOption(#optName, sstmp.str(), reason); \ - opts.write##domain().optName = value; \ + notifyModifyOption( \ + options::domain::longName::optName, sstmp.str(), reason); \ + opts.write_##domain().optName = value; \ } SetDefaults::SetDefaults(Env& env, bool isInternalSubsolver) @@ -116,20 +118,20 @@ void SetDefaults::setDefaultsPre(Options& opts) // implied options if (opts.smt.debugCheckModels) { - SET_AND_NOTIFY(Smt, checkModels, true, "debugCheckModels"); + SET_AND_NOTIFY(smt, checkModels, true, "debugCheckModels"); } if (opts.smt.checkModels || opts.driver.dumpModels) { - SET_AND_NOTIFY(Smt, produceModels, true, "check or dump models"); + SET_AND_NOTIFY(smt, produceModels, true, "check or dump models"); } if (opts.smt.checkModels) { - SET_AND_NOTIFY(Smt, produceAssignments, true, "checkModels"); + SET_AND_NOTIFY(smt, produceAssignments, true, "checkModels"); } // unsat cores and proofs shenanigans if (opts.driver.dumpDifficulty) { - SET_AND_NOTIFY(Smt, produceDifficulty, true, "dumpDifficulty"); + SET_AND_NOTIFY(smt, produceDifficulty, true, "dumpDifficulty"); } if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores || opts.driver.dumpUnsatCoresLemmas || opts.smt.unsatAssumptions @@ -137,46 +139,47 @@ void SetDefaults::setDefaultsPre(Options& opts) || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF) { SET_AND_NOTIFY( - Smt, produceUnsatCores, true, "option requiring unsat cores"); + smt, produceUnsatCores, true, "option requiring unsat cores"); } if (opts.smt.produceUnsatCores && opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) { - SET_AND_NOTIFY(Smt, + SET_AND_NOTIFY(smt, unsatCoresMode, options::UnsatCoresMode::ASSUMPTIONS, "enabling unsat cores"); } if (opts.proof.checkProofSteps) { - SET_AND_NOTIFY(Smt, checkProofs, true, "check-proof-steps"); + SET_AND_NOTIFY(smt, checkProofs, true, "check-proof-steps"); // maximize the granularity - SET_AND_NOTIFY_IF_NOT_USER(Proof, - proofGranularityMode, - options::ProofGranularityMode::DSL_REWRITE, - "check-proof-steps"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM( + proof, + proofGranularityMode, + options::ProofGranularityMode::DSL_REWRITE, + "check-proof-steps"); } // if check-proofs, dump-proofs, or proof-mode=full, then proofs being fully // enabled is implied if (opts.smt.checkProofs || opts.driver.dumpProofs || opts.smt.proofMode == options::ProofMode::FULL) { - SET_AND_NOTIFY(Smt, produceProofs, true, "option requiring proofs"); + SET_AND_NOTIFY(smt, produceProofs, true, "option requiring proofs"); } // this check assumes the user has requested *full* proofs if (opts.smt.produceProofs) { // if the user requested proofs, proof mode is full - SET_AND_NOTIFY(Smt, proofMode, options::ProofMode::FULL, "enabling proofs"); + SET_AND_NOTIFY(smt, proofMode, options::ProofMode::FULL, "enabling proofs"); // unsat cores are available due to proofs being enabled if (opts.smt.unsatCoresMode != options::UnsatCoresMode::SAT_PROOF) { - SET_AND_NOTIFY(Smt, produceUnsatCores, true, "enabling proofs"); + SET_AND_NOTIFY(smt, produceUnsatCores, true, "enabling proofs"); if (options().prop.satSolver == options::SatSolverMode::MINISAT) { // if full proofs are available in minisat, use them for unsat cores - SET_AND_NOTIFY(Smt, + SET_AND_NOTIFY(smt, unsatCoresMode, options::UnsatCoresMode::SAT_PROOF, "enabling proofs, minisat"); @@ -185,7 +188,7 @@ void SetDefaults::setDefaultsPre(Options& opts) { // unsat cores available by assumptions by default if proofs are enabled // with CaDiCaL. - SET_AND_NOTIFY(Smt, + SET_AND_NOTIFY(smt, unsatCoresMode, options::UnsatCoresMode::ASSUMPTIONS, "enabling proofs, non-minisat"); @@ -207,10 +210,11 @@ void SetDefaults::setDefaultsPre(Options& opts) if (opts.proof.proofGranularityMode < options::ProofGranularityMode::THEORY_REWRITE) { - SET_AND_NOTIFY(Proof, - proofGranularityMode, - options::ProofGranularityMode::THEORY_REWRITE, - "Alethe requires granularity at least theory-rewrite"); + SET_AND_NOTIFY_VAL_SYM( + proof, + proofGranularityMode, + options::ProofGranularityMode::THEORY_REWRITE, + "Alethe requires granularity at least theory-rewrite"); } } } @@ -220,35 +224,35 @@ void SetDefaults::setDefaultsPre(Options& opts) { // if (expert) user set proof mode to something other than off, enable // proofs - SET_AND_NOTIFY(Smt, produceProofs, true, "proof mode"); + SET_AND_NOTIFY(smt, produceProofs, true, "proof mode"); } // if proofs weren't enabled by user, and we are producing difficulty if (opts.smt.produceDifficulty) { - SET_AND_NOTIFY(Smt, produceProofs, true, "produce difficulty"); + SET_AND_NOTIFY(smt, produceProofs, true, "produce difficulty"); // ensure at least preprocessing proofs are enabled if (opts.smt.proofMode == options::ProofMode::OFF) { - SET_AND_NOTIFY( - Smt, proofMode, options::ProofMode::PP_ONLY, "produce difficulty"); + SET_AND_NOTIFY_VAL_SYM( + smt, proofMode, options::ProofMode::PP_ONLY, "produce difficulty"); } } // if proofs weren't enabled by user, and we are producing unsat cores if (opts.smt.produceUnsatCores) { - SET_AND_NOTIFY(Smt, produceProofs, true, "unsat cores"); + SET_AND_NOTIFY(smt, produceProofs, true, "unsat cores"); if (opts.smt.unsatCoresMode == options::UnsatCoresMode::SAT_PROOF) { // if requested to be based on proofs, we produce (preprocessing +) SAT // proofs - SET_AND_NOTIFY( - Smt, proofMode, options::ProofMode::SAT, "unsat cores SAT proof"); + SET_AND_NOTIFY_VAL_SYM( + smt, proofMode, options::ProofMode::SAT, "unsat cores SAT proof"); } else if (opts.smt.proofMode == options::ProofMode::OFF) { // otherwise, we always produce preprocessing proofs - SET_AND_NOTIFY( - Smt, proofMode, options::ProofMode::PP_ONLY, "unsat cores"); + SET_AND_NOTIFY_VAL_SYM( + smt, proofMode, options::ProofMode::PP_ONLY, "unsat cores"); } } } @@ -260,7 +264,7 @@ void SetDefaults::setDefaultsPre(Options& opts) if (opts.prop.satSolver == options::SatSolverMode::CADICAL) { // use SAT_EXTERNAL_PROVE for cadical by default - SET_AND_NOTIFY(Proof, + SET_AND_NOTIFY(proof, propProofMode, options::PropProofMode::SAT_EXTERNAL_PROVE, "cadical"); @@ -290,15 +294,15 @@ void SetDefaults::setDefaultsPre(Options& opts) { // these options must be disabled on internal subsolvers, as they are // used by the user to rephrase the input. - SET_AND_NOTIFY(Quantifiers, - sygusInference, - options::SygusInferenceMode::OFF, - "internal subsolver"); + SET_AND_NOTIFY_VAL_SYM(quantifiers, + sygusInference, + options::SygusInferenceMode::OFF, + "internal subsolver"); // deep restart does not work with internal subsolvers? - SET_AND_NOTIFY(Smt, - deepRestartMode, - options::DeepRestartMode::NONE, - "internal subsolver"); + SET_AND_NOTIFY_VAL_SYM(smt, + deepRestartMode, + options::DeepRestartMode::NONE, + "internal subsolver"); } } @@ -319,7 +323,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const && logic.areIntegersUsed())) && !opts.base.incrementalSolving) { - SET_AND_NOTIFY(Quantifiers, sygusInst, true, "logic"); + SET_AND_NOTIFY(quantifiers, sygusInst, true, "logic"); } if (opts.bv.bitblastMode == options::BitblastMode::EAGER) @@ -339,12 +343,12 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const throw OptionException(ss.str()); } SET_AND_NOTIFY( - Bv, bitblastMode, options::BitblastMode::LAZY, "model generation"); + bv, bitblastMode, options::BitblastMode::LAZY, "model generation"); } else if (!opts.base.incrementalSolving) { // if not incremental, we rely on ackermann to eliminate other theories. - SET_AND_NOTIFY(Smt, ackermann, true, "bit-blast eager"); + SET_AND_NOTIFY(smt, ackermann, true, "bit-blast eager"); } else if (logic.isQuantified() || !logic.isPure(THEORY_BV)) { @@ -394,7 +398,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const throw OptionException(std::string( "Ackermannization currently does not support model generation.")); } - SET_AND_NOTIFY(Smt, ackermann, false, "model generation"); + SET_AND_NOTIFY(smt, ackermann, false, "model generation"); // we are not relying on ackermann to eliminate theories in this case Assert(opts.bv.bitblastMode != options::BitblastMode::EAGER); } @@ -417,7 +421,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const if (logic.isTheoryEnabled(THEORY_STRINGS) && !options().strings.stringExpWasSetByUser) { - SET_AND_NOTIFY(Strings, stringExp, true, "logic including strings"); + SET_AND_NOTIFY(strings, stringExp, true, "logic including strings"); } // If strings-exp is enabled, we require quantifiers. We also enable them // if we are using eager string preprocessing or aggressive regular expression @@ -490,7 +494,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { - SET_AND_NOTIFY(Smt, produceAssertions, true, "always enabled"); + SET_AND_NOTIFY(smt, produceAssertions, true, "always enabled"); if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF) { @@ -500,7 +504,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const * Therefore, we enable bv-to-bool, which runs before * the translation to integers. */ - SET_AND_NOTIFY(Bv, bitvectorToBool, true, "solve-bv-as-int"); + SET_AND_NOTIFY(bv, bitvectorToBool, true, "solve-bv-as-int"); } // Disable options incompatible with incremental solving, or output an error @@ -546,7 +550,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && logic.isTheoryEnabled(THEORY_BV) && !logic.isTheoryEnabled(THEORY_ARITH); SET_AND_NOTIFY_VAL_SYM( - Smt, unconstrainedSimp, uncSimp, "logic and options"); + smt, unconstrainedSimp, uncSimp, "logic and options"); } // by default, nonclausal simplification is off for QF_SAT @@ -557,17 +561,17 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const // quantifiers, not others if (qf_sat) { - SET_AND_NOTIFY(Smt, - simplificationMode, - options::SimplificationMode::NONE, - "logic"); + SET_AND_NOTIFY_VAL_SYM(smt, + simplificationMode, + options::SimplificationMode::NONE, + "logic"); } else { - SET_AND_NOTIFY(Smt, - simplificationMode, - options::SimplificationMode::BATCH, - "logic"); + SET_AND_NOTIFY_VAL_SYM(smt, + simplificationMode, + options::SimplificationMode::BATCH, + "logic"); } } } @@ -582,15 +586,15 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const "bool-to-bv != off not supported with CEGQI BV for quantified " "logics"); } - SET_AND_NOTIFY( - Bv, boolToBitvector, options::BoolToBVMode::OFF, "cegqiBv"); + SET_AND_NOTIFY_VAL_SYM( + bv, boolToBitvector, options::BoolToBVMode::OFF, "cegqiBv"); } } // cases where we need produce models if (opts.smt.produceAssignments || usesSygus(opts)) { - SET_AND_NOTIFY(Smt, produceModels, true, "produce assignments or sygus"); + SET_AND_NOTIFY(smt, produceModels, true, "produce assignments or sygus"); } // --ite-simp is an experimental option designed for QF_LIA/nec. This @@ -599,7 +603,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const // this by default. if (opts.smt.doITESimp) { - SET_AND_NOTIFY_IF_NOT_USER(Smt, earlyIteRemoval, true, "doITESimp"); + SET_AND_NOTIFY_IF_NOT_USER(smt, earlyIteRemoval, true, "doITESimp"); } // Set the options for the theoryOf @@ -612,10 +616,10 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && !(logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() && !logic.isQuantified())) { - SET_AND_NOTIFY(Theory, - theoryOfMode, - options::TheoryOfMode::THEORY_OF_TERM_BASED, - "logic"); + SET_AND_NOTIFY_VAL_SYM(theory, + theoryOfMode, + options::TheoryOfMode::THEORY_OF_TERM_BASED, + "logic"); } } @@ -626,7 +630,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && !opts.base.incrementalSolving && !safeUnsatCores(opts); SET_AND_NOTIFY_VAL_SYM( - Uf, ufSymmetryBreaker, qf_uf_noinc, "logic and options"); + uf, ufSymmetryBreaker, qf_uf_noinc, "logic and options"); } // If in arrays, set the UF handler to arrays @@ -647,7 +651,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const bool qf_aufbv = !logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS) && logic.isTheoryEnabled(THEORY_UF) && logic.isTheoryEnabled(THEORY_BV); - SET_AND_NOTIFY_VAL_SYM(Smt, simplifyWithCareEnabled, qf_aufbv, "logic"); + SET_AND_NOTIFY_VAL_SYM(smt, simplifyWithCareEnabled, qf_aufbv, "logic"); } // Turn off array eager index splitting for QF_AUFLIA if (!opts.arrays.arraysEagerIndexSplittingWasSetByUser) @@ -656,7 +660,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && logic.isTheoryEnabled(THEORY_UF) && logic.isTheoryEnabled(THEORY_ARITH)) { - SET_AND_NOTIFY(Arrays, arraysEagerIndexSplitting, false, "logic"); + SET_AND_NOTIFY(arrays, arraysEagerIndexSplitting, false, "logic"); } } // Turn on multiple-pass non-clausal simplification for QF_AUFBV @@ -667,13 +671,13 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const && logic.isTheoryEnabled(THEORY_UF) && logic.isTheoryEnabled(THEORY_BV)) && !safeUnsatCores(opts); - SET_AND_NOTIFY_VAL_SYM(Smt, repeatSimp, repeatSimp, "logic"); + SET_AND_NOTIFY_VAL_SYM(smt, repeatSimp, repeatSimp, "logic"); } /* Disable bit-level propagation by default for the BITBLAST solver. */ if (opts.bv.bvSolver == options::BVSolver::BITBLAST) { - SET_AND_NOTIFY(Bv, bitvectorPropagate, false, "bitblast solver"); + SET_AND_NOTIFY(bv, bitvectorPropagate, false, "bitblast solver"); } if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL @@ -684,8 +688,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const throw OptionException( "bool-to-bv=all not supported for non-bitvector logics."); } - SET_AND_NOTIFY( - Bv, boolToBitvector, options::BoolToBVMode::OFF, "non-BV logic"); + SET_AND_NOTIFY_VAL_SYM( + bv, boolToBitvector, options::BoolToBVMode::OFF, "non-BV logic"); } // Turn on arith rewrite equalities only for pure arithmetic @@ -693,7 +697,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { bool arithRewriteEq = logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified(); - SET_AND_NOTIFY_VAL_SYM(Arith, arithRewriteEq, arithRewriteEq, "logic"); + SET_AND_NOTIFY_VAL_SYM(arith, arithRewriteEq, arithRewriteEq, "logic"); } if (!opts.arith.arithHeuristicPivotsWasSetByUser) { @@ -710,7 +714,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } } SET_AND_NOTIFY_VAL_SYM( - Arith, arithHeuristicPivots, heuristicPivots, "logic"); + arith, arithHeuristicPivots, heuristicPivots, "logic"); } if (!opts.arith.arithPivotThresholdWasSetByUser) { @@ -722,7 +726,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const pivotThreshold = 16; } } - SET_AND_NOTIFY_VAL_SYM(Arith, arithPivotThreshold, pivotThreshold, "logic"); + SET_AND_NOTIFY_VAL_SYM(arith, arithPivotThreshold, pivotThreshold, "logic"); } if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser) { @@ -732,12 +736,12 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const varOrderPivots = 200; } SET_AND_NOTIFY_VAL_SYM( - Arith, arithStandardCheckVarOrderPivots, varOrderPivots, "logic"); + arith, arithStandardCheckVarOrderPivots, varOrderPivots, "logic"); } if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed()) { SET_AND_NOTIFY( - Arith, nlExtTangentPlanesInterleave, true, "pure integer logic"); + arith, nlExtTangentPlanesInterleave, true, "pure integer logic"); } if (!opts.arith.nlRlvAssertBoundsWasSetByUser) { @@ -745,7 +749,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const // use bound inference to determine when bounds are irrelevant only when // the logic is quantifier-free SET_AND_NOTIFY_VAL_SYM( - Arith, nlRlvAssertBounds, val, "non-quantified logic"); + arith, nlRlvAssertBounds, val, "non-quantified logic"); } // set the default decision mode @@ -756,12 +760,12 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { // use the arithmetic equality solver by default SET_AND_NOTIFY_IF_NOT_USER( - Arith, arithEqSolver, true, "central equality engine"); + arith, arithEqSolver, true, "central equality engine"); } if (logic.isHigherOrder()) { - SET_AND_NOTIFY(Theory, assignFunctionValues, true, "higher-order logic"); + SET_AND_NOTIFY(theory, assignFunctionValues, true, "higher-order logic"); } // set all defaults in the quantifiers theory, which includes sygus @@ -772,7 +776,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const if (logic.isQuantified() && !usesSygus(opts)) { SET_AND_NOTIFY_IF_NOT_USER( - Datatypes, dtSharedSelectors, false, "quantified logic without SyGuS"); + datatypes, dtSharedSelectors, false, "quantified logic without SyGuS"); } if (opts.prop.minisatSimpMode == options::MinisatSimpMode::ALL) @@ -790,32 +794,32 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const || opts.smt.checkModels || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())) { - SET_AND_NOTIFY_IF_NOT_USER(Prop, - minisatSimpMode, - options::MinisatSimpMode::CLAUSE_ELIM, - "non-basic logic"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(prop, + minisatSimpMode, + options::MinisatSimpMode::CLAUSE_ELIM, + "non-basic logic"); } } if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() && opts.arith.nlRlvMode != options::NlRlvMode::NONE) { - SET_AND_NOTIFY(Theory, relevanceFilter, true, "nl relevance mode"); + SET_AND_NOTIFY(theory, relevanceFilter, true, "nl relevance mode"); } // For now, these array theory optimizations do not support model-building if (opts.smt.produceModels || opts.smt.produceAssignments || opts.smt.checkModels) { - SET_AND_NOTIFY(Arrays, arraysOptimizeLinear, false, "models"); + SET_AND_NOTIFY(arrays, arraysOptimizeLinear, false, "models"); } if (opts.strings.stringFMF) { - SET_AND_NOTIFY_IF_NOT_USER(Strings, - stringProcessLoopMode, - options::ProcessLoopMode::SIMPLE, - "strings-fmf"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(strings, + stringProcessLoopMode, + options::ProcessLoopMode::SIMPLE, + "strings-fmf"); } // !!! All options that require disabling models go here @@ -831,7 +835,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const ss << "Cannot use " << sOptNoModel << " with model generation."; throw OptionException(ss.str()); } - SET_AND_NOTIFY(Smt, produceModels, false, sOptNoModel); + SET_AND_NOTIFY(smt, produceModels, false, sOptNoModel); } if (opts.smt.produceAssignments) { @@ -842,7 +846,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const << " with model generation (produce-assignments)."; throw OptionException(ss.str()); } - SET_AND_NOTIFY(Smt, produceAssignments, false, sOptNoModel); + SET_AND_NOTIFY(smt, produceAssignments, false, sOptNoModel); } if (opts.smt.checkModels) { @@ -853,7 +857,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const << " with model generation (check-models)."; throw OptionException(ss.str()); } - SET_AND_NOTIFY(Smt, checkModels, false, sOptNoModel); + SET_AND_NOTIFY(smt, checkModels, false, sOptNoModel); } } @@ -870,9 +874,9 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser) { - SET_AND_NOTIFY(Arith, nlCov, true, "QF_UFNRA"); - SET_AND_NOTIFY_IF_NOT_USER( - Arith, nlExt, options::NlExtMode::LIGHT, "QF_UFNRA"); + SET_AND_NOTIFY(arith, nlCov, true, "QF_UFNRA"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM( + arith, nlExt, options::NlExtMode::LIGHT, "QF_UFNRA"); } } else if (logic.isQuantified() && logic.isTheoryEnabled(theory::THEORY_ARITH) @@ -881,9 +885,9 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser) { - SET_AND_NOTIFY(Arith, nlCov, true, "logic with reals"); - SET_AND_NOTIFY_IF_NOT_USER( - Arith, nlExt, options::NlExtMode::LIGHT, "logic with reals"); + SET_AND_NOTIFY(arith, nlCov, true, "logic with reals"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM( + arith, nlExt, options::NlExtMode::LIGHT, "logic with reals"); } } #else @@ -898,16 +902,16 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } else { - SET_AND_NOTIFY(Arith, nlCov, false, "no support for libpoly"); - SET_AND_NOTIFY( - Arith, nlExt, options::NlExtMode::FULL, "no support for libpoly"); + SET_AND_NOTIFY(arith, nlCov, false, "no support for libpoly"); + SET_AND_NOTIFY_VAL_SYM( + arith, nlExt, options::NlExtMode::FULL, "no support for libpoly"); } } #endif if (logic.isTheoryEnabled(theory::THEORY_ARITH) && logic.areTranscendentalsUsed()) { - SET_AND_NOTIFY_IF_NOT_USER( - Arith, nlExt, options::NlExtMode::FULL, "logic with transcendentals"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM( + arith, nlExt, options::NlExtMode::FULL, "logic with transcendentals"); } } @@ -990,16 +994,16 @@ bool SetDefaults::incompatibleWithProofs(Options& opts, // options that are automatically set to support proofs if (opts.bv.bvAssertInput) { - SET_AND_NOTIFY(Bv, bvAssertInput, false, "proofs"); + SET_AND_NOTIFY_VAL_SYM(bv, bvAssertInput, false, "proofs"); } // If proofs are required and the user did not specify a specific BV solver, // we make sure to use the proof producing BITBLAST_INTERNAL solver. if (opts.smt.proofMode == options::ProofMode::FULL) { - SET_AND_NOTIFY_IF_NOT_USER( - Bv, bvSolver, options::BVSolver::BITBLAST_INTERNAL, "proofs"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM( + bv, bvSolver, options::BVSolver::BITBLAST_INTERNAL, "proofs"); } - SET_AND_NOTIFY_IF_NOT_USER(Arith, nlCovVarElim, false, "proofs"); + SET_AND_NOTIFY_IF_NOT_USER(arith, nlCovVarElim, false, "proofs"); if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) { reason << "deep restarts"; @@ -1085,7 +1089,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "unconstrained simplification"; return true; } - SET_AND_NOTIFY(Smt, unconstrainedSimp, false, "incremental solving"); + SET_AND_NOTIFY(smt, unconstrainedSimp, false, "incremental solving"); } if (opts.bv.bitblastMode == options::BitblastMode::EAGER && !logic.isPure(THEORY_BV)) @@ -1102,10 +1106,10 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "sygus inference"; return true; } - SET_AND_NOTIFY(Quantifiers, - sygusInference, - options::SygusInferenceMode::OFF, - "incremental solving"); + SET_AND_NOTIFY_VAL_SYM(quantifiers, + sygusInference, + options::SygusInferenceMode::OFF, + "incremental solving"); } if (opts.quantifiers.sygusInst) { @@ -1114,7 +1118,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "sygus inst"; return true; } - SET_AND_NOTIFY(Quantifiers, sygusInst, false, "incremental solving"); + SET_AND_NOTIFY(quantifiers, sygusInst, false, "incremental solving"); } if (opts.smt.solveIntAsBV > 0) { @@ -1133,11 +1137,11 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, } // disable modes not supported by incremental - SET_AND_NOTIFY(Smt, sortInference, false, "incremental solving"); - SET_AND_NOTIFY(Uf, ufssFairnessMonotone, false, "incremental solving"); - SET_AND_NOTIFY(Quantifiers, globalNegate, false, "incremental solving"); - SET_AND_NOTIFY(Quantifiers, cegqiNestedQE, false, "incremental solving"); - SET_AND_NOTIFY(Arith, arithMLTrick, false, "incremental solving"); + SET_AND_NOTIFY(smt, sortInference, false, "incremental solving"); + SET_AND_NOTIFY(uf, ufssFairnessMonotone, false, "incremental solving"); + SET_AND_NOTIFY(quantifiers, globalNegate, false, "incremental solving"); + SET_AND_NOTIFY(quantifiers, cegqiNestedQE, false, "incremental solving"); + SET_AND_NOTIFY(arith, arithMLTrick, false, "incremental solving"); return false; } @@ -1157,8 +1161,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "deep restarts"; return true; } - SET_AND_NOTIFY( - Smt, deepRestartMode, options::DeepRestartMode::NONE, "unsat cores"); + SET_AND_NOTIFY_VAL_SYM( + smt, deepRestartMode, options::DeepRestartMode::NONE, "unsat cores"); } if (opts.smt.learnedRewrite) { @@ -1167,7 +1171,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "learned rewrites"; return true; } - SET_AND_NOTIFY(Smt, learnedRewrite, false, "unsat cores"); + SET_AND_NOTIFY(smt, learnedRewrite, false, "unsat cores"); } // most static learning techniques are local, although arithmetic static // learning is not. @@ -1178,7 +1182,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "arith static learning"; return true; } - SET_AND_NOTIFY(Arith, arithStaticLearning, false, "unsat cores"); + SET_AND_NOTIFY(arith, arithStaticLearning, false, "unsat cores"); } if (opts.arith.pbRewrites) @@ -1188,7 +1192,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "pseudoboolean rewrites"; return true; } - SET_AND_NOTIFY(Arith, pbRewrites, false, "unsat cores"); + SET_AND_NOTIFY(arith, pbRewrites, false, "unsat cores"); } if (opts.quantifiers.globalNegate) @@ -1198,7 +1202,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "global-negate"; return true; } - SET_AND_NOTIFY(Quantifiers, globalNegate, false, "unsat cores"); + SET_AND_NOTIFY(quantifiers, globalNegate, false, "unsat cores"); } if (opts.smt.doITESimp) @@ -1266,7 +1270,7 @@ bool SetDefaults::incompatibleWithSeparationLogic(Options& opts, // conjunctions). Thus, we cannot apply BCP as a substitution for spatial // predicates to the input formula. We disable this option altogether to // ensure this is the case - SET_AND_NOTIFY(Smt, simplificationBoolConstProp, false, "separation logic"); + SET_AND_NOTIFY(smt, simplificationBoolConstProp, false, "separation logic"); return false; } @@ -1368,72 +1372,72 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, { if (opts.quantifiers.fullSaturateQuant) { - SET_AND_NOTIFY(Quantifiers, enumInst, true, "full-saturate-quant"); + SET_AND_NOTIFY(quantifiers, enumInst, true, "full-saturate-quant"); } if (opts.arrays.arraysExp) { // Allows to answer sat more often by default. - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, fmfBound, true, "arrays-exp"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, fmfBound, true, "arrays-exp"); } if (logic.hasCardinalityConstraints()) { // must have finite model finding on - SET_AND_NOTIFY(Quantifiers, + SET_AND_NOTIFY(quantifiers, finiteModelFind, true, "logic with cardinality constraints"); } if (opts.quantifiers.instMaxLevel != -1) { - SET_AND_NOTIFY(Quantifiers, cegqi, false, "instMaxLevel"); + SET_AND_NOTIFY(quantifiers, cegqi, false, "instMaxLevel"); } if (opts.quantifiers.mbqi) { // MBQI is an alternative to CEGQI/SyQI - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, cegqi, false, "mbqi"); - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, sygusInst, false, "mbqi"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, cegqi, false, "mbqi"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, sygusInst, false, "mbqi"); } if (opts.quantifiers.fmfBoundLazy) { - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, fmfBound, true, "fmfBoundLazy"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, fmfBound, true, "fmfBoundLazy"); } // now have determined whether fmfBound is on/off // apply fmfBound options if (opts.quantifiers.fmfBound) { // if bounded integers are set, use no MBQI by default - SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, fmfMbqiMode, options::FmfMbqiMode::NONE, "fmfBound"); - SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, prenexQuant, options::PrenexQuantMode::NONE, "fmfBound"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM( + quantifiers, fmfMbqiMode, options::FmfMbqiMode::NONE, "fmfBound"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM( + quantifiers, prenexQuant, options::PrenexQuantMode::NONE, "fmfBound"); } if (logic.isHigherOrder()) { // if higher-order, then current variants of model-based instantiation // cannot be used - SET_AND_NOTIFY(Quantifiers, - fmfMbqiMode, - options::FmfMbqiMode::NONE, - "higher-order logic"); + SET_AND_NOTIFY_VAL_SYM(quantifiers, + fmfMbqiMode, + options::FmfMbqiMode::NONE, + "higher-order logic"); // by default, use store axioms only if --ho-elim is set - SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(Quantifiers, + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, hoElimStoreAx, opts.quantifiers.hoElim, "higher-order logic"); // Cannot use macros, since lambda lifting and macro elimination are inverse // operations. - SET_AND_NOTIFY(Quantifiers, macrosQuant, false, "higher-order logic"); + SET_AND_NOTIFY(quantifiers, macrosQuant, false, "higher-order logic"); } if (opts.quantifiers.fmfFunWellDefinedRelevant) { SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, fmfFunWellDefined, true, "fmfFunWellDefinedRelevant"); + quantifiers, fmfFunWellDefined, true, "fmfFunWellDefinedRelevant"); } if (opts.quantifiers.fmfFunWellDefined) { SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, finiteModelFind, true, "fmfFunWellDefined"); + quantifiers, finiteModelFind, true, "fmfFunWellDefined"); } // now, have determined whether finite model find is on/off @@ -1441,21 +1445,21 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, if (opts.quantifiers.finiteModelFind) { // apply conservative quantifiers splitting - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - quantDynamicSplit, - options::QuantDSplitMode::DEFAULT, - "finiteModelFind"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + quantDynamicSplit, + options::QuantDSplitMode::DEFAULT, + "finiteModelFind"); // do not use E-matching by default. For E-matching + FMF, the user should // specify --finite-model-find --e-matching. SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, eMatching, false, "finiteModelFind"); + quantifiers, eMatching, false, "finiteModelFind"); // instantiate only on last call if (opts.quantifiers.eMatching) { - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - instWhenMode, - options::InstWhenMode::LAST_CALL, - "finiteModelFind"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + instWhenMode, + options::InstWhenMode::LAST_CALL, + "finiteModelFind"); } } @@ -1482,12 +1486,12 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, || logic.isTheoryEnabled(THEORY_FP))) || opts.quantifiers.cegqiAll) { - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, cegqi, true, "logic"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, cegqi, true, "logic"); // check whether we should apply full cbqi if (logic.isPure(THEORY_BV)) { SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, cegqiFullEffort, true, "pure BV logic"); + quantifiers, cegqiFullEffort, true, "pure BV logic"); } } if (opts.quantifiers.cegqi) @@ -1495,122 +1499,122 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV)) { SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, conflictBasedInst, false, "cegqi pure logic"); + quantifiers, conflictBasedInst, false, "cegqi pure logic"); SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, instNoEntail, false, "cegqi pure logic"); + quantifiers, instNoEntail, false, "cegqi pure logic"); // only instantiation should happen at last call when model is avaiable - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - instWhenMode, - options::InstWhenMode::LAST_CALL, - "cegqi pure logic"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + instWhenMode, + options::InstWhenMode::LAST_CALL, + "cegqi pure logic"); } else { // only supported in pure arithmetic or pure BV - SET_AND_NOTIFY(Quantifiers, cegqiNestedQE, false, "cegqi non-pure logic"); + SET_AND_NOTIFY(quantifiers, cegqiNestedQE, false, "cegqi non-pure logic"); } if (opts.quantifiers.globalNegate) { - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - prenexQuant, - options::PrenexQuantMode::NONE, - "globalNegate"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + prenexQuant, + options::PrenexQuantMode::NONE, + "globalNegate"); } } // implied options... if (opts.quantifiers.cbqiModeWasSetByUser || opts.quantifiers.cbqiTConstraint) { - SET_AND_NOTIFY(Quantifiers, conflictBasedInst, true, "cbqi option"); + SET_AND_NOTIFY(quantifiers, conflictBasedInst, true, "cbqi option"); } if (opts.quantifiers.cegqiNestedQE) { - SET_AND_NOTIFY(Quantifiers, prenexQuantUser, true, "cegqiNestedQE"); - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - preSkolemQuant, - options::PreSkolemQuantMode::ON, - "cegqiNestedQE"); + SET_AND_NOTIFY(quantifiers, prenexQuantUser, true, "cegqiNestedQE"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + preSkolemQuant, + options::PreSkolemQuantMode::ON, + "cegqiNestedQE"); } // for induction techniques if (opts.quantifiers.quantInduction) { SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, dtStcInduction, true, "quantInduction"); + quantifiers, dtStcInduction, true, "quantInduction"); SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, intWfInduction, true, "quantInduction"); + quantifiers, intWfInduction, true, "quantInduction"); } if (opts.quantifiers.dtStcInduction) { // try to remove ITEs from quantified formulas SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, iteDtTesterSplitQuant, true, "dtStcInduction"); - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - iteLiftQuant, - options::IteLiftQuantMode::ALL, - "dtStcInduction"); + quantifiers, iteDtTesterSplitQuant, true, "dtStcInduction"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + iteLiftQuant, + options::IteLiftQuantMode::ALL, + "dtStcInduction"); } if (opts.quantifiers.intWfInduction) { SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, purifyTriggers, true, "intWfInduction"); + quantifiers, purifyTriggers, true, "intWfInduction"); } if (opts.quantifiers.conjectureGenPerRoundWasSetByUser) { bool conjNZero = (opts.quantifiers.conjectureGenPerRound > 0); SET_AND_NOTIFY_VAL_SYM( - Quantifiers, conjectureGen, conjNZero, "conjectureGenPerRound"); + quantifiers, conjectureGen, conjNZero, "conjectureGenPerRound"); } // can't pre-skolemize nested quantifiers without UF theory if (!logic.isTheoryEnabled(THEORY_UF) && opts.quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF) { SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, preSkolemQuantNested, false, "preSkolemQuant"); + quantifiers, preSkolemQuantNested, false, "preSkolemQuant"); } if (!logic.isTheoryEnabled(THEORY_DATATYPES)) { - SET_AND_NOTIFY(Quantifiers, - quantDynamicSplit, - options::QuantDSplitMode::NONE, - "non-datatypes logic"); + SET_AND_NOTIFY_VAL_SYM(quantifiers, + quantDynamicSplit, + options::QuantDSplitMode::NONE, + "non-datatypes logic"); } if (opts.quantifiers.globalNegate) { - SET_AND_NOTIFY( - Smt, deepRestartMode, options::DeepRestartMode::NONE, "globalNegate"); + SET_AND_NOTIFY_VAL_SYM( + smt, deepRestartMode, options::DeepRestartMode::NONE, "globalNegate"); } } void SetDefaults::setDefaultsSygus(Options& opts) const { - SET_AND_NOTIFY(Quantifiers, sygus, true, "enabling sygus"); + SET_AND_NOTIFY(quantifiers, sygus, true, "enabling sygus"); // must use Ferrante/Rackoff for real arithmetic - SET_AND_NOTIFY(Quantifiers, cegqiMidpoint, true, "sygus"); + SET_AND_NOTIFY(quantifiers, cegqiMidpoint, true, "sygus"); // must disable cegqi-bv since it may introduce witness terms, which // cannot appear in synthesis solutions - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, cegqiBv, false, "sygus"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, cegqiBv, false, "sygus"); if (opts.quantifiers.sygusRepairConst) { - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, cegqi, true, "sygusRepairConst"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, cegqi, true, "sygusRepairConst"); } if (opts.quantifiers.sygusInference != options::SygusInferenceMode::OFF) { // optimization: apply preskolemization, makes it succeed more often - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - preSkolemQuant, - options::PreSkolemQuantMode::ON, - "sygusInference"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + preSkolemQuant, + options::PreSkolemQuantMode::ON, + "sygusInference"); SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, preSkolemQuantNested, true, "sygusInference"); + quantifiers, preSkolemQuantNested, true, "sygusInference"); } // counterexample-guided instantiation for sygus - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - cegqiSingleInvMode, - options::CegqiSingleInvMode::USE, - "sygus"); - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, conflictBasedInst, false, "sygus"); - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, instNoEntail, false, "sygus"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + cegqiSingleInvMode, + options::CegqiSingleInvMode::USE, + "sygus"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, conflictBasedInst, false, "sygus"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, instNoEntail, false, "sygus"); // should use full effort cbqi for single invocation and repair const - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, cegqiFullEffort, true, "sygus"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, cegqiFullEffort, true, "sygus"); // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm // is one that is specialized for returning a single solution. Non-basic // sygus algorithms currently include the PBE solver, UNIF+PI, static @@ -1620,10 +1624,10 @@ void SetDefaults::setDefaultsSygus(Options& opts) const if (opts.smt.produceAbducts) { // if doing abduction, we should filter strong solutions - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - sygusFilterSolMode, - options::SygusFilterSolMode::STRONG, - "produceAbducts"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + sygusFilterSolMode, + options::SygusFilterSolMode::STRONG, + "produceAbducts"); // we must use basic sygus algorithms, since e.g. we require checking // a sygus side condition for consistency with axioms. reqBasicSygus = true; @@ -1637,25 +1641,25 @@ void SetDefaults::setDefaultsSygus(Options& opts) const // Now, disable options for non-basic sygus algorithms, if necessary. if (reqBasicSygus) { - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, sygusUnifPbe, false, "basic sygus"); - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - sygusUnifPi, - options::SygusUnifPiMode::NONE, - "basic sygus"); - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - sygusInvTemplMode, - options::SygusInvTemplMode::NONE, - "basic sygus"); - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, - cegqiSingleInvMode, - options::CegqiSingleInvMode::NONE, - "basic sygus"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, sygusUnifPbe, false, "basic sygus"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + sygusUnifPi, + options::SygusUnifPiMode::NONE, + "basic sygus"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + sygusInvTemplMode, + options::SygusInvTemplMode::NONE, + "basic sygus"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers, + cegqiSingleInvMode, + options::CegqiSingleInvMode::NONE, + "basic sygus"); } // do not miniscope - SET_AND_NOTIFY_IF_NOT_USER( - Quantifiers, miniscopeQuant, options::MiniscopeQuantMode::OFF, "sygus"); + SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM( + quantifiers, miniscopeQuant, options::MiniscopeQuantMode::OFF, "sygus"); // do not do macros - SET_AND_NOTIFY_IF_NOT_USER(Quantifiers, macrosQuant, false, "sygus"); + SET_AND_NOTIFY_IF_NOT_USER(quantifiers, macrosQuant, false, "sygus"); } void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic, Options& opts) const @@ -1727,7 +1731,7 @@ void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic, Assert(decMode == options::DecisionMode::INTERNAL); } } - SET_AND_NOTIFY_VAL_SYM(Decision, decisionMode, decMode, "logic"); + SET_AND_NOTIFY_VAL_SYM(decision, decisionMode, decMode, "logic"); } void SetDefaults::notifyModifyOption(const std::string& x, @@ -1740,16 +1744,31 @@ void SetDefaults::notifyModifyOption(const std::string& x, verbose(1) << " due to " << reason; } verbose(1) << std::endl; + // don't print -o options-auto for internal subsolvers + if (!d_isInternalSubsolver) + { + if (isOutputOn(OutputTag::OPTIONS_AUTO)) + { + output(OutputTag::OPTIONS_AUTO) << "(options-auto"; + output(OutputTag::OPTIONS_AUTO) << " " << x; + output(OutputTag::OPTIONS_AUTO) << " " << val; + if (!reason.empty()) + { + output(OutputTag::OPTIONS_AUTO) << " :reason \"" << reason << "\""; + } + output(OutputTag::OPTIONS_AUTO) << ")" << std::endl; + } + } } void SetDefaults::disableChecking(Options& opts) { - opts.writeSmt().checkUnsatCores = false; - opts.writeSmt().produceProofs = false; - opts.writeSmt().checkProofs = false; - opts.writeSmt().debugCheckModels = false; - opts.writeSmt().checkModels = false; - opts.writeProof().checkProofSteps = false; + opts.write_smt().checkUnsatCores = false; + opts.write_smt().produceProofs = false; + opts.write_smt().checkProofs = false; + opts.write_smt().debugCheckModels = false; + opts.write_smt().checkModels = false; + opts.write_proof().checkProofSteps = false; } } // namespace smt diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 68ce3bc36ab..0d08e6b0f12 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -342,7 +342,7 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value) if (key == "filename") { - d_env->d_options.writeDriver().filename = value; + d_env->d_options.write_driver().filename = value; d_env->getStatisticsRegistry().registerValue( "driver::filename", value); } @@ -355,12 +355,12 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value) << " unsupported, defaulting to language (and semantics of) " "SMT-LIB 2.6\n"; } - getOptions().writeBase().inputLanguage = Language::LANG_SMTLIB_V2_6; + getOptions().write_base().inputLanguage = Language::LANG_SMTLIB_V2_6; // also update the output language if (!getOptions().printer.outputLanguageWasSetByUser) { setOption("output-language", "smtlib2.6"); - getOptions().writePrinter().outputLanguageWasSetByUser = false; + getOptions().write_printer().outputLanguageWasSetByUser = false; } } else if (key == "status") @@ -2038,16 +2038,16 @@ void SolverEngine::setResourceLimit(uint64_t units, bool cumulative) { if (cumulative) { - d_env->d_options.writeBase().cumulativeResourceLimit = units; + d_env->d_options.write_base().cumulativeResourceLimit = units; } else { - d_env->d_options.writeBase().perCallResourceLimit = units; + d_env->d_options.write_base().perCallResourceLimit = units; } } void SolverEngine::setTimeLimit(uint64_t millis) { - d_env->d_options.writeBase().perCallMillisecondLimit = millis; + d_env->d_options.write_base().perCallMillisecondLimit = millis; } unsigned long SolverEngine::getResourceUsage() const diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 3706d1eba64..42d371f91c6 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -435,8 +435,8 @@ void SygusSolver::checkSynthSolution(Assertions& as, // Start new SMT engine to check solutions std::unique_ptr solChecker; initializeSygusSubsolver(solChecker, as); - solChecker->getOptions().writeSmt().checkSynthSol = false; - solChecker->getOptions().writeQuantifiers().sygusRecFun = false; + solChecker->getOptions().write_smt().checkSynthSol = false; + solChecker->getOptions().write_quantifiers().sygusRecFun = false; Assert(conj.getKind() == Kind::FORALL); Node conjBody = conj[1]; // we must apply substitutions here, since define-fun may contain the diff --git a/src/theory/quantifiers/inst_strategy_sub_conflict.cpp b/src/theory/quantifiers/inst_strategy_sub_conflict.cpp index 8a028e06b9d..896fb6bb13e 100644 --- a/src/theory/quantifiers/inst_strategy_sub_conflict.cpp +++ b/src/theory/quantifiers/inst_strategy_sub_conflict.cpp @@ -39,15 +39,15 @@ InstStrategySubConflict::InstStrategySubConflict( // we start with the provided options d_subOptions.copyValues(options()); // requires full proofs - d_subOptions.writeSmt().produceProofs = true; + d_subOptions.write_smt().produceProofs = true; // don't do simplification, which can preprocess quantifiers to those not // occurring in the main solver - d_subOptions.writeSmt().simplificationMode = + d_subOptions.write_smt().simplificationMode = options::SimplificationMode::NONE; // requires unsat cores - d_subOptions.writeSmt().produceUnsatCores = true; + d_subOptions.write_smt().produceUnsatCores = true; // don't do this strategy - d_subOptions.writeQuantifiers().quantSubCbqi = false; + d_subOptions.write_quantifiers().quantSubCbqi = false; } void InstStrategySubConflict::reset_round(Theory::Effort e) {} diff --git a/src/theory/quantifiers/query_generator_unsat.cpp b/src/theory/quantifiers/query_generator_unsat.cpp index 4ffa1c8bfb5..bc9d1ecf808 100644 --- a/src/theory/quantifiers/query_generator_unsat.cpp +++ b/src/theory/quantifiers/query_generator_unsat.cpp @@ -32,11 +32,11 @@ QueryGeneratorUnsat::QueryGeneratorUnsat(Env& env) : QueryGenerator(env) // determine the options to use for the verification subsolvers we spawn // we start with the provided options d_subOptions.copyValues(d_env.getOptions()); - d_subOptions.writeQuantifiers().sygus = false; - d_subOptions.writeSmt().produceProofs = true; - d_subOptions.writeSmt().checkProofs = true; - d_subOptions.writeSmt().produceModels = true; - d_subOptions.writeSmt().checkModels = true; + d_subOptions.write_quantifiers().sygus = false; + d_subOptions.write_smt().produceProofs = true; + d_subOptions.write_smt().checkProofs = true; + d_subOptions.write_smt().produceModels = true; + d_subOptions.write_smt().checkModels = true; } bool QueryGeneratorUnsat::addTerm(Node n, std::vector& queries) diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 57817735e4b..3a78555bddc 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -361,7 +361,7 @@ bool SygusInterpol::solveInterpolation(const std::string& name, Options subOptions; subOptions.copyValues(d_env.getOptions()); - subOptions.writeQuantifiers().sygus = true; + subOptions.write_quantifiers().sygus = true; smt::SetDefaults::disableChecking(subOptions); SubsolverSetupInfo ssi(d_env, subOptions); initializeSubsolver(d_subSolver, ssi); diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp index c083760c997..7a544adbb91 100644 --- a/src/theory/quantifiers/sygus/synth_verify.cpp +++ b/src/theory/quantifiers/sygus/synth_verify.cpp @@ -40,24 +40,24 @@ SynthVerify::SynthVerify(Env& env, TermDbSygus* tds) // we start with the provided options d_subOptions.copyValues(options()); // limit the number of instantiation rounds on subcalls - d_subOptions.writeQuantifiers().instMaxRounds = + d_subOptions.write_quantifiers().instMaxRounds = d_subOptions.quantifiers.sygusVerifyInstMaxRounds; // Disable sygus on the subsolver. This is particularly important since it // ensures that recursive function definitions have the standard ownership // instead of being claimed by sygus in the subsolver. - d_subOptions.writeBase().inputLanguage = Language::LANG_SMTLIB_V2_6; - d_subOptions.writeQuantifiers().sygus = false; + d_subOptions.write_base().inputLanguage = Language::LANG_SMTLIB_V2_6; + d_subOptions.write_quantifiers().sygus = false; // use tangent planes by default, since we want to put effort into // the verification step for sygus queries with non-linear arithmetic if (!d_subOptions.arith.nlExtTangentPlanesWasSetByUser) { - d_subOptions.writeArith().nlExtTangentPlanes = true; + d_subOptions.write_arith().nlExtTangentPlanes = true; } // we must use the same setting for datatype selectors, since shared selectors // can appear in solutions - d_subOptions.writeDatatypes().dtSharedSelectors = + d_subOptions.write_datatypes().dtSharedSelectors = options().datatypes.dtSharedSelectors; - d_subOptions.writeDatatypes().dtSharedSelectorsWasSetByUser = true; + d_subOptions.write_datatypes().dtSharedSelectorsWasSetByUser = true; // disable checking smt::SetDefaults::disableChecking(d_subOptions); } diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 6a455e33b35..cd595868f73 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1266,6 +1266,7 @@ set(regress_0_tests regress0/printer/portfolio-out-err.smt2 regress0/printer/post-asserts-output.smt2 regress0/printer/pre-asserts-output.smt2 + regress0/printer/print_options_auto.smt2 regress0/printer/print_sat_lemmas.smt2 regress0/printer/print_subs.smt2 regress0/printer/print_trusted_proof_steps.smt2 diff --git a/test/regress/cli/regress0/printer/print_options_auto.smt2 b/test/regress/cli/regress0/printer/print_options_auto.smt2 new file mode 100644 index 00000000000..e62c7cbeedb --- /dev/null +++ b/test/regress/cli/regress0/printer/print_options_auto.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: -o options-auto +; SCRUBBER: sed -e 's/(options-auto.*//' +; EXPECT: sat +(set-logic QF_LRA) +(assert true) +(check-sat) diff --git a/test/unit/theory/theory_arith_coverings_white.cpp b/test/unit/theory/theory_arith_coverings_white.cpp index 4d1fafc19f2..b40dd054ac4 100644 --- a/test/unit/theory/theory_arith_coverings_white.cpp +++ b/test/unit/theory/theory_arith_coverings_white.cpp @@ -384,8 +384,8 @@ TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_proof_1) { Options opts; // enable proofs - opts.writeSmt().proofMode = options::ProofMode::FULL; - opts.writeSmt().produceProofs = true; + opts.write_smt().proofMode = options::ProofMode::FULL; + opts.write_smt().produceProofs = true; Env env(d_nodeManager, &opts); smt::PfManager pfm(env); env.finishInit(pfm.getProofNodeManager());