Replace options listener infrastructure (#4764)

This replaces the old options listener infrastructure with the OptionsManager introduced in cb8d041.

It eliminates a "beforeSearchListener", which was a custom way of some options throwing a modal exception if they were set after initialization. Now all options are consistent: no option can be set after initialization.

It also moves managed ostream objects to the OptionsManager.

@mpreiner The next step will be to remove the "notifies" field from the Options build system and then proceed with cleaning src/options/.

19 files changed, 75 insertions, 875 deletions

diff --git a/src/base/listener.cpp b/src/base/listener.cpp
index 63617f978..0800e4b43 100644
--- a/src/base/listener.cpp
+++ b/src/base/listener.cpp
@@ -25,75 +25,5 @@ namespace CVC4 {
 Listener::Listener(){}
 Listener::~Listener(){}
 
-ListenerCollection::ListenerCollection() : d_listeners() {}
-ListenerCollection::~ListenerCollection() { Assert(empty()); }
-
-ListenerCollection::iterator ListenerCollection::addListener(Listener* listener)
-{
-  return d_listeners.insert(d_listeners.end(), listener);
-}
-
-void ListenerCollection::removeListener(iterator position) {
-  d_listeners.erase(position);
-}
-
-void ListenerCollection::notify() {
-  for(iterator i = d_listeners.begin(), iend = d_listeners.end(); i != iend;
-      ++i)
-  {
-    Listener* listener = *i;
-    listener->notify();
-  }
-}
-
-bool ListenerCollection::empty() const { return d_listeners.empty(); }
-
-
-ListenerCollection::Registration::Registration(
-    ListenerCollection* collection, Listener* listener)
-    : d_listener(listener)
-    , d_position()
-    , d_collection(collection)
-{
-  d_position = d_collection->addListener(d_listener);
-}
-
-ListenerCollection::Registration::~Registration() {
-  d_collection->removeListener(d_position);
-  delete d_listener;
-}
-
- ListenerCollection::Registration* ListenerCollection::registerListener(
-     Listener* listener)
-{
-  return new Registration(this, listener);
-}
-
-
-ListenerRegistrationList::ListenerRegistrationList()
-    : d_registrations()
-{}
-
-ListenerRegistrationList::~ListenerRegistrationList() {
-  clear();
-}
-
-void ListenerRegistrationList::add(
-    ListenerCollection::Registration* registration)
-{
-  d_registrations.push_back(registration);
-}
-
-void ListenerRegistrationList::clear(){
-  typedef std::list<ListenerCollection::Registration*>::iterator iterator;
-  for(iterator i = d_registrations.begin(), iend = d_registrations.end();
-      i != iend; ++i)
-  {
-    ListenerCollection::Registration* current = *i;
-    delete current;
-  }
-  d_registrations.clear();
-}
-
 
 }/* CVC4 namespace */
diff --git a/src/base/listener.h b/src/base/listener.h
index e131d0420..2e682b7ba 100644
--- a/src/base/listener.h
+++ b/src/base/listener.h
@@ -12,10 +12,7 @@
  ** \brief Utility classes for listeners and collections of listeners.
  **
  ** Utilities for the development of a Listener interface class. This class
- ** provides a single notification that must be overwritten. This file also
- ** provides a utility class for a collection of listeners and an RAII style
- ** Registration class for managing the relationship between Listeners
- ** and the collection.
+ ** provides a single notification that must be overwritten.
  **/
 
 #include "cvc4_public.h"
@@ -41,124 +38,6 @@ public:
   virtual void notify() = 0;
 };
 
-/**
- * ListenerCollection is a list of Listener instances.
- * One can add and remove Listeners.
- *
- * ListenerCollection does not own the memory of the Listeners.
- * As a sanity check, it asserted that all of its listeners
- * have been removed.
- */
-class CVC4_PUBLIC ListenerCollection {
-public:
-  typedef std::list<Listener*> ListenerList;
-  typedef ListenerList::iterator iterator;
-
-  /** Creates an empty listener collection. */
-  ListenerCollection();
-
-  /**
-   * Destroys an iterator collection.
-   * If assertions are on, this throws an AssertionException if the collection
-   * is not empty().
-   */
-  ~ListenerCollection();
-
-  /**
-   * This adds a listener to the current collection and returns
-   * an iterator to the listener in the collection.
-   * The user of the collection must call removeListener() using
-   * this iterator.
-   * The collection does not take over the memory for the listener.
-   */
-  iterator addListener(Listener* listener);
-
-  /**
-   * Remove an listener using the iterator distributed when adding the
-   * listener.
-   */
-  void removeListener(iterator position);
-
-  /** Calls notify() on all listeners in the collection. */
-  void notify();
-
-  /** Returns true if the collection contains no listeners. */
-  bool empty() const;
-
-  /**
-   * Registration is an RAII utility function for using Listener
-   * with ListenerCollection.
-   *
-   * On construction, the Registration takes a ListenerCollection,
-   * collection,
-   * and a Listener*, listener. It takes over the memory for listener. It then
-   * adds listener to collection. On destruction it removes listener and calls
-   * delete on listener.
-   *
-   * Because of this usage, a Registration must be destroyed before the
-   * ListenerCollection it is attached to.
-   */
-  class CVC4_PUBLIC Registration {
-  public:
-    Registration(ListenerCollection* collection, Listener* listener);
-    ~Registration();
-
-  private:
-    Listener* d_listener;
-    ListenerCollection::iterator d_position;
-    ListenerCollection* d_collection;
-  };/* class CVC4::ListenerCollection::Registration */
-
-
-  /**
-   * Returns a new Registration given a Listener that is attached to this
-   * ListenerCollection. Management of the memory is handed to the user of
-   * this function. To remove the listener, call the destructor for the
-   * Registration.
-   */
-  Registration* registerListener(Listener* listener);
-
-private:
-
-  /**
-   * Disabling the copy-constructor.
-   * The user of the class must be know to remove listeners on the collection.
-   * Allowing copies will only cause confusion.
-   */
-  ListenerCollection(const ListenerCollection& copy) = delete;
-
-  /**
-   * Disabling the assignment operator.
-   * The user of the class must be know to remove listeners on the collection.
-   * Allowing copies will only cause confusion.
-   */
-  ListenerCollection& operator=(const ListenerCollection& copy) = delete;
-
-  /** A list of the listeners in the collection.*/
-  ListenerList d_listeners;
-};/* class CVC4::ListenerCollection */
-
-/**
- * A list of ListenerCollection::Registration* pointers.
- *
- * This list assumes it has control over all of the memory of the registrations.
- */
-class ListenerRegistrationList {
- public:
-  ListenerRegistrationList();
-  ~ListenerRegistrationList();
-
-  void add(ListenerCollection::Registration* registration);
-  void clear();
-
- private:
-  /** Disallow copying.*/
-  ListenerRegistrationList(const ListenerRegistrationList&) = delete;
-  /** Disallow assignment.*/
-  ListenerRegistrationList operator=(const ListenerRegistrationList&) = delete;
-  std::list<ListenerCollection::Registration*> d_registrations;
-};/* class CVC4::ListenerRegistrationList */
-
 }/* CVC4 namespace */
 
 #endif /* CVC4__LISTENER_H */
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 65eeda3ae..cab4332b8 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -151,6 +151,5 @@ header = "options/base_options.h"
   category   = "regular"
   long       = "print-success"
   type       = "bool"
