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.
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
options.h
options_handler.cpp
options_handler.h
+ options_listener.h
options_public_functions.cpp
printer_modes.cpp
printer_modes.h
class OptionsHandler;
}/* CVC4::options namespace */
+class OptionsListener;
+
class CVC4_PUBLIC Options {
friend api::Solver;
/** The struct that holds all option values. */
return s_current;
}
- Options();
+ Options(OptionsListener* ol = nullptr);
~Options();
/**
*/
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.
*
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
--- /dev/null
+/********************* */
+/*! \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 */
#include "options/didyoumean.h"
#include "options/language.h"
#include "options/options_handler.h"
+#include "options/options_listener.h"
${headers_module}$
}
-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() {
return ss.str();
}
+void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
+
ListenerCollection::Registration* Options::registerAndNotify(
ListenerCollection& collection, Listener* listener, bool notify)
{
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);
}
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
projects / cvc5.git / commitdiff