From e04248ec858c97b8d716796f87ed42078a953967 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 5 Aug 2021 18:18:49 -0700 Subject: [PATCH] Clear options manager (#6991) This PR moves the remaining responsibilities from the options manager into option predicates. They belong there anyway, given that this code shall be executed immediately when an option is set. This also allows to remove the infrastructure for an options listener. --- src/options/base_options.toml | 1 + src/options/expr_options.toml | 6 ++- src/options/mkoptions.py | 9 ++-- src/options/options_handler.cpp | 53 +++++++++++++++++----- src/options/options_handler.h | 19 +++++--- src/options/options_public_template.cpp | 2 - src/options/options_template.cpp | 13 +----- src/options/options_template.h | 11 +---- src/options/smt_options.toml | 1 + src/smt/options_manager.cpp | 60 ------------------------- 10 files changed, 67 insertions(+), 108 deletions(-) diff --git a/src/options/base_options.toml b/src/options/base_options.toml index bdc369b60..9a2d2f74e 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -158,6 +158,7 @@ public = true category = "regular" long = "print-success" type = "bool" + predicates = ["setPrintSuccess"] help = "print the \"success\" output required of SMT-LIBv2" [[option]] diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml index 075ce6fa9..c95fd3dfc 100644 --- a/src/options/expr_options.toml +++ b/src/options/expr_options.toml @@ -7,7 +7,8 @@ name = "Expression" long = "expr-depth=N" type = "int64_t" default = "0" - predicates = ["setDefaultExprDepthPredicate"] + minimum = "-1" + predicates = ["setDefaultExprDepth"] help = "print exprs to depth N (0 == default, -1 == no limit)" [[option]] @@ -16,7 +17,8 @@ name = "Expression" long = "dag-thresh=N" type = "int64_t" default = "1" - predicates = ["setDefaultDagThreshPredicate"] + minimum = "0" + predicates = ["setDefaultDagThresh"] help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)" [[option]] diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 02087d6a0..15f319e9c 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -239,12 +239,13 @@ def get_predicates(option): return [] optname = option.long_name if option.long else "" assert option.type != 'void' - res = ['opts.handler().{}("{}", option, value);'.format(x, optname) - for x in option.predicates] + res = [] if option.minimum: - res.append('opts.handler().checkMinimum("{}", option, value, {});'.format(optname, option.minimum)) + res.append('opts.handler().checkMinimum("{}", option, value, static_cast<{}>({}));'.format(optname, option.type, option.minimum)) if option.maximum: - res.append('opts.handler().checkMaximum("{}", option, value, {});'.format(optname, option.maximum)) + res.append('opts.handler().checkMaximum("{}", option, value, static_cast<{}>({}));'.format(optname, option.type, option.maximum)) + res += ['opts.handler().{}("{}", option, value);'.format(x, optname) + for x in option.predicates] return res diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index f5c80a758..55661a094 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -26,6 +26,7 @@ #include "base/exception.h" #include "base/modal_exception.h" #include "base/output.h" +#include "expr/expr_iomanip.h" #include "lib/strtok_r.h" #include "options/base_options.h" #include "options/bv_options.h" @@ -35,6 +36,7 @@ #include "options/option_exception.h" #include "options/smt_options.h" #include "options/theory_options.h" +#include "smt/command.h" #include "smt/dump.h" namespace cvc5 { @@ -294,22 +296,29 @@ void OptionsHandler::threadN(const std::string& option, const std::string& flag) } // expr/options_handlers.h -void OptionsHandler::setDefaultExprDepthPredicate(const std::string& option, - const std::string& flag, - int depth) +void OptionsHandler::setDefaultExprDepth(const std::string& option, + const std::string& flag, + int depth) { - if(depth < -1) { - throw OptionException("--expr-depth requires a positive argument, or -1."); - } + Debug.getStream() << expr::ExprSetDepth(depth); + Trace.getStream() << expr::ExprSetDepth(depth); + Notice.getStream() << expr::ExprSetDepth(depth); + Chat.getStream() << expr::ExprSetDepth(depth); + CVC5Message.getStream() << expr::ExprSetDepth(depth); + Warning.getStream() << expr::ExprSetDepth(depth); } -void OptionsHandler::setDefaultDagThreshPredicate(const std::string& option, - const std::string& flag, - int dag) +void OptionsHandler::setDefaultDagThresh(const std::string& option, + const std::string& flag, + int dag) { - if(dag < 0) { - throw OptionException("--dag-thresh requires a nonnegative argument."); - } + Debug.getStream() << expr::ExprDag(dag); + Trace.getStream() << expr::ExprDag(dag); + Notice.getStream() << expr::ExprDag(dag); + Chat.getStream() << expr::ExprDag(dag); + CVC5Message.getStream() << expr::ExprDag(dag); + Warning.getStream() << expr::ExprDag(dag); + Dump.getStream() << expr::ExprDag(dag); } // main/options_handlers.h @@ -630,5 +639,25 @@ void OptionsHandler::decreaseVerbosity(const std::string& option, setVerbosity(option, flag, d_options->base.verbosity); } +void OptionsHandler::setDumpMode(const std::string& option, + const std::string& flag, + const std::string& optarg) +{ + Dump.setDumpFromString(optarg); +} + +void OptionsHandler::setPrintSuccess(const std::string& option, + const std::string& flag, + bool value) +{ + Debug.getStream() << Command::printsuccess(value); + Trace.getStream() << Command::printsuccess(value); + Notice.getStream() << Command::printsuccess(value); + Chat.getStream() << Command::printsuccess(value); + CVC5Message.getStream() << Command::printsuccess(value); + Warning.getStream() << Command::printsuccess(value); + *d_options->base.out << Command::printsuccess(value); +} + } // namespace options } // namespace cvc5 diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 867d48a44..f19e63445 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -123,12 +123,12 @@ public: const std::string& optarg); /* expr/options_handlers.h */ - void setDefaultExprDepthPredicate(const std::string& option, - const std::string& flag, - int depth); - void setDefaultDagThreshPredicate(const std::string& option, - const std::string& flag, - int dag); + void setDefaultExprDepth(const std::string& option, + const std::string& flag, + int depth); + void setDefaultDagThresh(const std::string& option, + const std::string& flag, + int dag); /* main/options_handlers.h */ void copyright(const std::string& option, const std::string& flag); @@ -172,6 +172,13 @@ public: const std::string& flag, const std::string& optarg); + void setDumpMode(const std::string& option, + const std::string& flag, + const std::string& optarg); + void setPrintSuccess(const std::string& option, + const std::string& flag, + bool value); + private: /** Pointer to the containing Options object.*/ diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp index a744cf0a9..33c363b55 100644 --- a/src/options/options_public_template.cpp +++ b/src/options/options_public_template.cpp @@ -520,8 +520,6 @@ void set(Options& opts, const std::string& name, const std::string& optionarg) << std::endl; // first update this object setInternal(opts, name, optionarg); - // then, notify the provided listener - opts.notifyListener(name); } std::vector > getAll(const Options& opts) diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index db58c3a4a..06a423438 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -37,9 +37,8 @@ namespace cvc5 { thread_local Options* Options::s_current = nullptr; - Options::Options(OptionsListener * ol) + Options::Options() : - d_olisten(ol), // clang-format off ${holder_mem_inits}$ ${holder_ref_inits}$ @@ -58,15 +57,5 @@ ${holder_mem_copy}$ } } -void Options::setListener(OptionsListener* ol) { d_olisten = ol; } - -void Options::notifyListener(const std::string& key) - { - if (d_olisten != nullptr) - { - d_olisten->notifySetOption(key); - } - } - } // namespace cvc5 diff --git a/src/options/options_template.h b/src/options/options_template.h index a4e595f0d..290b96f9e 100644 --- a/src/options/options_template.h +++ b/src/options/options_template.h @@ -23,7 +23,6 @@ #include #include -#include "base/listener.h" #include "cvc5_export.h" namespace cvc5 { @@ -77,7 +76,7 @@ class CVC5_EXPORT Options return *s_current; } - Options(OptionsListener* ol = nullptr); + Options(); ~Options(); options::OptionsHandler& handler() const { @@ -87,18 +86,10 @@ class CVC5_EXPORT Options /** * Copies the value of the options stored in OptionsHolder into the current * Options object. - * This does not copy the listeners in the Options object. */ void copyValues(const Options& options); - /** Set the generic listener associated with this class to ol */ - void setListener(OptionsListener* ol); - - void notifyListener(const std::string& key); - private: - /** Pointer to the options listener, if one exists */ - OptionsListener* d_olisten = nullptr; // clang-format off ${holder_mem_decls}$ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 3a0e3e9f5..8094b5a6b 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -7,6 +7,7 @@ name = "SMT Layer" long = "dump=MODE" type = "std::string" help = "dump preprocessed assertions, etc., see --dump=help" + predicates = ["setDumpMode"] [[option]] name = "dumpToFileName" diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 8bdbd7755..a5dee27ae 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -30,72 +30,12 @@ namespace smt { OptionsManager::OptionsManager(Options* opts) : d_options(opts) { - // set options that must take effect immediately - if (opts->expr.defaultExprDepthWasSetByUser) - { - notifySetOption(options::expr::defaultExprDepth__name); - } - if (opts->expr.defaultDagThreshWasSetByUser) - { - notifySetOption(options::expr::defaultDagThresh__name); - } - if (opts->smt.dumpModeStringWasSetByUser) - { - notifySetOption(options::smt::dumpModeString__name); - } - if (opts->base.printSuccessWasSetByUser) - { - notifySetOption(options::base::printSuccess__name); - } - // set this as a listener to be notified of options changes from now on - opts->setListener(this); } OptionsManager::~OptionsManager() {} void OptionsManager::notifySetOption(const std::string& key) { - Trace("smt") << "SmtEnginePrivate::notifySetOption(" << key << ")" - << std::endl; - if (key == options::expr::defaultExprDepth__name) - { - int depth = d_options->expr.defaultExprDepth; - Debug.getStream() << expr::ExprSetDepth(depth); - Trace.getStream() << expr::ExprSetDepth(depth); - Notice.getStream() << expr::ExprSetDepth(depth); - Chat.getStream() << expr::ExprSetDepth(depth); - CVC5Message.getStream() << expr::ExprSetDepth(depth); - Warning.getStream() << expr::ExprSetDepth(depth); - // intentionally exclude Dump stream from this list - } - else if (key == options::expr::defaultDagThresh__name) - { - int dag = d_options->expr.defaultDagThresh; - Debug.getStream() << expr::ExprDag(dag); - Trace.getStream() << expr::ExprDag(dag); - Notice.getStream() << expr::ExprDag(dag); - Chat.getStream() << expr::ExprDag(dag); - CVC5Message.getStream() << expr::ExprDag(dag); - Warning.getStream() << expr::ExprDag(dag); - Dump.getStream() << expr::ExprDag(dag); - } - else if (key == options::smt::dumpModeString__name) - { - const std::string& value = d_options->smt.dumpModeString; - Dump.setDumpFromString(value); - } - else if (key == options::base::printSuccess__name) - { - bool value = d_options->base.printSuccess; - Debug.getStream() << Command::printsuccess(value); - Trace.getStream() << Command::printsuccess(value); - Notice.getStream() << Command::printsuccess(value); - Chat.getStream() << Command::printsuccess(value); - CVC5Message.getStream() << Command::printsuccess(value); - Warning.getStream() << Command::printsuccess(value); - *options::out() << Command::printsuccess(value); - } - // otherwise, no action is necessary } void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver) -- 2.30.2