-  notifies   = ["notifyPrintSuccess"]
   read_only  = true
   help       = "print the \"success\" output required of SMT-LIBv2"
diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index 5f70aee43..037d46169 100644
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -9,7 +9,6 @@ header = "options/expr_options.h"
   type       = "int"
   default    = "0"
   predicates = ["setDefaultExprDepthPredicate"]
-  notifies   = ["notifySetDefaultExprDepth"]
   read_only  = true
   help       = "print exprs to depth N (0 == default, -1 == no limit)"
 
@@ -21,7 +20,6 @@ header = "options/expr_options.h"
   type       = "int"
   default    = "1"
   predicates = ["setDefaultDagThreshPredicate"]
-  notifies   = ["notifySetDefaultDagThresh"]
   read_only  = true
   help       = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
 
@@ -31,7 +29,6 @@ header = "options/expr_options.h"
   long       = "print-expr-types"
   type       = "bool"
   default    = "false"
-  notifies   = ["notifySetPrintExprTypes"]
   read_only  = true
   help       = "print types with variables when printing exprs"
 
diff --git a/src/options/options.h b/src/options/options.h
index 2ea72ca92..44f4be7b4 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -53,36 +53,6 @@ class CVC4_PUBLIC Options {
   /** The current Options in effect */
   static thread_local Options* s_current;
 
-  /** Listeners for notifyBeforeSearch. */
-  ListenerCollection d_beforeSearchListeners;
-
-  /** Listeners for options::defaultExprDepth. */
-  ListenerCollection d_setDefaultExprDepthListeners;
-
-  /** Listeners for options::defaultDagThresh. */
-  ListenerCollection d_setDefaultDagThreshListeners;
-
-  /** Listeners for options::printExprTypes. */
-  ListenerCollection d_setPrintExprTypesListeners;
-
-  /** Listeners for options::dumpModeString. */
-  ListenerCollection d_setDumpModeListeners;
-
-  /** Listeners for options::printSuccess. */
-  ListenerCollection d_setPrintSuccessListeners;
-
-  /** Listeners for options::dumpToFileName. */
-  ListenerCollection d_dumpToFileListeners;
-
-  /** Listeners for options::regularChannelName. */
-  ListenerCollection d_setRegularChannelListeners;
-
-  /** Listeners for options::diagnosticChannelName. */
-  ListenerCollection d_setDiagnosticChannelListeners;
-
-  static ListenerCollection::Registration* registerAndNotify(
-      ListenerCollection& collection, Listener* listener, bool notify);
-
   /** Low-level assignment function for options */
   template <class T>
   void assign(T, std::string option, std::string value);
@@ -304,113 +274,6 @@ public:
 
   /** Set the generic listener associated with this class to ol */
   void setListener(OptionsListener* ol);
-  /**
-   * Registers a listener for the notification, notifyBeforeSearch.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   *
-   * This has multiple usages so having a notifyIfSet flag does not add
-   * clarity. Users should check the relevant flags before registering this.
-   */
-  ListenerCollection::Registration* registerBeforeSearchListener(
-      Listener* listener);
-
-  /**
-   * Registers a listener for options::defaultExprDepth being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetDefaultExprDepthListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::defaultDagThresh being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetDefaultExprDagListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::printExprTypes being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetPrintExprTypesListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::dumpModeString being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetDumpModeListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::printSuccess being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetPrintSuccessListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::dumpToFileName being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerDumpToFileNameListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::regularChannelName being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetRegularOutputChannelListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::diagnosticChannelName being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetDiagnosticOutputChannelListener(
-      Listener* listener, bool notifyIfSet);
 
   /** Sends a std::flush to getErr(). */
   void flushErr();
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 40f9b898e..b752bfdda 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -69,17 +69,6 @@ void throwLazyBBUnsupported(options::SatSolverMode m)
 
 OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
 
-void OptionsHandler::notifyBeforeSearch(const std::string& option)
-{
-  try{
-    d_options->d_beforeSearchListeners.notify();
-  } catch (ModalException&){
-    std::stringstream ss;
-    ss << "cannot change option `" << option << "' after final initialization";
-    throw ModalException(ss.str());
-  }
-}
-
 unsigned long OptionsHandler::limitHandler(std::string option,
                                            std::string optarg)
 {
@@ -92,12 +81,6 @@ unsigned long OptionsHandler::limitHandler(std::string option,
   }
   return ms;
 }
-
-/* options/base_options_handlers.h */
-void OptionsHandler::notifyPrintSuccess(std::string option) {
-  d_options->d_setPrintSuccessListeners.notify();
-}
-
 // theory/quantifiers/options_handlers.h
 
 void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
@@ -310,19 +293,6 @@ void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) {
 #endif /* CVC4_USE_LFSC */
 }
 
