summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/options/CMakeLists.txt1
-rw-r--r--src/options/options.h13
-rw-r--r--src/options/options_listener.h37
-rw-r--r--src/options/options_template.cpp27
-rw-r--r--src/smt/options_manager.cpp137
-rw-r--r--src/smt/options_manager.h73
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback