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.

4 files changed, 70 insertions, 8 deletions

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);
 }