-void OptionsHandler::notifyDumpToFile(std::string option) {
-  d_options->d_dumpToFileListeners.notify();
-}
-
-
-void OptionsHandler::notifySetRegularOutputChannel(std::string option) {
-  d_options->d_setRegularChannelListeners.notify();
-}
-
-void OptionsHandler::notifySetDiagnosticOutputChannel(std::string option) {
-  d_options->d_setDiagnosticChannelListeners.notify();
-}
-
 void OptionsHandler::statsEnabledBuild(std::string option, bool value)
 {
 #ifndef CVC4_STATISTICS_ON
@@ -338,12 +308,6 @@ void OptionsHandler::threadN(std::string option) {
   throw OptionException(option + " is not a real option by itself.  Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
 }
 
-void OptionsHandler::notifyDumpMode(std::string option)
-{
-  d_options->d_setDumpModeListeners.notify();
-}
-
-
 // expr/options_handlers.h
 void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
   if(depth < -1) {
@@ -357,19 +321,6 @@ void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
   }
 }
 
-void OptionsHandler::notifySetDefaultExprDepth(std::string option) {
-  d_options->d_setDefaultExprDepthListeners.notify();
-}
-
-void OptionsHandler::notifySetDefaultDagThresh(std::string option) {
-  d_options->d_setDefaultDagThreshListeners.notify();
-}
-
-void OptionsHandler::notifySetPrintExprTypes(std::string option) {
-  d_options->d_setPrintExprTypesListeners.notify();
-}
-
-
 // main/options_handlers.h
 
 static void print_config (const char * str, std::string config) {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 876edfad7..221e6179f 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -84,14 +84,9 @@ public:
    * Throws a ModalException if this option is being set after final
    * initialization.
    */
-  void notifyBeforeSearch(const std::string& option);
-  void notifyDumpMode(std::string option);
   void setProduceAssertions(std::string option, bool value);
   void proofEnabledBuild(std::string option, bool value);
   void LFSCEnabledBuild(std::string option, bool value);
-  void notifyDumpToFile(std::string option);
-  void notifySetRegularOutputChannel(std::string option);
-  void notifySetDiagnosticOutputChannel(std::string option);
 
   void statsEnabledBuild(std::string option, bool value);
 
@@ -100,9 +95,6 @@ public:
   /* expr/options_handlers.h */
   void setDefaultExprDepthPredicate(std::string option, int depth);
   void setDefaultDagThreshPredicate(std::string option, int dag);
-  void notifySetDefaultExprDepth(std::string option);
-  void notifySetDefaultDagThresh(std::string option);
-  void notifySetPrintExprTypes(std::string option);
 
   /* main/options_handlers.h */
   void copyright(std::string option);
@@ -119,7 +111,6 @@ public:
   InputLanguage stringToInputLanguage(std::string option, std::string optarg);
   void enableTraceTag(std::string option, std::string optarg);
   void enableDebugTag(std::string option, std::string optarg);
-  void notifyPrintSuccess(std::string option);
 
  private:
 
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index b4aa3dae0..5afa9173e 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -224,12 +224,10 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h
   // that can throw exceptions.
 }
 
-
 Options::Options(OptionsListener* ol)
-    : d_holder(new options::OptionsHolder())
-    , d_handler(new options::OptionsHandler(this))
-    , d_beforeSearchListeners(),
-    d_olisten(ol)
+    : d_holder(new options::OptionsHolder()),
+      d_handler(new options::OptionsHandler(this)),
+      d_olisten(ol)
 {}
 
 Options::~Options() {
@@ -254,94 +252,6 @@ std::string Options::formatThreadOptionException(const std::string& option) {
 
 void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
 
-ListenerCollection::Registration* Options::registerAndNotify(
-    ListenerCollection& collection, Listener* listener, bool notify)
-{
-  ListenerCollection::Registration* registration =
-      collection.registerListener(listener);
-  if(notify) {
-    try
-    {
-      listener->notify();
-    }
-    catch (OptionException& e)
-    {
-      // It can happen that listener->notify() throws an OptionException. In
-      // that case, we have to make sure that we delete the registration of our
-      // listener before rethrowing the exception. Otherwise the
-      // ListenerCollection deconstructor will complain that not all
-      // registrations have been removed before invoking the deconstructor.
-      delete registration;
-      throw OptionException(e.getRawMessage());
-    }
-  }
-  return registration;
-}
-
-ListenerCollection::Registration* Options::registerBeforeSearchListener(
-   Listener* listener)
-{
-  return d_beforeSearchListeners.registerListener(listener);
-}
-
-ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::defaultExprDepth);
-  return registerAndNotify(d_setDefaultExprDepthListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetDefaultExprDagListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::defaultDagThresh);
-  return registerAndNotify(d_setDefaultDagThreshListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetPrintExprTypesListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::printExprTypes);
-  return registerAndNotify(d_setPrintExprTypesListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetDumpModeListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::dumpModeString);
-  return registerAndNotify(d_setDumpModeListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetPrintSuccessListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::printSuccess);
-  return registerAndNotify(d_setPrintSuccessListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerDumpToFileNameListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::dumpToFileName);
-  return registerAndNotify(d_dumpToFileListeners, listener, notify);
-}
-
-ListenerCollection::Registration*
-Options::registerSetRegularOutputChannelListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::regularChannelName);
-  return registerAndNotify(d_setRegularChannelListeners, listener, notify);
-}
-
-ListenerCollection::Registration*
-Options::registerSetDiagnosticOutputChannelListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::diagnosticChannelName);
-  return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify);
-}
-
 ${custom_handlers}$
 
 #if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
