Adding listeners to Options.

- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.

- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.

- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.

- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.

- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.

- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.

- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.

7 files changed, 141 insertions, 6 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index b3fb13253..c04de4421 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -31,7 +31,8 @@ libexpr_la_SOURCES = \
 	node_manager.cpp \
 	node_manager.h \
 	node_manager_attributes.h \
-	node_self_iterator.h \
+	node_manager_listeners.cpp \
+	node_manager_listeners.h \
 	node_self_iterator.h \
 	node_value.cpp \
 	node_value.h \
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 7d82cb222..d037a6bb9 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -40,7 +40,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 45 "${template}"
+#line 44 "${template}"
 
 namespace CVC4 {
 
@@ -553,7 +553,7 @@ private:
 
 ${getConst_instantiations}
 
-#line 939 "${template}"
+#line 557 "${template}"
 
 inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
   return (size_t) e.getId();
diff --git a/src/expr/node.h b/src/expr/node.h
index c0e2a5542..a51de6d66 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -30,6 +30,7 @@
 #include <functional>
 #include <stdint.h>
 
+#include "base/configuration.h"
 #include "base/cvc4_assert.h"
 #include "base/exception.h"
 #include "base/output.h"
@@ -40,7 +41,6 @@
 #include "expr/expr_iomanip.h"
 #include "options/language.h"
 #include "options/set_language.h"
-#include "util/configuration.h"
 #include "util/utility.h"
 #include "util/hash.h"
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 13960b717..e52776fce 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -23,9 +23,11 @@
 #include <utility>
 
 #include "base/cvc4_assert.h"
+#include "base/listener.h"
 #include "base/tls.h"
 #include "expr/attribute.h"
 #include "expr/node_manager_attributes.h"
+#include "expr/node_manager_listeners.h"
 #include "expr/type_checker.h"
 #include "options/options.h"
 #include "options/smt_options.h"
@@ -84,6 +86,7 @@ NodeManager::NodeManager(ExprManager* exprManager) :
   d_options(new Options()),
   d_statisticsRegistry(new StatisticsRegistry()),
   d_resourceManager(new ResourceManager()),
+  d_registrations(new ListenerRegistrationList()),
   next_id(0),
   d_attrManager(new expr::attr::AttributeManager()),
   d_exprManager(exprManager),
@@ -96,16 +99,19 @@ NodeManager::NodeManager(ExprManager* exprManager) :
 
 NodeManager::NodeManager(ExprManager* exprManager,
                          const Options& options) :
-  d_options(new Options(options)),
+  d_options(new Options()),
   d_statisticsRegistry(new StatisticsRegistry()),
   d_resourceManager(new ResourceManager()),
+  d_registrations(new ListenerRegistrationList()),
   next_id(0),
   d_attrManager(new expr::attr::AttributeManager()),
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
   d_inReclaimZombies(false),
   d_abstractValueCount(0),
-  d_skolemCounter(0) {
+  d_skolemCounter(0)
+{
+  d_options->copyValues(options);
   init();
 }
 
@@ -135,6 +141,16 @@ void NodeManager::init() {
   if((*d_options)[options::cpuTime]) {
     d_resourceManager->useCPUTime(true);
   }
+
+  // Do not notify() upon registration as these were handled manually above.
+  d_registrations->add(d_options->registerTlimitListener(
+      new TlimitListener(d_resourceManager), false));
+  d_registrations->add(d_options->registerTlimitPerListener(
+      new TlimitPerListener(d_resourceManager), false));
+  d_registrations->add(d_options->registerRlimitListener(
+      new RlimitListener(d_resourceManager), false));
+  d_registrations->add(d_options->registerRlimitPerListener(
+      new RlimitPerListener(d_resourceManager), false));
 }
 
 NodeManager::~NodeManager() {
@@ -180,6 +196,8 @@ NodeManager::~NodeManager() {
   // defensive coding, in case destruction-order issues pop up (they often do)
   delete d_statisticsRegistry;
   d_statisticsRegistry = NULL;
+  delete d_registrations;
+  d_registrations = NULL;
   delete d_resourceManager;
   d_resourceManager = NULL;
   delete d_attrManager;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 870408939..1ae9f1e8e 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -102,8 +102,15 @@ class NodeManager {
 
   Options* d_options;
   StatisticsRegistry* d_statisticsRegistry;
+
   ResourceManager* d_resourceManager;
 
+  /**
+   * A list of registrations on d_options to that call into d_resourceManager.
+   * These must be garbage collected before d_options and d_resourceManager.
+   */
+  ListenerRegistrationList* d_registrations;
+
   NodeValuePool d_nodeValuePool;
 
   size_t next_id;
@@ -295,6 +302,8 @@ class NodeManager {
   // undefined private copy constructor (disallow copy)
   NodeManager(const NodeManager&) CVC4_UNDEFINED;
 
+  NodeManager& operator=(const NodeManager&) CVC4_UNDEFINED;
+
   void init();
 
   /**
diff --git a/src/expr/node_manager_listeners.cpp b/src/expr/node_manager_listeners.cpp
new file mode 100644
index 000000000..ec2de105a
--- /dev/null
+++ b/src/expr/node_manager_listeners.cpp
@@ -0,0 +1,44 @@
+/*********************                                                        */
+/*! \file node_manager_listeners.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-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Listeners that NodeManager registers to its Options object.
+ **
+ ** Listeners that NodeManager registers to its Options object.
+ **/
+
+#include "node_manager_listeners.h"
+
+#include "base/listener.h"
+#include "options/smt_options.h"
+#include "util/resource_manager.h"
+
+namespace CVC4 {
+namespace expr {
+
+
+void TlimitListener::notify() {
+  d_rm->setTimeLimit(options::cumulativeMillisecondLimit(), true);
+}
+
+void TlimitPerListener::notify() {
+  d_rm->setTimeLimit(options::perCallMillisecondLimit(), false);
+}
+
+void RlimitListener::notify() {
+  d_rm->setTimeLimit(options::cumulativeResourceLimit(), true);
+}
+
+void RlimitPerListener::notify() {
+  d_rm->setTimeLimit(options::perCallResourceLimit(), false);
+}
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/node_manager_listeners.h b/src/expr/node_manager_listeners.h
new file mode 100644
index 000000000..fc7c2f65f
--- /dev/null
+++ b/src/expr/node_manager_listeners.h
@@ -0,0 +1,63 @@
+/*********************                                                        */
+/*! \file node_manager_listeners.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-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Listeners that NodeManager registers to its Options object.
+ **
+ ** Listeners that NodeManager registers to its Options object.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__EXPR__NODE_MANAGER_LISTENERS_H
+#define __CVC4__EXPR__NODE_MANAGER_LISTENERS_H
+
+#include "base/listener.h"
+#include "util/resource_manager.h"
+
+namespace CVC4 {
+namespace expr {
+
+class TlimitListener : public Listener {
+ public:
+  TlimitListener(ResourceManager* rm) : d_rm(rm) {}
+  virtual void notify();
+ private:
+  ResourceManager* d_rm;
+};
+
+class TlimitPerListener : public Listener {
+ public:
+  TlimitPerListener(ResourceManager* rm) : d_rm(rm) {}
+  virtual void notify();
+ private:
+  ResourceManager* d_rm;
+};
+
+class RlimitListener : public Listener {
+ public:
+  RlimitListener(ResourceManager* rm) : d_rm(rm) {}
+  virtual void notify();
+ private:
+  ResourceManager* d_rm;
+};
+
+class RlimitPerListener : public Listener {
+ public:
+  RlimitPerListener(ResourceManager* rm) : d_rm(rm) {}
+  virtual void notify();
+ private:
+  ResourceManager* d_rm;
+};
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__NODE_MANAGER_LISTENERS_H */