From cb8d041d3820a46721f689f188839184003e0e7c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 17 Jul 2020 07:35:14 -0500 Subject: [PATCH] Add option manager and simpler option listener (#4745) This adds the "OptionManager" class, which will live in SmtEngine. This is the required infrastructure for implementing all "reactive" options, i.e. those that must take effect immediately. This PR does not enable this class yet, it simply adds the definitions. After this PR, we can connect it to SmtEngine and delete the old options listener infrastructure. --- src/CMakeLists.txt | 2 + src/options/CMakeLists.txt | 1 + src/options/options.h | 13 ++- src/options/options_listener.h | 37 +++++++++ src/options/options_template.cpp | 27 ++++-- src/smt/options_manager.cpp | 137 +++++++++++++++++++++++++++++++ src/smt/options_manager.h | 73 ++++++++++++++++ 7 files changed, 282 insertions(+), 8 deletions(-) create mode 100644 src/options/options_listener.h create mode 100644 src/smt/options_manager.cpp create mode 100644 src/smt/options_manager.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5c1a18900..306813122 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -241,6 +241,8 @@ libcvc4_add_sources( smt/model_core_builder.h smt/model_blocker.cpp smt/model_blocker.h + smt/options_manager.cpp + smt/options_manager.h smt/preprocess_proof_generator.cpp smt/preprocess_proof_generator.h smt/process_assertions.cpp diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 46bd17172..a4f993d99 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -26,6 +26,7 @@ libcvc4_add_sources( options.h options_handler.cpp options_handler.h + options_listener.h options_public_functions.cpp printer_modes.cpp printer_modes.h diff --git a/src/options/options.h b/src/options/options.h index 0732d4ddb..2ea72ca92 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -40,6 +40,8 @@ namespace options { class OptionsHandler; }/* CVC4::options namespace */ +class OptionsListener; + class CVC4_PUBLIC Options { friend api::Solver; /** The struct that holds all option values. */ @@ -132,7 +134,7 @@ public: return s_current; } - Options(); + Options(OptionsListener* ol = nullptr); ~Options(); /** @@ -300,6 +302,8 @@ public: */ std::vector > getOptions() const; + /** Set the generic listener associated with this class to ol */ + void setListener(OptionsListener* ol); /** * Registers a listener for the notification, notifyBeforeSearch. * @@ -415,6 +419,13 @@ public: void flushOut(); private: + /** Pointer to the options listener, if one exists */ + OptionsListener* d_olisten; + /** + * Helper method for setOption, updates this object for setting the given + * option. + */ + void setOptionInternal(const std::string& key, const std::string& optionarg); /** * Internal procedure for implementing the parseOptions function. * Initializes the options object based on the given command-line diff --git a/src/options/options_listener.h b/src/options/options_listener.h new file mode 100644 index 000000000..0c441b714 --- /dev/null +++ b/src/options/options_listener.h @@ -0,0 +1,37 @@ +/********************* */ +/*! \file options_listener.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Base class for option listener + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__OPTIONS__OPTIONS_LISTENER_H +#define CVC4__OPTIONS__OPTIONS_LISTENER_H + +#include + +namespace CVC4 { + +class OptionsListener +{ + public: + OptionsListener() {} + virtual ~OptionsListener() {} + /** + * Notify that option key has been set. + */ + virtual void notifySetOption(const std::string& key) = 0; +}; + +} // namespace CVC4 + +#endif /* CVC4__OPTIONS__OPTION_LISTENER_H */ diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index bf8926521..b4aa3dae0 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -54,6 +54,7 @@ extern int optreset; #include "options/didyoumean.h" #include "options/language.h" #include "options/options_handler.h" +#include "options/options_listener.h" ${headers_module}$ @@ -224,10 +225,11 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h } -Options::Options() +Options::Options(OptionsListener* ol) : d_holder(new options::OptionsHolder()) , d_handler(new options::OptionsHandler(this)) - , d_beforeSearchListeners() + , d_beforeSearchListeners(), + d_olisten(ol) {} Options::~Options() { @@ -250,6 +252,8 @@ std::string Options::formatThreadOptionException(const std::string& option) { return ss.str(); } +void Options::setListener(OptionsListener* ol) { d_olisten = ol; } + ListenerCollection::Registration* Options::registerAndNotify( ListenerCollection& collection, Listener* listener, bool notify) { @@ -662,14 +666,23 @@ std::vector > Options::getOptions() const void Options::setOption(const std::string& key, const std::string& optionarg) { - options::OptionsHandler* handler = d_handler; - Options* options = this; - Trace("options") << "SMT setOption(" << key << ", " << optionarg << ")" + Trace("options") << "setOption(" << key << ", " << optionarg << ")" << std::endl; + // first update this object + setOptionInternal(key, optionarg); + // then, notify the provided listener + if (d_olisten != nullptr) + { + d_olisten->notifySetOption(key); + } +} +void Options::setOptionInternal(const std::string& key, + const std::string& optionarg) +{ + options::OptionsHandler* handler = d_handler; + Options* options = this; ${setoption_handlers}$ - - throw UnrecognizedOptionException(key); } diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp new file mode 100644 index 000000000..5b976bc31 --- /dev/null +++ b/src/smt/options_manager.cpp @@ -0,0 +1,137 @@ +/********************* */ +/*! \file options_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Module for managing options of an SmtEngine. + **/ + +#include "smt/options_manager.h" + +#include "base/output.h" +#include "expr/expr_iomanip.h" +#include "options/base_options.h" +#include "options/expr_options.h" +#include "options/smt_options.h" +#include "smt/command.h" +#include "smt/dump.h" +#include "smt/set_defaults.h" +#include "util/resource_manager.h" + +namespace CVC4 { +namespace smt { + +OptionsManager::OptionsManager(Options* opts, ResourceManager* rm) + : d_options(opts), d_resourceManager(rm) +{ + // set options that must take effect immediately + if (opts->wasSetByUser(options::defaultExprDepth)) + { + notifySetOption(options::defaultExprDepth.getName()); + } + if (opts->wasSetByUser(options::defaultDagThresh)) + { + notifySetOption(options::defaultDagThresh.getName()); + } + if (opts->wasSetByUser(options::printExprTypes)) + { + notifySetOption(options::printExprTypes.getName()); + } + if (opts->wasSetByUser(options::dumpModeString)) + { + notifySetOption(options::dumpModeString.getName()); + } + if (opts->wasSetByUser(options::printSuccess)) + { + notifySetOption(options::printSuccess.getName()); + } + // 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::defaultExprDepth.getName()) + { + int depth = (*d_options)[options::defaultExprDepth]; + Debug.getStream() << expr::ExprSetDepth(depth); + Trace.getStream() << expr::ExprSetDepth(depth); + Notice.getStream() << expr::ExprSetDepth(depth); + Chat.getStream() << expr::ExprSetDepth(depth); + Message.getStream() << expr::ExprSetDepth(depth); + Warning.getStream() << expr::ExprSetDepth(depth); + // intentionally exclude Dump stream from this list + } + else if (key == options::defaultDagThresh.getName()) + { + int dag = (*d_options)[options::defaultDagThresh]; + Debug.getStream() << expr::ExprDag(dag); + Trace.getStream() << expr::ExprDag(dag); + Notice.getStream() << expr::ExprDag(dag); + Chat.getStream() << expr::ExprDag(dag); + Message.getStream() << expr::ExprDag(dag); + Warning.getStream() << expr::ExprDag(dag); + Dump.getStream() << expr::ExprDag(dag); + } + else if (key == options::printExprTypes.getName()) + { + bool value = (*d_options)[options::printExprTypes]; + Debug.getStream() << expr::ExprPrintTypes(value); + Trace.getStream() << expr::ExprPrintTypes(value); + Notice.getStream() << expr::ExprPrintTypes(value); + Chat.getStream() << expr::ExprPrintTypes(value); + Message.getStream() << expr::ExprPrintTypes(value); + Warning.getStream() << expr::ExprPrintTypes(value); + // intentionally exclude Dump stream from this list + } + else if (key == options::dumpModeString.getName()) + { + const std::string& value = (*d_options)[options::dumpModeString]; + Dump.setDumpFromString(value); + } + else if (key == options::printSuccess.getName()) + { + bool value = (*d_options)[options::printSuccess]; + Debug.getStream() << Command::printsuccess(value); + Trace.getStream() << Command::printsuccess(value); + Notice.getStream() << Command::printsuccess(value); + Chat.getStream() << Command::printsuccess(value); + Message.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) +{ + // set up the timeouts and resource limits + if ((*d_options)[options::perCallResourceLimit] != 0) + { + d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false); + } + if ((*d_options)[options::cumulativeResourceLimit] != 0) + { + d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(), + true); + } + if ((*d_options)[options::perCallMillisecondLimit] != 0) + { + d_resourceManager->setTimeLimit(options::perCallMillisecondLimit()); + } + // ensure that our heuristics are properly set up + setDefaults(logic, isInternalSubsolver); +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h new file mode 100644 index 000000000..bc58f17ba --- /dev/null +++ b/src/smt/options_manager.h @@ -0,0 +1,73 @@ +/********************* */ +/*! \file options_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Module for managing options of an SmtEngine. + **/ + +#ifndef CVC4__SMT__OPTIONS_MANAGER_H +#define CVC4__SMT__OPTIONS_MANAGER_H + +#include "options/options.h" +#include "options/options_listener.h" + +namespace CVC4 { + +class SmtEngine; +class LogicInfo; +class ResourceManager; + +namespace smt { + +/** + * This class is intended to be used by SmtEngine, and is responsible for: + * (1) Implementing core options including timeouts and output preferences, + * (2) Setting default values for options based on a logic. + * + * Notice that the constructor of this class retroactively sets all + * necessary options that have already been set in the options object it is + * given. This is to ensure that the command line arguments, which modified + * on an options object in the driver, immediately take effect upon creation of + * this class. + */ +class OptionsManager : public OptionsListener +{ + public: + OptionsManager(Options* opts, ResourceManager* rm = nullptr); + ~OptionsManager(); + /** + * Called when a set option call is made on the options object associated + * with this class. This handles all options that should be taken into account + * immediately instead of e.g. at SmtEngine::finishInit time. This primarily + * includes options related to parsing and output. + * + * This function call is made after the option has been updated. This means + * that the value of the option can be queried in the options object that + * this class is listening to. + */ + void notifySetOption(const std::string& key) override; + /** + * Finish init, which is called at the beginning of SmtEngine::finishInit, + * just before solving begins. This initializes the options pertaining to + * time limits, and sets the default options. + */ + void finishInit(LogicInfo& logic, bool isInternalSubsolver); + + private: + /** Reference to the options object */ + Options* d_options; + /** Pointer to the resource manager */ + ResourceManager* d_resourceManager; +}; + +} // namespace smt +} // namespace CVC4 + +#endif /* CVC4__SMT__OPTIONS_MANAGER_H */ -- 2.30.2