@@ -497,7 +407,6 @@ std::vector<std::string> Options::parseOptions(Options* options,
   }
   options->d_holder->binary_name = std::string(progName);
 
-
   std::vector<std::string> nonoptions;
   parseOptionsRecursive(options, argc, argv, &nonoptions);
   if(Debug.isOn("options")){
@@ -688,11 +597,9 @@ void Options::setOptionInternal(const std::string& key,
 
 std::string Options::getOption(const std::string& key) const
 {
-  Trace("options") << "SMT getOption(" << key << ")" << std::endl;
-
+  Trace("options") << "Options::getOption(" << key << ")" << std::endl;
   ${getoption_handlers}$
 
-
   throw UnrecognizedOptionException(key);
 }
 
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 18a99ad3c..3fecab5c9 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -8,7 +8,6 @@ header = "options/smt_options.h"
   category   = "common"
   long       = "dump=MODE"
   type       = "std::string"
-  notifies   = ["notifyDumpMode"]
   read_only  = true
   help       = "dump preprocessed assertions, etc., see --dump=help"
 
@@ -18,7 +17,6 @@ header = "options/smt_options.h"
   category   = "common"
   long       = "dump-to=FILE"
   type       = "std::string"
-  notifies   = ["notifyDumpToFile"]
   read_only  = true
   help       = "all dumping goes to FILE (instead of stdout)"
 
@@ -71,7 +69,6 @@ header = "options/smt_options.h"
   long       = "produce-models"
   type       = "bool"
   default    = "false"
-  notifies   = ["notifyBeforeSearch"]
   help       = "support the get-value and get-model commands"
 
 [[option]]
@@ -79,7 +76,6 @@ header = "options/smt_options.h"
   category   = "regular"
   long       = "check-models"
   type       = "bool"
-  notifies   = ["notifyBeforeSearch"]
   help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions"
 
 [[option]]
@@ -87,7 +83,6 @@ header = "options/smt_options.h"
   category   = "regular"
   long       = "debug-check-models"
   type       = "bool"
-  notifies   = ["notifyBeforeSearch"]
   help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions"
 
 [[option]]
@@ -143,7 +138,6 @@ header = "options/smt_options.h"
   type       = "bool"
   default    = "false"
   predicates = ["proofEnabledBuild"]
-  notifies   = ["notifyBeforeSearch"]
   help       = "turn on proof generation"
 
 [[option]]
@@ -152,7 +146,6 @@ header = "options/smt_options.h"
   long       = "check-proofs"
   type       = "bool"
   predicates = ["LFSCEnabledBuild"]
-  notifies   = ["notifyBeforeSearch"]
   help       = "after UNSAT/VALID, machine-check the generated proof"
 
 [[option]]
@@ -234,7 +227,6 @@ header = "options/smt_options.h"
   long       = "produce-unsat-cores"
   type       = "bool"
   predicates = ["proofEnabledBuild"]
-  notifies   = ["notifyBeforeSearch"]
   help       = "turn on unsat core generation"
 
 [[option]]
@@ -250,7 +242,6 @@ header = "options/smt_options.h"
   long       = "dump-unsat-cores"
   type       = "bool"
   default    = "false"
-  notifies   = ["notifyBeforeSearch"]
   help       = "output unsat cores after every UNSAT/VALID response"
 
 [[option]]
@@ -259,7 +250,6 @@ header = "options/smt_options.h"
   long       = "dump-unsat-cores-full"
   type       = "bool"
   default    = "false"
-  notifies   = ["notifyBeforeSearch"]
   read_only  = true
   help       = "dump the full unsat core, including unlabeled assertions"
 
@@ -270,7 +260,6 @@ header = "options/smt_options.h"
   type       = "bool"
   default    = "false"
   predicates = ["proofEnabledBuild"]
-  notifies   = ["notifyBeforeSearch"]
   read_only  = true
   help       = "turn on unsat assumptions generation"
 
@@ -288,7 +277,6 @@ header = "options/smt_options.h"
   long       = "produce-assignments"
   type       = "bool"
   default    = "false"
-  notifies   = ["notifyBeforeSearch"]
   help       = "support the get-assignment command"
 
 [[option]]
@@ -297,7 +285,6 @@ header = "options/smt_options.h"
   category   = "undocumented"
   type       = "bool"
   predicates = ["setProduceAssertions"]
-  notifies   = ["notifyBeforeSearch"]
   help       = "deprecated name for produce-assertions"
 
 [[option]]
@@ -306,7 +293,6 @@ header = "options/smt_options.h"
   long       = "produce-assertions"
   type       = "bool"
   predicates = ["setProduceAssertions"]
-  notifies   = ["notifyBeforeSearch"]
   help       = "keep an assertions list (enables get-assertions command)"
 
 [[option]]
@@ -429,7 +415,6 @@ header = "options/smt_options.h"
   smt_name   = "regular-output-channel"
   category   = "regular"
   type       = "std::string"
-  notifies   = ["notifySetRegularOutputChannel"]
   read_only  = true
   help       = "set the regular output channel of the solver"
 
@@ -438,7 +423,6 @@ header = "options/smt_options.h"
   smt_name   = "diagnostic-output-channel"
   category   = "regular"
   type       = "std::string"
-  notifies   = ["notifySetDiagnosticOutputChannel"]
   read_only  = true
   help       = "set the diagnostic output channel of the solver"
 
diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index 577ef3226..c53def1f8 100644
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -74,20 +74,6 @@ class ManagedOstream {
   std::ostream* d_managed;
 }; /* class ManagedOstream */
 
-class SetToDefaultSourceListener : public Listener {
- public:
-  SetToDefaultSourceListener(ManagedOstream* managedOstream)
-      : d_managedOstream(managedOstream){}
-
-  void notify() override
-  {
-    d_managedOstream->set(d_managedOstream->defaultSource());
-  }
-
- private:
-  ManagedOstream* d_managedOstream;
-};
-
 /**
  * This controls the memory associated with --dump-to.
  * This is is assumed to recieve a set whenever diagnosticChannelName
diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 5b976bc31..ce5652650 100644
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -51,6 +51,18 @@ OptionsManager::OptionsManager(Options* opts, ResourceManager* rm)
   {
     notifySetOption(options::printSuccess.getName());
   }
+  if (opts->wasSetByUser(options::diagnosticChannelName))
+  {
+    notifySetOption(options::diagnosticChannelName.getName());
+  }
+  if (opts->wasSetByUser(options::regularChannelName))
+  {
+    notifySetOption(options::regularChannelName.getName());
+  }
+  if (opts->wasSetByUser(options::dumpToFileName))
+  {
+    notifySetOption(options::dumpToFileName.getName());
+  }
   // set this as a listener to be notified of options changes from now on
   opts->setListener(this);
 }
@@ -110,6 +122,18 @@ void OptionsManager::notifySetOption(const std::string& key)
     Warning.getStream() << Command::printsuccess(value);
     *options::out() << Command::printsuccess(value);
   }
+  else if (key == options::regularChannelName.getName())
+  {
+    d_managedRegularChannel.set(options::regularChannelName());
+  }
+  else if (key == options::diagnosticChannelName.getName())
+  {
+    d_managedDiagnosticChannel.set(options::diagnosticChannelName());
+  }
+  else if (key == options::dumpToFileName.getName())
+  {
+    d_managedDumpChannel.set(options::dumpToFileName());
+  }
   // otherwise, no action is necessary
 }
 
diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h
index bc58f17ba..ad5fe9fa2 100644
--- a/src/smt/options_manager.h
+++ b/src/smt/options_manager.h
@@ -17,6 +17,7 @@
 
 #include "options/options.h"
 #include "options/options_listener.h"
+#include "smt/managed_ostreams.h"
 
 namespace CVC4 {
 
@@ -65,6 +66,12 @@ class OptionsManager : public OptionsListener
   Options* d_options;
   /** Pointer to the resource manager */
   ResourceManager* d_resourceManager;
+  /** Manager for the memory of regular-output-channel. */
+  ManagedRegularOutputChannel d_managedRegularChannel;
+  /** Manager for the memory of diagnostic-output-channel. */
+  ManagedDiagnosticOutputChannel d_managedDiagnosticChannel;
+  /** Manager for the memory of --dump-to. */
+  ManagedDumpOStream d_managedDumpChannel;
 };
 
 }  // namespace smt
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index 606921b7c..972d828bd 100644
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -28,7 +28,7 @@ namespace smt {
  * updated by this method based on the current options and the logic itself.
  * @param isInternalSubsolver Whether we are setting the options for an
  * internal subsolver (see SmtEngine::isInternalSubsolver).
- * 
+ *
  * NOTE: we currently modify the current options in scope. This method
  * can be further refactored to modify an options object provided as an
  * explicit argument.
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 16e4e916a..c8896b621 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -81,17 +81,16 @@
 #include "proof/theory_proof.h"
 #include "proof/unsat_core.h"
 #include "prop/prop_engine.h"
-#include "smt/abstract_values.h"
 #include "smt/abduction_solver.h"
+#include "smt/abstract_values.h"
 #include "smt/command.h"
 #include "smt/command_list.h"
 #include "smt/defined_function.h"
 #include "smt/logic_request.h"
-#include "smt/managed_ostreams.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
+#include "smt/options_manager.h"
 #include "smt/process_assertions.h"
-#include "smt/set_defaults.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_engine_stats.h"
 #include "smt/term_formula_removal.h"
@@ -161,86 +160,6 @@ class ResourceOutListener : public Listener {
   SmtEngine* d_smt;
 }; /* class ResourceOutListener */
 
-class BeforeSearchListener : public Listener {
- public:
-  BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {}
-  void notify() override { d_smt->beforeSearch(); }
-
- private:
-  SmtEngine* d_smt;
-}; /* class BeforeSearchListener */
-
-class SetDefaultExprDepthListener : public Listener {
- public:
-  void notify() override
-  {
-    int depth = 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
-  }
-};
-
-class SetDefaultExprDagListener : public Listener {
- public:
-  void notify() override
-  {
-    int dag = 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);
-  }
-};
-
-class SetPrintExprTypesListener : public Listener {
- public:
-  void notify() override
-  {
-    bool value = 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
-  }
-};
-
-class DumpModeListener : public Listener {
- public:
-  void notify() override
-  {
-    const std::string& value = options::dumpModeString();
-    Dump.setDumpFromString(value);
-  }
-};
-
-class PrintSuccessListener : public Listener {
- public:
-  void notify() override
-  {
-    bool value = 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);
-  }
-};
-
-
-
 /**
  * This is an inelegant solution, but for the present, it will work.
  * The point of this is to separate the public and private portions of
@@ -261,25 +180,13 @@ class SmtEnginePrivate : public NodeManagerListener {
   typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
   typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 
-  /** Manager for the memory of regular-output-channel. */
-  ManagedRegularOutputChannel d_managedRegularChannel;
-
-  /** Manager for the memory of diagnostic-output-channel. */
-  ManagedDiagnosticOutputChannel d_managedDiagnosticChannel;
-
-  /** Manager for the memory of --dump-to. */
-  ManagedDumpOStream d_managedDumpChannel;
-
   /**
-   * This list contains:
-   *  softResourceOut
-   *  hardResourceOut
-   *  beforeSearchListener
-   *
-   * This needs to be deleted before both NodeManager's Options,
-   * SmtEngine, d_resourceManager, and TheoryEngine.
+   * Manager for limiting time and abstract resource usage.
    */
