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/.

2 files changed, 1 insertions, 192 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 */