diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-17 13:38:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-17 13:38:50 -0500 |
commit | f99889b0c1260fccf28daac995e58312912bae9f (patch) | |
tree | c9bba127e62aedef587ee7da83950281a4c131f4 /src/base | |
parent | e8df6f67cc2654f50d49995377a4b411668235e1 (diff) |
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/.
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/listener.cpp | 70 | ||||
-rw-r--r-- | src/base/listener.h | 123 |
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 */ |