-  ListenerRegistrationList* d_listenerRegistrations;
+  ResourceManager* d_resourceManager;
+
+  /** Resource out listener */
+  std::unique_ptr<ResourceOutListener> d_routListener;
 
   /** A circuit propagator for non-clausal propositional deduction */
   booleans::CircuitPropagator d_propagator;
@@ -333,15 +240,11 @@ class SmtEnginePrivate : public NodeManagerListener {
  public:
   SmtEnginePrivate(SmtEngine& smt)
       : d_smt(smt),
-        d_managedRegularChannel(),
-        d_managedDiagnosticChannel(),
-        d_managedDumpChannel(),
-        d_listenerRegistrations(new ListenerRegistrationList()),
+        d_routListener(new ResourceOutListener(d_smt)),
         d_propagator(true, true),
         d_assertions(),
         d_assertionsProcessed(smt.getUserContext(), false),
         d_processor(smt, *smt.getResourceManager()),
-        // d_needsExpandDefs(true),  //TODO?
         d_exprNames(smt.getUserContext()),
         d_iteRemover(smt.getUserContext()),
         d_sygusConjectureStale(smt.getUserContext(), true)
@@ -349,62 +252,11 @@ class SmtEnginePrivate : public NodeManagerListener {
     d_smt.d_nodeManager->subscribeEvents(this);
     d_true = NodeManager::currentNM()->mkConst(true);
     ResourceManager* rm = d_smt.getResourceManager();
-
-    d_listenerRegistrations->add(
-        rm->registerListener(new ResourceOutListener(d_smt)));
-
-    try
-    {
-      Options& opts = d_smt.getOptions();
-      // Multiple options reuse BeforeSearchListener so registration requires an
-      // extra bit of care.
-      // We can safely not call notify on this before search listener at
-      // registration time. This d_smt cannot be beforeSearch at construction
-      // time. Therefore the BeforeSearchListener is a no-op. Therefore it does
-      // not have to be called.
-      d_listenerRegistrations->add(
-          opts.registerBeforeSearchListener(new BeforeSearchListener(d_smt)));
-
-      // These do need registration calls.
-      d_listenerRegistrations->add(opts.registerSetDefaultExprDepthListener(
-          new SetDefaultExprDepthListener(), true));
-      d_listenerRegistrations->add(opts.registerSetDefaultExprDagListener(
-          new SetDefaultExprDagListener(), true));
-      d_listenerRegistrations->add(opts.registerSetPrintExprTypesListener(
-          new SetPrintExprTypesListener(), true));
-      d_listenerRegistrations->add(
-          opts.registerSetDumpModeListener(new DumpModeListener(), true));
-      d_listenerRegistrations->add(opts.registerSetPrintSuccessListener(
-          new PrintSuccessListener(), true));
-      d_listenerRegistrations->add(opts.registerSetRegularOutputChannelListener(
-          new SetToDefaultSourceListener(&d_managedRegularChannel), true));
-      d_listenerRegistrations->add(
-          opts.registerSetDiagnosticOutputChannelListener(
-              new SetToDefaultSourceListener(&d_managedDiagnosticChannel),
-              true));
-      d_listenerRegistrations->add(opts.registerDumpToFileNameListener(
-          new SetToDefaultSourceListener(&d_managedDumpChannel), true));
-    }
-    catch (OptionException& e)
-    {
-      // Registering the option listeners can lead to OptionExceptions, e.g.
-      // when the user chooses a dump tag that does not exist. In that case, we
-      // have to make sure that we delete existing listener registrations and
-      // that we unsubscribe from NodeManager events. Otherwise we will have
-      // errors in the deconstructors of the NodeManager (because the
-      // NodeManager tries to notify an SmtEnginePrivate that does not exist)
-      // and the ListenerCollection (because not all registrations have been
-      // removed before calling the deconstructor).
-      delete d_listenerRegistrations;
-      d_smt.d_nodeManager->unsubscribeEvents(this);
-      throw OptionException(e.getRawMessage());
-    }
+    rm->registerListener(d_routListener.get());
   }
 
   ~SmtEnginePrivate()
   {
-    delete d_listenerRegistrations;
-
     if(d_propagator.getNeedsFinish()) {
       d_propagator.finish();
       d_propagator.setNeedsFinish(false);
@@ -620,6 +472,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
   d_statisticsRegistry.reset(new StatisticsRegistry());
   d_resourceManager.reset(
       new ResourceManager(*d_statisticsRegistry.get(), d_options));
+  d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get()));
   d_private.reset(new smt::SmtEnginePrivate(*this));
   d_stats.reset(new SmtEngineStatistics());
   
@@ -645,27 +498,14 @@ void SmtEngine::finishInit()
   // parsing smt2, this occurs at the moment we enter "Assert mode", page 52
   // of SMT-LIB 2.6 standard.
 
-  // Inialize the resource manager based on the options.
-  if (options::perCallResourceLimit() != 0)
-  {
-    d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
-  }
-  if (options::cumulativeResourceLimit() != 0)
-  {
-    d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(),
-                                        true);
-  }
-  if (options::perCallMillisecondLimit() != 0)
-  {
-    d_resourceManager->setTimeLimit(options::perCallMillisecondLimit());
-  }
-
   // set the random seed
   Random::getRandom().setSeed(options::seed());
 
