From 66cdf5254bc58ecff335321478e73c8c0d6df296 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 2 Jun 2021 15:21:22 +0200 Subject: [PATCH] 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(-) 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(); } -- 2.30.2