diff options
| -rw-r--r-- | src/options/mkoptions.py | 23 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 4 | ||||
| -rw-r--r-- | src/options/options_public.cpp | 8 | ||||
| -rw-r--r-- | src/options/options_template.h | 9 | ||||
| -rw-r--r-- | src/printer/printer.cpp | 4 | ||||
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 2 | ||||
| -rw-r--r-- | src/smt/options_manager.cpp | 14 | ||||
| -rw-r--r-- | src/smt/set_defaults.cpp | 204 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 |
11 files changed, 128 insertions, 148 deletions
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 73de9209b..7e1cf68e4 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -75,7 +75,7 @@ void assign_{module}_{name}(Options& opts, const std::string& option, const std: auto value = {handler}; {predicates} opts.{module}.{name} = value; - opts.{module}.{name}__setByUser = true; + opts.{module}.{name}WasSetByUser = true; Trace("options") << "user assigned option {name} = " << value << std::endl; }}''' @@ -83,7 +83,7 @@ TPL_ASSIGN_BOOL = ''' void assign_{module}_{name}(Options& opts, const std::string& option, bool value) {{ {predicates} opts.{module}.{name} = value; - opts.{module}.{name}__setByUser = true; + opts.{module}.{name}WasSetByUser = true; Trace("options") << "user assigned option {name} = " << value << std::endl; }}''' @@ -95,15 +95,15 @@ TPL_CALL_SET_OPTION = 'setOption(std::string("{smtname}"), ("{value}"));' TPL_GETOPT_LONG = '{{ "{}", {}_argument, nullptr, {} }},' TPL_HOLDER_MACRO_ATTR = ''' {type} {name}; - bool {name}__setByUser = false;''' + bool {name}WasSetByUser = false;''' TPL_HOLDER_MACRO_ATTR_DEF = ''' {type} {name} = {default}; - bool {name}__setByUser = false;''' + bool {name}WasSetByUser = false;''' TPL_DECL_SET_DEFAULT = 'void setDefault{funcname}(Options& opts, {type} value);' TPL_IMPL_SET_DEFAULT = TPL_DECL_SET_DEFAULT[:-1] + ''' {{ - if (!opts.{module}.{name}__setByUser) {{ + if (!opts.{module}.{name}WasSetByUser) {{ opts.{module}.{name} = value; }} }}''' @@ -117,15 +117,6 @@ TPL_OPTION_STRUCT_RW = \ type operator()() const; }} thread_local {name};""" -TPL_DECL_WAS_SET_BY_USER = \ -"""template <> bool Options::wasSetByUser(options::{name}__option_t) const;""" - -TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \ -""" -{{ - return {module}.{name}__setByUser; -}}""" - # Option specific methods TPL_IMPL_OP_PAR = \ @@ -556,7 +547,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): # Generate module specialization default_decl.append(TPL_DECL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type)) - specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name)) if option.long and option.type not in ['bool', 'void'] and \ '=' not in option.long: @@ -577,7 +567,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): # Accessors default_impl.append(TPL_IMPL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type)) - accs.append(TPL_IMPL_WAS_SET_BY_USER.format(module=module.id, name=option.name)) # Global definitions defs.append('thread_local struct {name}__option_t {name};'.format(name=option.name)) @@ -925,7 +914,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ if option.mode and option.type not in default: default = '{}::{}'.format(option.type, default) defaults.append('{}({})'.format(option.name, default)) - defaults.append('{}__setByUser(false)'.format(option.name)) + defaults.append('{}WasSetByUser(false)'.format(option.name)) write_file(dst_dir, 'options.h', tpl_options_h.format( holder_fwd_decls=get_holder_fwd_decls(modules), diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 1178f205d..d06c64517 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -159,7 +159,7 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) || m == SatSolverMode::KISSAT)) { if (options::bitblastMode() == options::BitblastMode::LAZY - && Options::current().wasSetByUser(options::bitblastMode)) + && d_options->bv.bitblastModeWasSetByUser) { throwLazyBBUnsupported(m); } @@ -189,7 +189,7 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) void OptionsHandler::setBitblastAig(std::string option, bool arg) { if(arg) { - if(Options::current().wasSetByUser(options::bitblastMode)) { + if (d_options->bv.bitblastModeWasSetByUser) { if (options::bitblastMode() != options::BitblastMode::EAGER) { throw OptionException("bitblast-aig must be used with eager bitblaster"); diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp index f590ba083..7d72496aa 100644 --- a/src/options/options_public.cpp +++ b/src/options/options_public.cpp @@ -120,19 +120,19 @@ void setOutputLanguage(OutputLanguage val, Options& opts) bool wasSetByUserEarlyExit(const Options& opts) { - return opts.driver.earlyExit__setByUser; + return opts.driver.earlyExitWasSetByUser; } bool wasSetByUserForceLogicString(const Options& opts) { - return opts.parser.forceLogicString__setByUser; + return opts.parser.forceLogicStringWasSetByUser; } bool wasSetByUserIncrementalSolving(const Options& opts) { - return opts.smt.incrementalSolving__setByUser; + return opts.smt.incrementalSolvingWasSetByUser; } bool wasSetByUserInteractive(const Options& opts) { - return opts.driver.interactive__setByUser; + return opts.driver.interactiveWasSetByUser; } } // namespace cvc5::options diff --git a/src/options/options_template.h b/src/options/options_template.h index 6ce77d7a1..76c599d23 100644 --- a/src/options/options_template.h +++ b/src/options/options_template.h @@ -137,15 +137,6 @@ public: static std::ostream* currentGetOut(); /** - * Returns true iff the value of the given option was set - * by the user via a command-line option or SmtEngine::setOption(). - * (Options::set() is low-level and doesn't count.) Returns false - * otherwise. - */ - template <class T> - bool wasSetByUser(T) const; - - /** * Get a description of the command-line flags accepted by * parseOptions. The returned string will be escaped so that it is * suitable as an argument to printf. */ diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 048f5d06b..b733f62ce 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -135,12 +135,12 @@ Printer* Printer::getPrinter(OutputLanguage lang) // the singleton "null" expr. So we guard against segfault if (not Options::isCurrentNull()) { - if (Options::current().wasSetByUser(options::outputLanguage)) + if (Options::current().base.outputLanguageWasSetByUser) { lang = options::outputLanguage(); } if (lang == language::output::LANG_AUTO - && Options::current().wasSetByUser(options::inputLanguage)) + && Options::current().base.inputLanguageWasSetByUser) { lang = language::toOutputLanguage(options::inputLanguage()); } diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 74cbadfc2..04db5e3cb 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -76,7 +76,7 @@ SimpSolver::SimpSolver(cvc5::prop::TheoryProxy* proxy, n_touched(0) { if(options::minisatUseElim() && - Options::current().wasSetByUser(options::minisatUseElim) && + Options::current().prop.minisatUseElimWasSetByUser && enableIncremental) { WarningOnce() << "Incremental mode incompatible with --minisat-elim" << std::endl; } diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 37541751e..4d6be68b8 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -31,31 +31,31 @@ namespace smt { OptionsManager::OptionsManager(Options* opts) : d_options(opts) { // set options that must take effect immediately - if (opts->wasSetByUser(options::defaultExprDepth)) + if (opts->expr.defaultExprDepthWasSetByUser) { notifySetOption(options::expr::defaultExprDepth__name); } - if (opts->wasSetByUser(options::defaultDagThresh)) + if (opts->expr.defaultDagThreshWasSetByUser) { notifySetOption(options::expr::defaultDagThresh__name); } - if (opts->wasSetByUser(options::dumpModeString)) + if (opts->smt.dumpModeStringWasSetByUser) { notifySetOption(options::smt::dumpModeString__name); } - if (opts->wasSetByUser(options::printSuccess)) + if (opts->base.printSuccessWasSetByUser) { notifySetOption(options::base::printSuccess__name); } - if (opts->wasSetByUser(options::diagnosticChannelName)) + if (opts->smt.diagnosticChannelNameWasSetByUser) { notifySetOption(options::smt::diagnosticChannelName__name); } - if (opts->wasSetByUser(options::regularChannelName)) + if (opts->smt.regularChannelNameWasSetByUser) { notifySetOption(options::smt::regularChannelName__name); } - if (opts->wasSetByUser(options::dumpToFileName)) + if (opts->smt.dumpToFileNameWasSetByUser) { notifySetOption(options::smt::dumpToFileName__name); } diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 96081e97b..b9095c91b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -77,7 +77,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::unsatCores() && options::unsatCoresMode() == options::UnsatCoresMode::OFF) { - if (opts.wasSetByUser(options::unsatCoresMode)) + if (opts.smt.unsatCoresModeWasSetByUser) { Notice() << "Overriding OFF unsat-core mode since cores were requested.\n"; @@ -93,7 +93,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::produceProofs() && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) { - if (opts.wasSetByUser(options::unsatCoresMode)) + if (opts.smt.unsatCoresModeWasSetByUser) { Notice() << "Forcing full-proof mode for unsat cores mode since proofs " "were requested.\n"; @@ -106,7 +106,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // set proofs on if not yet set if (options::unsatCores() && !options::produceProofs()) { - if (opts.wasSetByUser(options::produceProofs)) + if (opts.smt.produceProofsWasSetByUser) { Notice() << "Forcing proof production since new unsat cores were requested.\n"; @@ -118,12 +118,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Assert(options::unsatCores() == (options::unsatCoresMode() != options::UnsatCoresMode::OFF)); - if (opts.wasSetByUser(options::bitvectorAigSimplifications)) + if (opts.bv.bitvectorAigSimplificationsWasSetByUser) { Notice() << "SmtEngine: setting bitvectorAig" << std::endl; opts.bv.bitvectorAig = true; } - if (opts.wasSetByUser(options::bitvectorAlgebraicBudget)) + if (opts.bv.bitvectorAlgebraicBudgetWasSetByUser) { Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl; opts.bv.bitvectorAlgebraicSolver = true; @@ -138,8 +138,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) && (logic.isTheoryEnabled(THEORY_ARRAYS) || logic.isTheoryEnabled(THEORY_UF))) { - if (opts.wasSetByUser(options::bitblastMode) - || opts.wasSetByUser(options::produceModels)) + if (opts.bv.bitblastModeWasSetByUser + || opts.smt.produceModelsWasSetByUser) { throw OptionException(std::string( "Eager bit-blasting currently does not support model generation " @@ -228,7 +228,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) && (logic.isTheoryEnabled(THEORY_ARRAYS) || logic.isTheoryEnabled(THEORY_UF))) { - if (opts.wasSetByUser(options::produceModels)) + if (opts.smt.produceModelsWasSetByUser) { throw OptionException(std::string( "Ackermannization currently does not support model generation.")); @@ -271,7 +271,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // this by default. if (options::doITESimp()) { - if (!opts.wasSetByUser(options::earlyIteRemoval)) + if (!opts.smt.earlyIteRemovalWasSetByUser) { opts.smt.earlyIteRemoval = true; } @@ -298,7 +298,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << std::endl; } // We require bounded quantifier handling. - if (!opts.wasSetByUser(options::fmfBound)) + if (!opts.quantifiers.fmfBoundWasSetByUser) { opts.quantifiers.fmfBound = true; Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; @@ -320,7 +320,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) { // no fine-graininess - if (!opts.wasSetByUser(options::proofGranularityMode)) + if (!opts.proof.proofGranularityModeWasSetByUser) { opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF; } @@ -335,7 +335,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) logic.lock(); } // Allows to answer sat more often by default. - if (!opts.wasSetByUser(options::fmfBound)) + if (!opts.quantifiers.fmfBoundWasSetByUser) { opts.quantifiers.fmfBound = true; Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl; @@ -424,7 +424,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::unconstrainedSimp()) { - if (opts.wasSetByUser(options::unconstrainedSimp)) + if (opts.smt.unconstrainedSimpWasSetByUser) { throw OptionException( "unconstrained simplification not supported with old unsat " @@ -439,7 +439,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) else { // Turn on unconstrained simplification for QF_AUFBV - if (!opts.wasSetByUser(options::unconstrainedSimp)) + if (!opts.smt.unconstrainedSimpWasSetByUser) { bool uncSimp = !logic.isQuantified() && !options::produceModels() && !options::produceAssignments() @@ -457,7 +457,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::sygusInference()) { - if (opts.wasSetByUser(options::sygusInference)) + if (opts.quantifiers.sygusInferenceWasSetByUser) { throw OptionException( "sygus inference not supported with incremental solving"); @@ -486,7 +486,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::simplificationMode() != options::SimplificationMode::NONE) { - if (opts.wasSetByUser(options::simplificationMode)) + if (opts.smt.simplificationModeWasSetByUser) { throw OptionException( "simplification not supported with old unsat cores"); @@ -499,7 +499,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::pbRewrites()) { - if (opts.wasSetByUser(options::pbRewrites)) + if (opts.arith.pbRewritesWasSetByUser) { throw OptionException( "pseudoboolean rewrites not supported with old unsat cores"); @@ -511,7 +511,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::sortInference()) { - if (opts.wasSetByUser(options::sortInference)) + if (opts.smt.sortInferenceWasSetByUser) { throw OptionException( "sort inference not supported with old unsat cores"); @@ -523,7 +523,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::preSkolemQuant()) { - if (opts.wasSetByUser(options::preSkolemQuant)) + if (opts.quantifiers.preSkolemQuantWasSetByUser) { throw OptionException( "pre-skolemization not supported with old unsat cores"); @@ -535,7 +535,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::bitvectorToBool()) { - if (opts.wasSetByUser(options::bitvectorToBool)) + if (opts.bv.bitvectorToBoolWasSetByUser) { throw OptionException("bv-to-bool not supported with old unsat cores"); } @@ -546,7 +546,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::boolToBitvector() != options::BoolToBVMode::OFF) { - if (opts.wasSetByUser(options::boolToBitvector)) + if (opts.bv.boolToBitvectorWasSetByUser) { throw OptionException( "bool-to-bv != off not supported with old unsat cores"); @@ -558,7 +558,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::bvIntroducePow2()) { - if (opts.wasSetByUser(options::bvIntroducePow2)) + if (opts.bv.bvIntroducePow2WasSetByUser) { throw OptionException( "bv-intro-pow2 not supported with old unsat cores"); @@ -570,7 +570,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::repeatSimp()) { - if (opts.wasSetByUser(options::repeatSimp)) + if (opts.smt.repeatSimpWasSetByUser) { throw OptionException("repeat-simp not supported with old unsat cores"); } @@ -581,7 +581,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::globalNegate()) { - if (opts.wasSetByUser(options::globalNegate)) + if (opts.quantifiers.globalNegateWasSetByUser) { throw OptionException( "global-negate not supported with old unsat cores"); @@ -604,7 +604,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) else { // by default, nonclausal simplification is off for QF_SAT - if (!opts.wasSetByUser(options::simplificationMode)) + if (!opts.smt.simplificationModeWasSetByUser) { bool qf_sat = logic.isPure(THEORY_BOOL) && !logic.isQuantified(); Trace("smt") << "setting simplification mode to <" @@ -623,7 +623,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::boolToBitvector() != options::BoolToBVMode::OFF) { - if (opts.wasSetByUser(options::boolToBitvector)) + if (opts.bv.boolToBitvectorWasSetByUser) { throw OptionException( "bool-to-bv != off not supported with CBQI BV for quantified " @@ -682,7 +682,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) needsUf = true; } else if (options::preSkolemQuantNested() - && opts.wasSetByUser(options::preSkolemQuantNested)) + && opts.quantifiers.preSkolemQuantNestedWasSetByUser) { // if pre-skolem nested is explictly set, then we require UF. If it is // not explicitly set, it is disabled below if UF is not present. @@ -737,7 +737,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) ///////////////////////////////////////////////////////////////////////////// // Set the options for the theoryOf - if (!opts.wasSetByUser(options::theoryOfMode)) + if (!opts.theory.theoryOfModeWasSetByUser) { if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV) && !logic.isTheoryEnabled(THEORY_STRINGS) @@ -752,7 +752,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // by default, symmetry breaker is on only for non-incremental QF_UF - if (!opts.wasSetByUser(options::ufSymmetryBreaker)) + if (!opts.uf.ufSymmetryBreakerWasSetByUser) { bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified() && !options::incrementalSolving() && !safeUnsatCores; @@ -774,7 +774,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Theory::setUninterpretedSortOwner(THEORY_UF); } - if (!opts.wasSetByUser(options::simplifyWithCareEnabled)) + if (!opts.smt.simplifyWithCareEnabledWasSetByUser) { bool qf_aufbv = !logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS) @@ -786,7 +786,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.simplifyWithCareEnabled = withCare; } // Turn off array eager index splitting for QF_AUFLIA - if (!opts.wasSetByUser(options::arraysEagerIndexSplitting)) + if (!opts.arrays.arraysEagerIndexSplittingWasSetByUser) { if (not logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS) && logic.isTheoryEnabled(THEORY_UF) @@ -798,7 +798,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } // Turn on multiple-pass non-clausal simplification for QF_AUFBV - if (!opts.wasSetByUser(options::repeatSimp)) + if (!opts.smt.repeatSimpWasSetByUser) { bool repeatSimp = !logic.isQuantified() && (logic.isTheoryEnabled(THEORY_ARRAYS) @@ -813,7 +813,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::boolToBitvector() == options::BoolToBVMode::ALL && !logic.isTheoryEnabled(THEORY_BV)) { - if (opts.wasSetByUser(options::boolToBitvector)) + if (opts.bv.boolToBitvectorWasSetByUser) { throw OptionException( "bool-to-bv=all not supported for non-bitvector logics."); @@ -823,7 +823,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.bv.boolToBitvector = options::BoolToBVMode::OFF; } - if (!opts.wasSetByUser(options::bvEagerExplanations) + if (!opts.bv.bvEagerExplanationsWasSetByUser && logic.isTheoryEnabled(THEORY_ARRAYS) && logic.isTheoryEnabled(THEORY_BV)) { @@ -832,7 +832,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // Turn on arith rewrite equalities only for pure arithmetic - if (!opts.wasSetByUser(options::arithRewriteEq)) + if (!opts.arith.arithRewriteEqWasSetByUser) { bool arithRewriteEq = logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified(); @@ -840,7 +840,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << std::endl; opts.arith.arithRewriteEq = arithRewriteEq; } - if (!opts.wasSetByUser(options::arithHeuristicPivots)) + if (!opts.arith.arithHeuristicPivotsWasSetByUser) { int16_t heuristicPivots = 5; if (logic.isPure(THEORY_ARITH) && !logic.isQuantified()) @@ -858,7 +858,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << std::endl; opts.arith.arithHeuristicPivots = heuristicPivots; } - if (!opts.wasSetByUser(options::arithPivotThreshold)) + if (!opts.arith.arithPivotThresholdWasSetByUser) { uint16_t pivotThreshold = 2; if (logic.isPure(THEORY_ARITH) && !logic.isQuantified()) @@ -872,7 +872,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << std::endl; opts.arith.arithPivotThreshold = pivotThreshold; } - if (!opts.wasSetByUser(options::arithStandardCheckVarOrderPivots)) + if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser) { int16_t varOrderPivots = -1; if (logic.isPure(THEORY_ARITH) && !logic.isQuantified()) @@ -885,7 +885,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed()) { - if (!opts.wasSetByUser(options::nlExtTangentPlanesInterleave)) + if (!opts.arith.nlExtTangentPlanesInterleaveWasSetByUser) { Trace("smt") << "setting nlExtTangentPlanesInterleave to true" << std::endl; @@ -894,7 +894,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // Set decision mode based on logic (if not set by user) - if (!opts.wasSetByUser(options::decisionMode)) + if (!opts.decision.decisionModeWasSetByUser) { options::DecisionMode decMode = // anything that uses sygus uses internal @@ -974,8 +974,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.cegqi = false; } - if ((opts.wasSetByUser(options::fmfBoundLazy) && options::fmfBoundLazy()) - || (opts.wasSetByUser(options::fmfBoundInt) && options::fmfBoundInt())) + if ((opts.quantifiers.fmfBoundLazyWasSetByUser && options::fmfBoundLazy()) + || (opts.quantifiers.fmfBoundIntWasSetByUser && options::fmfBoundInt())) { opts.quantifiers.fmfBound = true; } @@ -983,14 +983,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // apply fmfBoundInt options if (options::fmfBound()) { - if (!opts.wasSetByUser(options::mbqiMode) + if (!opts.quantifiers.mbqiModeWasSetByUser || (options::mbqiMode() != options::MbqiMode::NONE && options::mbqiMode() != options::MbqiMode::FMC)) { // if bounded integers are set, use no MBQI by default opts.quantifiers.mbqiMode = options::MbqiMode::NONE; } - if (!opts.wasSetByUser(options::prenexQuant)) + if (!opts.quantifiers.prenexQuantUserWasSetByUser) { opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE; } @@ -1003,7 +1003,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { opts.quantifiers.mbqiMode = options::MbqiMode::NONE; } - if (!opts.wasSetByUser(options::hoElimStoreAx)) + if (!opts.quantifiers.hoElimStoreAxWasSetByUser) { // by default, use store axioms only if --ho-elim is set opts.quantifiers.hoElimStoreAx = options::hoElim(); @@ -1022,14 +1022,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (options::fmfFunWellDefinedRelevant()) { - if (!opts.wasSetByUser(options::fmfFunWellDefined)) + if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser) { opts.quantifiers.fmfFunWellDefined = true; } } if (options::fmfFunWellDefined()) { - if (!opts.wasSetByUser(options::finiteModelFind)) + if (!opts.quantifiers.finiteModelFindWasSetByUser) { opts.quantifiers.finiteModelFind = true; } @@ -1040,15 +1040,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::finiteModelFind()) { // apply conservative quantifiers splitting - if (!opts.wasSetByUser(options::quantDynamicSplit)) + if (!opts.quantifiers.quantDynamicSplitWasSetByUser) { opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::DEFAULT; } - if (!opts.wasSetByUser(options::eMatching)) + if (!opts.quantifiers.eMatchingWasSetByUser) { opts.quantifiers.eMatching = options::fmfInstEngine(); } - if (!opts.wasSetByUser(options::instWhenMode)) + if (!opts.quantifiers.instWhenModeWasSetByUser) { // instantiate only on last call if (options::eMatching()) @@ -1068,19 +1068,19 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } opts.quantifiers.sygus = true; // must use Ferrante/Rackoff for real arithmetic - if (!opts.wasSetByUser(options::cegqiMidpoint)) + if (!opts.quantifiers.cegqiMidpointWasSetByUser) { opts.quantifiers.cegqiMidpoint = true; } // must disable cegqi-bv since it may introduce witness terms, which // cannot appear in synthesis solutions - if (!opts.wasSetByUser(options::cegqiBv)) + if (!opts.quantifiers.cegqiBvWasSetByUser) { opts.quantifiers.cegqiBv = false; } if (options::sygusRepairConst()) { - if (!opts.wasSetByUser(options::cegqi)) + if (!opts.quantifiers.cegqiWasSetByUser) { opts.quantifiers.cegqi = true; } @@ -1088,29 +1088,29 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::sygusInference()) { // optimization: apply preskolemization, makes it succeed more often - if (!opts.wasSetByUser(options::preSkolemQuant)) + if (!opts.quantifiers.preSkolemQuantWasSetByUser) { opts.quantifiers.preSkolemQuant = true; } - if (!opts.wasSetByUser(options::preSkolemQuantNested)) + if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) { opts.quantifiers.preSkolemQuantNested = true; } } // counterexample-guided instantiation for sygus - if (!opts.wasSetByUser(options::cegqiSingleInvMode)) + if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) { opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE; } - if (!opts.wasSetByUser(options::quantConflictFind)) + if (!opts.quantifiers.quantConflictFindWasSetByUser) { opts.quantifiers.quantConflictFind = false; } - if (!opts.wasSetByUser(options::instNoEntail)) + if (!opts.quantifiers.instNoEntailWasSetByUser) { opts.quantifiers.instNoEntail = false; } - if (!opts.wasSetByUser(options::cegqiFullEffort)) + if (!opts.quantifiers.cegqiFullEffortWasSetByUser) { // should use full effort cbqi for single invocation and repair const opts.quantifiers.cegqiFullEffort = true; @@ -1128,7 +1128,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.sygusRewSynth = true; // we should not use the extended rewriter, since we are interested // in rewrites that are not in the main rewriter - if (!opts.wasSetByUser(options::sygusExtRew)) + if (!opts.quantifiers.sygusExtRewWasSetByUser) { opts.quantifiers.sygusExtRew = false; } @@ -1142,7 +1142,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::produceAbducts()) { // if doing abduction, we should filter strong solutions - if (!opts.wasSetByUser(options::sygusFilterSolMode)) + if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) { opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG; } @@ -1165,48 +1165,48 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // Now, disable options for non-basic sygus algorithms, if necessary. if (reqBasicSygus) { - if (!opts.wasSetByUser(options::sygusUnifPbe)) + if (!opts.quantifiers.sygusUnifPbeWasSetByUser) { opts.quantifiers.sygusUnifPbe = false; } - if (opts.wasSetByUser(options::sygusUnifPi)) + if (opts.quantifiers.sygusUnifPiWasSetByUser) { opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE; } - if (!opts.wasSetByUser(options::sygusInvTemplMode)) + if (!opts.quantifiers.sygusInvTemplModeWasSetByUser) { opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE; } - if (!opts.wasSetByUser(options::cegqiSingleInvMode)) + if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) { opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE; } } - if (!opts.wasSetByUser(options::dtRewriteErrorSel)) + if (!opts.datatypes.dtRewriteErrorSelWasSetByUser) { opts.datatypes.dtRewriteErrorSel = true; } // do not miniscope - if (!opts.wasSetByUser(options::miniscopeQuant)) + if (!opts.quantifiers.miniscopeQuantWasSetByUser) { opts.quantifiers.miniscopeQuant = false; } - if (!opts.wasSetByUser(options::miniscopeQuantFreeVar)) + if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser) { opts.quantifiers.miniscopeQuantFreeVar = false; } - if (!opts.wasSetByUser(options::quantSplit)) + if (!opts.quantifiers.quantSplitWasSetByUser) { opts.quantifiers.quantSplit = false; } // do not do macros - if (!opts.wasSetByUser(options::macrosQuant)) + if (!opts.quantifiers.macrosQuantWasSetByUser) { opts.quantifiers.macrosQuant = false; } // use tangent planes by default, since we want to put effort into // the verification step for sygus queries with non-linear arithmetic - if (!opts.wasSetByUser(options::nlExtTangentPlanes)) + if (!opts.arith.nlExtTangentPlanesWasSetByUser) { opts.arith.nlExtTangentPlanes = true; } @@ -1220,14 +1220,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || logic.isTheoryEnabled(THEORY_FP))) || options::cegqiAll()) { - if (!opts.wasSetByUser(options::cegqi)) + if (!opts.quantifiers.cegqiWasSetByUser) { opts.quantifiers.cegqi = true; } // check whether we should apply full cbqi if (logic.isPure(THEORY_BV)) { - if (!opts.wasSetByUser(options::cegqiFullEffort)) + if (!opts.quantifiers.cegqiFullEffortWasSetByUser) { opts.quantifiers.cegqiFullEffort = true; } @@ -1242,15 +1242,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV)) { - if (!opts.wasSetByUser(options::quantConflictFind)) + if (!opts.quantifiers.quantConflictFindWasSetByUser) { opts.quantifiers.quantConflictFind = false; } - if (!opts.wasSetByUser(options::instNoEntail)) + if (!opts.quantifiers.instNoEntailWasSetByUser) { opts.quantifiers.instNoEntail = false; } - if (!opts.wasSetByUser(options::instWhenMode) && options::cegqiModel()) + if (!opts.quantifiers.instWhenModeWasSetByUser && options::cegqiModel()) { // only instantiation should happen at last call when model is avaiable opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; @@ -1263,7 +1263,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (options::globalNegate()) { - if (!opts.wasSetByUser(options::prenexQuant)) + if (!opts.quantifiers.prenexQuantWasSetByUser) { opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE; } @@ -1272,19 +1272,19 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // implied options... if (options::strictTriggers()) { - if (!opts.wasSetByUser(options::userPatternsQuant)) + if (!opts.quantifiers.userPatternsQuantWasSetByUser) { opts.quantifiers.userPatternsQuant = options::UserPatMode::TRUST; } } - if (opts.wasSetByUser(options::qcfMode) || options::qcfTConstraint()) + if (opts.quantifiers.qcfModeWasSetByUser || options::qcfTConstraint()) { opts.quantifiers.quantConflictFind = true; } if (options::cegqiNestedQE()) { opts.quantifiers.prenexQuantUser = true; - if (!opts.wasSetByUser(options::preSkolemQuant)) + if (!opts.quantifiers.preSkolemQuantWasSetByUser) { opts.quantifiers.preSkolemQuant = true; } @@ -1292,11 +1292,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // for induction techniques if (options::quantInduction()) { - if (!opts.wasSetByUser(options::dtStcInduction)) + if (!opts.quantifiers.dtStcInductionWasSetByUser) { opts.quantifiers.dtStcInduction = true; } - if (!opts.wasSetByUser(options::intWfInduction)) + if (!opts.quantifiers.intWfInductionWasSetByUser) { opts.quantifiers.intWfInduction = true; } @@ -1304,38 +1304,38 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::dtStcInduction()) { // try to remove ITEs from quantified formulas - if (!opts.wasSetByUser(options::iteDtTesterSplitQuant)) + if (!opts.quantifiers.iteDtTesterSplitQuantWasSetByUser) { opts.quantifiers.iteDtTesterSplitQuant = true; } - if (!opts.wasSetByUser(options::iteLiftQuant)) + if (!opts.quantifiers.iteLiftQuantWasSetByUser) { opts.quantifiers.iteLiftQuant = options::IteLiftQuantMode::ALL; } } if (options::intWfInduction()) { - if (!opts.wasSetByUser(options::purifyTriggers)) + if (!opts.quantifiers.purifyTriggersWasSetByUser) { opts.quantifiers.purifyTriggers = true; } } if (options::conjectureNoFilter()) { - if (!opts.wasSetByUser(options::conjectureFilterActiveTerms)) + if (!opts.quantifiers.conjectureFilterActiveTermsWasSetByUser) { opts.quantifiers.conjectureFilterActiveTerms = false; } - if (!opts.wasSetByUser(options::conjectureFilterCanonical)) + if (!opts.quantifiers.conjectureFilterCanonicalWasSetByUser) { opts.quantifiers.conjectureFilterCanonical = false; } - if (!opts.wasSetByUser(options::conjectureFilterModel)) + if (!opts.quantifiers.conjectureFilterModelWasSetByUser) { opts.quantifiers.conjectureFilterModel = false; } } - if (opts.wasSetByUser(options::conjectureGenPerRound)) + if (opts.quantifiers.conjectureGenPerRoundWasSetByUser) { if (options::conjectureGenPerRound() > 0) { @@ -1349,7 +1349,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // can't pre-skolemize nested quantifiers without UF theory if (!logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant()) { - if (!opts.wasSetByUser(options::preSkolemQuantNested)) + if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) { opts.quantifiers.preSkolemQuantNested = false; } @@ -1360,7 +1360,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // until bugs 371,431 are fixed - if (!opts.wasSetByUser(options::minisatUseElim)) + if (!opts.prop.minisatUseElimWasSetByUser) { // cannot use minisat elimination for logics where a theory solver // introduces new literals into the search. This includes quantifiers @@ -1382,7 +1382,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (!options::relevanceFilter()) { - if (opts.wasSetByUser(options::relevanceFilter)) + if (opts.theory.relevanceFilterWasSetByUser) { Warning() << "SmtEngine: turning on relevance filtering to support " "--nl-ext-rlv=" @@ -1404,7 +1404,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::bvLazyRewriteExtf()) { - if (opts.wasSetByUser(options::bvLazyRewriteExtf)) + if (opts.bv.bvLazyRewriteExtfWasSetByUser) { throw OptionException( "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set"); @@ -1416,7 +1416,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.bv.bvLazyRewriteExtf = false; } - if (options::stringFMF() && !opts.wasSetByUser(options::stringProcessLoopMode)) + if (options::stringFMF() && !opts.strings.stringProcessLoopModeWasSetByUser) { Trace("smt") << "settting stringProcessLoopMode to 'simple' since " "--strings-fmf enabled" @@ -1427,7 +1427,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // !!! All options that require disabling models go here bool disableModels = false; std::string sOptNoModel; - if (opts.wasSetByUser(options::unconstrainedSimp) && options::unconstrainedSimp()) + if (opts.smt.unconstrainedSimpWasSetByUser && options::unconstrainedSimp()) { disableModels = true; sOptNoModel = "unconstrained-simp"; @@ -1451,7 +1451,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::produceModels()) { - if (opts.wasSetByUser(options::produceModels)) + if (opts.smt.produceModelsWasSetByUser) { std::stringstream ss; ss << "Cannot use " << sOptNoModel << " with model generation."; @@ -1463,7 +1463,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (options::produceAssignments()) { - if (opts.wasSetByUser(options::produceAssignments)) + if (opts.smt.produceAssignmentsWasSetByUser) { std::stringstream ss; ss << "Cannot use " << sOptNoModel @@ -1476,7 +1476,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (options::checkModels()) { - if (opts.wasSetByUser(options::checkModels)) + if (opts.smt.checkModelsWasSetByUser) { std::stringstream ss; ss << "Cannot use " << sOptNoModel @@ -1503,14 +1503,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (logic == LogicInfo("QF_UFNRA")) { #ifdef CVC5_USE_POLY - if (!options::nlCad() && !opts.wasSetByUser(options::nlCad)) + if (!options::nlCad() && !opts.arith.nlCadWasSetByUser) { opts.arith.nlCad = true; - if (!opts.wasSetByUser(options::nlExt)) + if (!opts.arith.nlExtWasSetByUser) { opts.arith.nlExt = options::NlExtMode::LIGHT; } - if (!opts.wasSetByUser(options::nlRlvMode)) + if (!opts.arith.nlRlvModeWasSetByUser) { opts.arith.nlRlvMode = options::NlRlvMode::INTERLEAVE; } @@ -1520,7 +1520,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) #ifndef CVC5_USE_POLY if (options::nlCad()) { - if (opts.wasSetByUser(options::nlCad)) + if (opts.arith.nlCadWasSetByUser) { std::stringstream ss; ss << "Cannot use " << options::arith::nlCad__name << " without configuring with --poly."; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c84a29055..bd48fe0ea 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -444,7 +444,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) { d_state->setFilename(value); } - else if (key == "smt-lib-version" && !Options::current().wasSetByUser(options::inputLanguage)) + else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser) { language::input::Language ilang = language::input::LANG_SMTLIB_V2_6; @@ -456,7 +456,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) } getOptions().base.inputLanguage = ilang; // also update the output language - if (!Options::current().wasSetByUser(options::outputLanguage)) + if (!getOptions().base.outputLanguageWasSetByUser) { language::output::Language olang = language::toOutputLanguage(ilang); if (d_env->getOptions().base.outputLanguage != olang) diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 6069745e0..14bc05335 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, Node query) { Assert (!query.isNull()); - if (Options::current().quantifiers.sygusExprMinerCheckTimeout__setByUser) + if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser) { initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout()); } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index d45a96d3b..0b5d06bd2 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -234,7 +234,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, std::unique_ptr<SmtEngine> repcChecker; // initialize the subsolver using the standard method initializeSubsolver(repcChecker, - Options::current().wasSetByUser(options::sygusRepairConstTimeout), + Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser, options::sygusRepairConstTimeout()); // renable options disabled by sygus repcChecker->setOption("miniscope-quant", "true"); |