From 4dacf3183d6790ebb4615263908da294e43e3cb6 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 2 Jun 2021 08:55:24 +0200 Subject: Make `Options::assign()` specializations free functions (#6648) This PR removes the next two heavily specialized template functions. Both Options::assign() and Options::assignBool() are only used within options.cpp now and there is thus no reason to keep them in the public interface. Furthermore, we can just make them properly named functions instead of template functions. --- src/options/options_template.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/options/options_template.cpp') diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 091acfd7a..251072ba5 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -416,7 +416,7 @@ void Options::parseOptionsRecursive(int argc, char* argv[], std::vector* nonoptions) { - + Options& opts = *this; if(Debug.isOn("options")) { Debug("options") << "starting a new parseOptionsRecursive with " << argc << " arguments" << std::endl; @@ -553,6 +553,7 @@ void Options::setOptionInternal(const std::string& key, const std::string& optionarg) { options::OptionsHandler* handler = d_handler; + Options& opts = *this; ${setoption_handlers}$ throw UnrecognizedOptionException(key); } -- cgit v1.2.3 From 66cdf5254bc58ecff335321478e73c8c0d6df296 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 2 Jun 2021 15:21:22 +0200 Subject: Remove `Options::operator[]` (#6649) This PR removes the next heavily specialized template function Options::operator[] in favor of direct access to the option data. --- src/api/cpp/cvc5.cpp | 32 ++++++++--------- src/options/mkoptions.py | 28 ++++----------- src/options/options_template.cpp | 1 + src/options/options_template.h | 4 --- src/smt/env.cpp | 2 +- src/smt/env.h | 6 ---- src/smt/options_manager.cpp | 8 ++--- src/smt/smt_engine.cpp | 76 ++++++++++++++++++++-------------------- src/util/resource_manager.cpp | 34 +++++++++--------- 9 files changed, 84 insertions(+), 107 deletions(-) (limited to 'src/options/options_template.cpp') diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 0f2d5ad1b..668fc9382 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -4743,7 +4743,7 @@ Solver::Solver(Options* opts) } d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get())); d_smtEngine->setSolver(this); - d_rng.reset(new Random(d_smtEngine->getOptions()[options::seed])); + d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed)); resetStatistics(); } @@ -6452,7 +6452,7 @@ Result Solver::checkEntailed(const Term& term) const NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM(term); @@ -6468,7 +6468,7 @@ Result Solver::checkEntailed(const std::vector& terms) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS(terms); @@ -6497,7 +6497,7 @@ Result Solver::checkSat(void) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; //////// all checks before this line @@ -6512,7 +6512,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); @@ -6528,7 +6528,7 @@ Result Solver::checkSatAssuming(const std::vector& assumptions) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0 - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort()); @@ -6863,10 +6863,10 @@ std::vector Solver::getUnsatAssumptions(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot get unsat assumptions unless incremental solving is enabled " "(try --incremental)"; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatAssumptions) << "Cannot get unsat assumptions unless explicitly enabled " "(try --produce-unsat-assumptions)"; CVC5_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) @@ -6891,7 +6891,7 @@ std::vector Solver::getUnsatCore(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatCores) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) @@ -6925,7 +6925,7 @@ std::vector Solver::getValue(const std::vector& terms) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -6992,7 +6992,7 @@ Term Solver::getSeparationHeap() const d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7011,7 +7011,7 @@ Term Solver::getSeparationNilTerm() const d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7044,7 +7044,7 @@ void Solver::pop(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot pop when not solving incrementally (use --incremental)"; CVC5_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) << "Cannot pop beyond first pushed context"; @@ -7133,7 +7133,7 @@ void Solver::blockModel() const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7148,7 +7148,7 @@ void Solver::blockModelValues(const std::vector& terms) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7176,7 +7176,7 @@ void Solver::push(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot push when not solving incrementally (use --incremental)"; //////// all checks before this line for (uint32_t n = 0; n < nscopes; ++n) diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 91a5c32e0..c355ff436 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -129,16 +129,6 @@ TPL_OPTION_STRUCT_RW = \ type operator()() const; }} thread_local {name};""" -TPL_DECL_OP_BRACKET = \ -"""template <> const options::{name}__option_t::type& Options::operator[]( - options::{name}__option_t) const;""" - -TPL_IMPL_OP_BRACKET = TPL_DECL_OP_BRACKET[:-1] + \ -""" -{{ - return {module}.{name}; -}}""" - TPL_DECL_WAS_SET_BY_USER = \ """template <> bool Options::wasSetByUser(options::{name}__option_t) const;""" @@ -151,10 +141,8 @@ TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \ # Option specific methods TPL_IMPL_OP_PAR = \ -"""inline {name}__option_t::type {name}__option_t::operator()() const -{{ - return Options::current()[*this]; -}}""" +"""inline {type} {name}__option_t::operator()() const +{{ return Options::current().{module}.{name}; }}""" # Mode templates TPL_DECL_MODE_ENUM = \ @@ -591,7 +579,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_OP_BRACKET.format(name=option.name)) specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name)) if option.long and option.type not in ['bool', 'void'] and \ @@ -606,14 +593,13 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): module.id, option.long, option.type)) # Generate module inlines - inls.append(TPL_IMPL_OP_PAR.format(name=option.name)) + inls.append(TPL_IMPL_OP_PAR.format(module=module.id, name=option.name, type=option.type)) ### Generate code for {module.name}_options.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_OP_BRACKET.format(module=module.id, name=option.name)) accs.append(TPL_IMPL_WAS_SET_BY_USER.format(module=module.id, name=option.name)) # Global definitions @@ -872,17 +858,17 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ 'if ({}) {{'.format(cond)) if option.type == 'bool': getoption_handlers.append( - 'return (*this)[options::{}] ? "true" : "false";'.format(option.name)) + 'return options.{}.{} ? "true" : "false";'.format(module.id, option.name)) elif option.type == 'std::string': getoption_handlers.append( - 'return (*this)[options::{}];'.format(option.name)) + 'return options.{}.{};'.format(module.id, option.name)) elif is_numeric_cpp_type(option.type): getoption_handlers.append( - 'return std::to_string((*this)[options::{}]);'.format(option.name)) + 'return std::to_string(options.{}.{});'.format(module.id, option.name)) else: getoption_handlers.append('std::stringstream ss;') getoption_handlers.append( - 'ss << (*this)[options::{}];'.format(option.name)) + 'ss << options.{}.{};'.format(module.id, option.name)) getoption_handlers.append('return ss.str();') getoption_handlers.append('}') diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 251072ba5..0d6b7f01b 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -563,6 +563,7 @@ void Options::setOptionInternal(const std::string& key, std::string Options::getOption(const std::string& key) const { Trace("options") << "Options::getOption(" << key << ")" << std::endl; + const Options& options = *this; ${getoption_handlers}$ throw UnrecognizedOptionException(key); diff --git a/src/options/options_template.h b/src/options/options_template.h index 6e28aad85..6ce77d7a1 100644 --- a/src/options/options_template.h +++ b/src/options/options_template.h @@ -124,10 +124,6 @@ public: */ void setOption(const std::string& key, const std::string& optionarg); - /** Get the value of the given option. Const access only. */ - template - const typename T::type& operator[](T) const; - /** * Gets the value of the given option by key and returns value as a string. * diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 87c19d0e1..1381ef87c 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -104,7 +104,7 @@ ResourceManager* Env::getResourceManager() const const Printer& Env::getPrinter() { - return *Printer::getPrinter(d_options[options::outputLanguage]); + return *Printer::getPrinter(d_options.base.outputLanguage); } std::ostream& Env::getDumpOut() { return *d_options.base.out; } diff --git a/src/smt/env.h b/src/smt/env.h index 667497683..29a360209 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -91,12 +91,6 @@ class Env /** Get a pointer to the underlying dump manager. */ smt::DumpManager* getDumpManager(); - template - const auto& getOption(Opt opt) const - { - return d_options[opt]; - } - /** Get the options object (const version only) owned by this Env. */ const Options& getOptions() const; diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 3fc58ff05..37541751e 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -71,7 +71,7 @@ void OptionsManager::notifySetOption(const std::string& key) << std::endl; if (key == options::expr::defaultExprDepth__name) { - int depth = (*d_options)[options::defaultExprDepth]; + int depth = d_options->expr.defaultExprDepth; Debug.getStream() << expr::ExprSetDepth(depth); Trace.getStream() << expr::ExprSetDepth(depth); Notice.getStream() << expr::ExprSetDepth(depth); @@ -82,7 +82,7 @@ void OptionsManager::notifySetOption(const std::string& key) } else if (key == options::expr::defaultDagThresh__name) { - int dag = (*d_options)[options::defaultDagThresh]; + int dag = d_options->expr.defaultDagThresh; Debug.getStream() << expr::ExprDag(dag); Trace.getStream() << expr::ExprDag(dag); Notice.getStream() << expr::ExprDag(dag); @@ -93,12 +93,12 @@ void OptionsManager::notifySetOption(const std::string& key) } else if (key == options::smt::dumpModeString__name) { - const std::string& value = (*d_options)[options::dumpModeString]; + const std::string& value = d_options->smt.dumpModeString; Dump.setDumpFromString(value); } else if (key == options::base::printSuccess__name) { - bool value = (*d_options)[options::printSuccess]; + bool value = d_options->base.printSuccess; Debug.getStream() << Command::printsuccess(value); Trace.getStream() << Command::printsuccess(value); Notice.getStream() << Command::printsuccess(value); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7abeac44f..c84a29055 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -193,7 +193,7 @@ void SmtEngine::finishInit() } // set the random seed - Random::getRandom().setSeed(d_env->getOption(options::seed)); + Random::getRandom().setSeed(d_env->getOptions().driver.seed); // Call finish init on the options manager. This inializes the resource // manager based on the options, and sets up the best default options @@ -201,7 +201,7 @@ void SmtEngine::finishInit() d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver); ProofNodeManager* pnm = nullptr; - if (d_env->getOption(options::produceProofs)) + if (d_env->getOptions().smt.produceProofs) { // ensure bound variable uses canonical bound variables getNodeManager()->getBoundVarManager()->enableKeepCacheValues(); @@ -262,11 +262,11 @@ void SmtEngine::finishInit() getDumpManager()->finishInit(); // subsolvers - if (d_env->getOption(options::produceAbducts)) + if (d_env->getOptions().smt.produceAbducts) { d_abductSolver.reset(new AbductionSolver(this)); } - if (d_env->getOption(options::produceInterpols) + if (d_env->getOptions().smt.produceInterpols != options::ProduceInterpols::NONE) { d_interpolSolver.reset(new InterpolationSolver(this)); @@ -459,10 +459,10 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) if (!Options::current().wasSetByUser(options::outputLanguage)) { language::output::Language olang = language::toOutputLanguage(ilang); - if (d_env->getOption(options::outputLanguage) != olang) + if (d_env->getOptions().base.outputLanguage != olang) { getOptions().base.outputLanguage = olang; - *d_env->getOption(options::out) << language::SetLanguage(olang); + *d_env->getOptions().base.out << language::SetLanguage(olang); } } } @@ -575,7 +575,7 @@ void SmtEngine::debugCheckFunctionBody(Node formula, Node func) { TypeNode formulaType = - formula.getType(d_env->getOption(options::typeChecking)); + formula.getType(d_env->getOptions().expr.typeChecking); TypeNode funcType = func.getType(); // We distinguish here between definitions of constants and functions, // because the type checking for them is subtly different. Perhaps we @@ -741,7 +741,7 @@ Result SmtEngine::quickCheck() { Model* SmtEngine::getAvailableModel(const char* c) const { - if (!d_env->getOption(options::assignFunctionValues)) + if (!d_env->getOptions().theory.assignFunctionValues) { std::stringstream ss; ss << "Cannot " << c << " when --assign-function-values is false."; @@ -758,7 +758,7 @@ Model* SmtEngine::getAvailableModel(const char* c) const throw RecoverableModalException(ss.str().c_str()); } - if (!d_env->getOption(options::produceModels)) + if (!d_env->getOptions().smt.produceModels) { std::stringstream ss; ss << "Cannot " << c << " when produce-models options is off."; @@ -902,7 +902,7 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, << "(" << assumptions << ") => " << r << endl; // Check that SAT results generate a model correctly. - if (d_env->getOption(options::checkModels)) + if (d_env->getOptions().smt.checkModels) { if (r.asSatisfiabilityResult().isSat() == Result::SAT) { @@ -910,14 +910,14 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, } } // Check that UNSAT results generate a proof correctly. - if (d_env->getOption(options::checkProofs) - || d_env->getOption(options::proofEagerChecking)) + if (d_env->getOptions().smt.checkProofs + || d_env->getOptions().proof.proofEagerChecking) { if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { - if ((d_env->getOption(options::checkProofs) - || d_env->getOption(options::proofEagerChecking)) - && !d_env->getOption(options::produceProofs)) + if ((d_env->getOptions().smt.checkProofs + || d_env->getOptions().proof.proofEagerChecking) + && !d_env->getOptions().smt.produceProofs) { throw ModalException( "Cannot check-proofs because proofs were disabled."); @@ -926,7 +926,7 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, } } // Check that UNSAT results generate an unsat core correctly. - if (d_env->getOption(options::checkUnsatCores)) + if (d_env->getOptions().smt.checkUnsatCores) { if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { @@ -955,7 +955,7 @@ std::vector SmtEngine::getUnsatAssumptions(void) { Trace("smt") << "SMT getUnsatAssumptions()" << endl; SmtScope smts(this); - if (!d_env->getOption(options::unsatAssumptions)) + if (!d_env->getOptions().smt.unsatAssumptions) { throw ModalException( "Cannot get unsat assumptions when produce-unsat-assumptions option " @@ -1166,7 +1166,7 @@ Node SmtEngine::getValue(const Node& ex) const Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA || resultNode.isConst()); - if (d_env->getOption(options::abstractValues) + if (d_env->getOptions().smt.abstractValues && resultNode.getType().isArray()) { resultNode = d_absValues->mkAbstractValue(resultNode); @@ -1207,7 +1207,7 @@ Model* SmtEngine::getModel() { Assert(te != nullptr); te->setEagerModelBuilding(); - if (d_env->getOption(options::modelCoresMode) + if (d_env->getOptions().smt.modelCoresMode != options::ModelCoresMode::NONE) { // If we enabled model cores, we compute a model core for m based on our @@ -1215,7 +1215,7 @@ Model* SmtEngine::getModel() { std::vector eassertsProc = getExpandedAssertions(); ModelCoreBuilder::setModelCore(eassertsProc, m->getTheoryModel(), - d_env->getOption(options::modelCoresMode)); + d_env->getOptions().smt.modelCoresMode); } // set the information on the SMT-level model Assert(m != nullptr); @@ -1238,7 +1238,7 @@ Result SmtEngine::blockModel() Model* m = getAvailableModel("block model"); - if (d_env->getOption(options::blockModelsMode) + if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE) { std::stringstream ss; @@ -1251,7 +1251,7 @@ Result SmtEngine::blockModel() Node eblocker = ModelBlocker::getModelBlocker(eassertsProc, m->getTheoryModel(), - d_env->getOption(options::blockModelsMode)); + d_env->getOptions().smt.blockModelsMode); Trace("smt") << "Block formula: " << eblocker << std::endl; return assertFormula(eblocker); } @@ -1349,17 +1349,17 @@ Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } void SmtEngine::checkProof() { - Assert(d_env->getOption(options::produceProofs)); + Assert(d_env->getOptions().smt.produceProofs); // internal check the proof PropEngine* pe = getPropEngine(); Assert(pe != nullptr); - if (d_env->getOption(options::proofEagerChecking)) + if (d_env->getOptions().proof.proofEagerChecking) { pe->checkProof(d_asserts->getAssertionList()); } Assert(pe->getProof() != nullptr); std::shared_ptr pePfn = pe->getProof(); - if (d_env->getOption(options::checkProofs)) + if (d_env->getOptions().smt.checkProofs) { d_pfManager->checkProof(pePfn, *d_asserts); } @@ -1372,7 +1372,7 @@ StatisticsRegistry& SmtEngine::getStatisticsRegistry() UnsatCore SmtEngine::getUnsatCoreInternal() { - if (!d_env->getOption(options::unsatCores)) + if (!d_env->getOptions().smt.unsatCores) { throw ModalException( "Cannot get an unsat core when produce-unsat-cores or produce-proofs " @@ -1405,7 +1405,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal() } void SmtEngine::checkUnsatCore() { - Assert(d_env->getOption(options::unsatCores)) + Assert(d_env->getOptions().smt.unsatCores) << "cannot check unsat core if unsat cores are turned off"; Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; @@ -1514,7 +1514,7 @@ std::string SmtEngine::getProof() { getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut()); } - if (!d_env->getOption(options::produceProofs)) + if (!d_env->getOptions().smt.produceProofs) { throw ModalException("Cannot get a proof when proof option is off."); } @@ -1537,7 +1537,7 @@ std::string SmtEngine::getProof() void SmtEngine::printInstantiations( std::ostream& out ) { SmtScope smts(this); finishInit(); - if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS) + if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) { out << "% SZS output start Proof for " << d_state->getFilename() << std::endl; @@ -1546,9 +1546,9 @@ void SmtEngine::printInstantiations( std::ostream& out ) { // First, extract and print the skolemizations bool printed = false; - bool reqNames = !d_env->getOption(options::printInstFull); + bool reqNames = !d_env->getOptions().printer.printInstFull; // only print when in list mode - if (d_env->getOption(options::printInstMode) == options::PrintInstMode::LIST) + if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST) { std::map> sks; qe->getSkolemTermVectors(sks); @@ -1583,14 +1583,14 @@ void SmtEngine::printInstantiations( std::ostream& out ) { continue; } // must have a name - if (d_env->getOption(options::printInstMode) == options::PrintInstMode::NUM) + if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::NUM) { out << "(num-instantiations " << name << " " << i.second.size() << ")" << std::endl; } else { - Assert(d_env->getOption(options::printInstMode) + Assert(d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST); InstantiationList ilist(name, i.second); out << ilist; @@ -1602,7 +1602,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) { { out << "No instantiations" << std::endl; } - if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS) + if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) { out << "% SZS output end Proof for " << d_state->getFilename() << std::endl; } @@ -1613,9 +1613,9 @@ void SmtEngine::getInstantiationTermVectors( { SmtScope smts(this); finishInit(); - if (d_env->getOption(options::produceProofs) - && (!d_env->getOption(options::unsatCores) - || d_env->getOption(options::unsatCoresMode) == options::UnsatCoresMode::FULL_PROOF) + if (d_env->getOptions().smt.produceProofs + && (!d_env->getOptions().smt.unsatCores + || d_env->getOptions().smt.unsatCoresMode == options::UnsatCoresMode::FULL_PROOF) && getSmtMode() == SmtMode::UNSAT) { // minimize instantiations based on proof manager @@ -1716,7 +1716,7 @@ std::vector SmtEngine::getAssertions() getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut()); } Trace("smt") << "SMT getAssertions()" << endl; - if (!d_env->getOption(options::produceAssertions)) + if (!d_env->getOptions().smt.produceAssertions) { const char* msg = "Cannot query the current assertion list when not in produce-assertions mode."; diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index de9a32248..f0cc78789 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -164,7 +164,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, d_infidWeights.fill(1); d_resourceWeights.fill(1); - for (const auto& opt : d_options[options::resourceWeightHolder]) + for (const auto& opt : d_options.resman.resourceWeightHolder) { std::string name; uint64_t weight; @@ -189,9 +189,9 @@ uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; } uint64_t ResourceManager::getResourceRemaining() const { - if (d_options[options::cumulativeResourceLimit] <= d_cumulativeResourceUsed) + if (d_options.resman.cumulativeResourceLimit <= d_cumulativeResourceUsed) return 0; - return d_options[options::cumulativeResourceLimit] - d_cumulativeResourceUsed; + return d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed; } void ResourceManager::spendResource(uint64_t amount) @@ -237,21 +237,21 @@ void ResourceManager::spendResource(theory::InferenceId iid) void ResourceManager::beginCall() { - d_perCallTimer.set(d_options[options::perCallMillisecondLimit]); + d_perCallTimer.set(d_options.resman.perCallMillisecondLimit); d_thisCallResourceUsed = 0; - if (d_options[options::cumulativeResourceLimit] > 0) + if (d_options.resman.cumulativeResourceLimit > 0) { // Compute remaining cumulative resource budget d_thisCallResourceBudget = - d_options[options::cumulativeResourceLimit] - d_cumulativeResourceUsed; + d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed; } - if (d_options[options::perCallResourceLimit] > 0) + if (d_options.resman.perCallResourceLimit > 0) { // Check if per-call resource budget is even smaller - if (d_options[options::perCallResourceLimit] < d_thisCallResourceBudget) + if (d_options.resman.perCallResourceLimit < d_thisCallResourceBudget) { - d_thisCallResourceBudget = d_options[options::perCallResourceLimit]; + d_thisCallResourceBudget = d_options.resman.perCallResourceLimit; } } } @@ -265,25 +265,25 @@ void ResourceManager::endCall() bool ResourceManager::limitOn() const { - return (d_options[options::cumulativeResourceLimit] > 0) - || (d_options[options::perCallMillisecondLimit] > 0) - || (d_options[options::perCallResourceLimit] > 0); + return (d_options.resman.cumulativeResourceLimit > 0) + || (d_options.resman.perCallMillisecondLimit > 0) + || (d_options.resman.perCallResourceLimit > 0); } bool ResourceManager::outOfResources() const { - if (d_options[options::perCallResourceLimit] > 0) + if (d_options.resman.perCallResourceLimit > 0) { // Check if per-call resources are exhausted - if (d_thisCallResourceUsed >= d_options[options::perCallResourceLimit]) + if (d_thisCallResourceUsed >= d_options.resman.perCallResourceLimit) { return true; } } - if (d_options[options::cumulativeResourceLimit] > 0) + if (d_options.resman.cumulativeResourceLimit > 0) { // Check if cumulative resources are exhausted - if (d_cumulativeResourceUsed >= d_options[options::cumulativeResourceLimit]) + if (d_cumulativeResourceUsed >= d_options.resman.cumulativeResourceLimit) { return true; } @@ -293,7 +293,7 @@ bool ResourceManager::outOfResources() const bool ResourceManager::outOfTime() const { - if (d_options[options::perCallMillisecondLimit] == 0) return false; + if (d_options.resman.perCallMillisecondLimit == 0) return false; return d_perCallTimer.expired(); } -- cgit v1.2.3