Adding a new Listener utility class. Changing the ResourceManager to use Listeners for reporting hard and soft resource out() events.

3 files changed, 167 insertions, 0 deletions

diff --git a/src/base/Makefile.am b/src/base/Makefile.am
index ed41db8ed..f2fe3f306 100644
--- a/src/base/Makefile.am
+++ b/src/base/Makefile.am
@@ -19,6 +19,8 @@ libbase_la_SOURCES = \
 	cvc4_assert.h \
 	exception.cpp \
 	exception.h \
+	listener.cpp \
+	listener.h \
 	modal_exception.h \
 	output.cpp \
 	output.h
diff --git a/src/base/listener.cpp b/src/base/listener.cpp
new file mode 100644
index 000000000..62bec5990
--- /dev/null
+++ b/src/base/listener.cpp
@@ -0,0 +1,66 @@
+/*********************                                                        */
+/*! \file managed_listener.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Output utility classes and functions
+ **
+ ** Output utility classes and functions.
+ **/
+
+#include "base/listener.h"
+
+#include <list>
+
+#include "base/cvc4_assert.h"
+
+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(); }
+
+
+RegisterListener::RegisterListener(ListenerCollection* collection,
+                                   Listener* listener)
+    : d_listener(listener)
+    , d_position()
+    , d_collection(collection)
+{
+  d_position = d_collection->addListener(d_listener);
+}
+
+RegisterListener::~RegisterListener() {
+  d_collection->removeListener(d_position);
+  delete d_listener;
+}
+
+}/* CVC4 namespace */
diff --git a/src/base/listener.h b/src/base/listener.h
new file mode 100644
index 000000000..d6828818c
--- /dev/null
+++ b/src/base/listener.h
@@ -0,0 +1,99 @@
+/*********************                                                        */
+/*! \file listener.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \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
+ ** RegisterListener class for managing the relationship between Listeners
+ ** and the manager.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LISTENER_H
+#define __CVC4__LISTENER_H
+
+#include <list>
+
+namespace CVC4 {
+
+/**
+ * Listener interface class.
+ *
+ * The interface provides a notify() function.
+ */
+class CVC4_PUBLIC Listener {
+public:
+  Listener();
+  virtual ~Listener();
+
+  /** Note that notify may throw arbitrary exceptions. */
+  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;
+
+  ListenerCollection();
+
+  ~ListenerCollection();
+
+  iterator addListener(Listener* listener);
+
+  void removeListener(iterator position);
+
+  void notify();
+
+  bool empty() const;
+
+private:
+  ListenerList d_listeners;
+};
+
+/**
+ * RegisterListener is an RAII utility function for using Listener
+ * with ListenerCollection.
+ *
+ * On construction, the RegisterListener takes a ListenerCollection, collection,
+ * and a Listener*, listener. It takes over the memory for listener. It then
+ * add listener to collection. On destruction it removes listener and calls
+ * delete on listener.
+ *
+ * Because of this usage, a RegisterListener must be destroyed before
+ * collection.
+ */
+class CVC4_PUBLIC RegisterListener {
+public:
+  RegisterListener(ListenerCollection* collection, Listener* listener);
+  ~RegisterListener();
+
+private:
+  Listener* d_listener;
+  ListenerCollection::iterator d_position;
+  ListenerCollection* d_collection;
+};
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LISTENER_H */