-  // ensure that our heuristics are properly set up
-  setDefaults(d_logic, d_isInternalSubsolver);
-  
+  // Call finish init on the options manager. This inializes the resource
+  // manager based on the options, and sets up the best default options
+  // based on our heuristics.
+  d_optm->finishInit(d_logic, d_isInternalSubsolver);
+
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
@@ -850,6 +690,7 @@ SmtEngine::~SmtEngine()
 
     d_stats.reset(nullptr);
     d_private.reset(nullptr);
+    d_optm.reset(nullptr);
     // d_resourceManager must be destroyed before d_statisticsRegistry
     d_resourceManager.reset(nullptr);
     d_statisticsRegistry.reset(nullptr);
@@ -3425,17 +3266,14 @@ void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
   }
 }
 
-void SmtEngine::beforeSearch()
+void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
 {
+  // Always check whether the SmtEngine has been initialized (which is done
+  // upon entering Assert mode the first time). No option can  be set after
+  // initialized.
   if(d_fullyInited) {
-    throw ModalException(
-        "SmtEngine::beforeSearch called after initialization.");
+    throw ModalException("SmtEngine::setOption called after initialization.");
   }
-}
-
-
-void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
-{
   NodeManagerScope nms(d_nodeManager);
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 591b69424..b38ec2d7a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -93,6 +93,7 @@ namespace prop {
 namespace smt {
 /** Utilities */
 class AbstractValues;
+class OptionsManager;
 /** Subsolvers */
 class AbductionSolver;
 /**
@@ -856,14 +857,6 @@ class CVC4_PUBLIC SmtEngine
   void setPrintFuncInModel(Expr f, bool p);
 
   /**
-   * Check and throw a ModalException if the SmtEngine has been fully
-   * initialized.
-   *
-   * throw@ ModalException
-   */
-  void beforeSearch();
-
-  /**
    * Get expression name.
    *
    * Return true if given expressoion has a name in the current context.
@@ -1299,6 +1292,12 @@ class CVC4_PUBLIC SmtEngine
    */
   std::unique_ptr<ResourceManager> d_resourceManager;
   /**
+   * The options manager, which is responsible for implementing core options
+   * such as those related to time outs and printing. It is also responsible
+   * for set default options based on the logic.
+   */
+  std::unique_ptr<smt::OptionsManager> d_optm;
+  /**
    * The global scope object. Upon creation of this SmtEngine, it becomes the
    * SmtEngine in scope. It says the SmtEngine in scope until it is destructed,
    * or another SmtEngine is created.
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index ac1d57324..07b135b58 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -158,7 +158,6 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
       d_thisCallResourceUsed(0),
       d_thisCallResourceBudget(0),
       d_on(false),
-      d_listeners(),
       d_statistics(new ResourceManager::Statistics(stats)),
       d_options(options)
 
@@ -227,7 +226,10 @@ void ResourceManager::spendResource(unsigned amount)
                      << d_perCallTimer.elapsed() << std::endl;
     }
 
-    d_listeners.notify();
+    for (Listener* l : d_listeners)
+    {
+      l->notify();
+    }
   }
 }
 
@@ -369,10 +371,9 @@ void ResourceManager::enable(bool on)
   d_on = on;
 }
 
-ListenerCollection::Registration* ResourceManager::registerListener(
-    Listener* listener)
+void ResourceManager::registerListener(Listener* listener)
 {
-  return d_listeners.registerListener(listener);
+  return d_listeners.push_back(listener);
 }
 
 } /* namespace CVC4 */
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 57a227d7b..6a9b3e2bf 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -162,12 +162,10 @@ class CVC4_PUBLIC ResourceManager
   static uint64_t getFrequencyCount() { return s_resourceCount; }
 
   /**
-   * Registers a listener that is notified on a resource out.
-   *
-   * This Registration must be destroyed by the user before this
-   * ResourceManager.
+   * Registers a listener that is notified on a resource out or (per-call)
+   * timeout.
    */
-  ListenerCollection::Registration* registerListener(Listener* listener);
+  void registerListener(Listener* listener);
 
  private:
   /** The per-call wall clock timer. */
@@ -201,7 +199,7 @@ class CVC4_PUBLIC ResourceManager
   static const uint64_t s_resourceCount;
 
   /** Receives a notification on reaching a limit. */
-  ListenerCollection d_listeners;
+  std::vector<Listener*> d_listeners;
 
   void spendResource(unsigned amount);
 
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index af2ca0dfa..c28869dbd 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -13,7 +13,6 @@ cvc4_add_unit_test_black(datatype_black util)
 cvc4_add_unit_test_black(exception_black util)
 cvc4_add_unit_test_black(integer_black util)
 cvc4_add_unit_test_white(integer_white util)
-cvc4_add_unit_test_black(listener_black util)
 cvc4_add_unit_test_black(output_black util)
 cvc4_add_unit_test_black(rational_black util)
 cvc4_add_unit_test_white(rational_white util)
diff --git a/test/unit/util/listener_black.h b/test/unit/util/listener_black.h
deleted file mode 100644
index 2b34e8dbb..000000000
--- a/test/unit/util/listener_black.h
+++ /dev/null
@@ -1,153 +0,0 @@
-/*********************                                                        */
-/*! \file listener_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Andres Noetzli, Paul Meng
- ** 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 Black box testing of CVC4 output classes.
- **
- ** Black box testing of CVC4 output classes.
- **/
-
-#include <cxxtest/TestSuite.h>
-#include <sstream>
-
-#include "base/listener.h"
-
-using namespace CVC4;
-using namespace std;
-
-class ListenerBlack : public CxxTest::TestSuite {
-
-  std::multiset<std::string> d_events;
-
-  class EventListener : public Listener {
-   public:
-    EventListener(std::multiset<std::string>& events, std::string name)
-        : d_events(events), d_name(name) {}
-    ~EventListener() override {}
-
-    void notify() override { d_events.insert(d_name); }
-
-   private:
-    std::multiset<std::string>& d_events;
-    std::string d_name;
-  };
-
-public:
-
-  static std::multiset<std::string> mkMultiset(std::string arr[], int len){
-    return std::multiset<std::string>(arr, arr + len);
-  }
-
-  void setUp() override { d_events.clear(); }
-
-  void tearDown() override { d_events.clear(); }
-
-  void testEmptyCollection() {
-    // Makes an new collection and tests that it is empty.
-    ListenerCollection* collection = new ListenerCollection;
-    TS_ASSERT(collection->empty());
-    TS_ASSERT_THROWS_NOTHING( delete collection );
-  }
-
-  void testSingletonCollection() {
-    ListenerCollection collection;
-    std::string expected[1] = {"a"};
-    {
-      ListenerCollection::Registration a(&collection, new EventListener(d_events, "a"));
-      collection.notify();
-      TS_ASSERT(not collection.empty());
-    }
-    TS_ASSERT(collection.empty());
-    TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 1));
-  }
-
-  void testSingleRegisterTearDown() {
-    // Tests that collection succeeds at destruction after
-    // registering a single event.
-    ListenerCollection* collection = new ListenerCollection;
-    {
-      ListenerCollection::Registration a(collection, new EventListener(d_events, "a"));
-      TS_ASSERT(not collection->empty());
-      // The destructor for a now runs.
-    }
-    TS_ASSERT(collection->empty());
-    TS_ASSERT_THROWS_NOTHING( delete collection );
-  }
-
-  void testMultipleCollection() {
-    ListenerCollection* collection = new ListenerCollection;
-    {
-      ListenerCollection::Registration c(collection, new EventListener(d_events, "c"));
-      collection->notify();
-      // d_events == {"c"}
-      ListenerCollection::Registration b(collection, new EventListener(d_events, "b"));
-      ListenerCollection::Registration a(collection, new EventListener(d_events, "a"));
-      collection->notify();
-      // d_events == {"a", "b", "c", "c"}
-      TS_ASSERT(not collection->empty());
-    }
-    TS_ASSERT(collection->empty());
-    std::string expected[4] = {"a", "b", "c", "c"};
-    TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 4));
-    TS_ASSERT_THROWS_NOTHING( delete collection );
-  }
-
-  void testRegisterMiddleTearDown() {
-    // Tests that collection succeeds at destruction after
-    // registering several events.
-    ListenerCollection* collection = new ListenerCollection;
-    {
-      ListenerCollection::Registration a(collection, new EventListener(d_events, "a"));
-      ListenerCollection::Registration* b =
-          new ListenerCollection::Registration(collection, new EventListener(d_events, "b"));
-      ListenerCollection::Registration c(collection, new EventListener(d_events, "c"));
-
-      collection->notify();
-      delete b;
-      collection->notify();
-      // The destructor for a and c now run.
-      TS_ASSERT(not collection->empty());
-    }
-    TS_ASSERT(collection->empty());
-    TS_ASSERT_THROWS_NOTHING( delete collection );
-  }
-
-
-
-  void testRegisterMultiple() {
-    // This tests adds and notify multiple times.
-    ListenerCollection collection;
-
-    std::vector<ListenerCollection::Registration*> listeners;
-    for(int i = 0; i < 4 ; ++i){
-      stringstream ss; ss << i;
-      Listener* listener = new EventListener(d_events, ss.str());
-      listeners.push_back(new ListenerCollection::Registration(&collection, listener));
-      collection.notify();
-    }
-
-    TS_ASSERT(not collection.empty());
-    for(unsigned i=0; i < listeners.size(); ++i){
-      ListenerCollection::Registration* at_i = listeners[i];
-      delete at_i;
-    }
-    listeners.clear();
-    TS_ASSERT(collection.empty());
-
-    std::string expected[10] =
-        {"0", "0", "0", "0", "1", "1", "1", "2", "2", "3"};
-    TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 10));
-
-    // No more events occur.
-    collection.notify();
-    TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 10));
-  }
-
-};