diff options
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/options/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/options/options.h | 13 | ||||
-rw-r--r-- | src/options/options_listener.h | 37 | ||||
-rw-r--r-- | src/options/options_template.cpp | 27 | ||||
-rw-r--r-- | src/smt/options_manager.cpp | 137 | ||||
-rw-r--r-- | src/smt/options_manager.h | 73 |
7 files changed, 282 insertions, 8 deletions
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<std::vector<std::string> > 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 <string> + +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<std::vector<std::string> > 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 */ |