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

11 files changed, 39 insertions, 45 deletions

diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp
index b202bcccc..bc976685e 100644
--- a/test/system/smt2_compliance.cpp
+++ b/test/system/smt2_compliance.cpp
@@ -19,9 +19,8 @@
 #include <sstream>
 
 #include "expr/expr_manager.h"
-#include "options/base_options.h"
+#include "options/options.h"
 #include "options/set_language.h"
-#include "options/smt_options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/smt_engine.h"
@@ -35,8 +34,8 @@ void testGetInfo(SmtEngine& smt, const char* s);
 
 int main() {
   Options opts;
-  opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
-  opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2);
+  opts.setInputLanguage(language::input::LANG_SMTLIB_V2);
+  opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
 
   cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
 
@@ -59,7 +58,8 @@ int main() {
 }
 
 void testGetInfo(SmtEngine& smt, const char* s) {
-  ParserBuilder pb(smt.getExprManager(), "<internal>", smt.getExprManager()->getOptions());
+  ParserBuilder pb(smt.getExprManager(), "<internal>",
+                   smt.getExprManager()->getOptions());
   Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
   assert(p != NULL);
   Command* c = p->nextCommand();
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index d162171d6..bea04a139 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -145,9 +145,10 @@ public:
   }
 
   class Foo {
-    int blah CVC4_UNUSED;
+    int d_bar;
   public:
-    Foo(int b) : blah(b) {}
+    Foo(int b) : d_bar(b) {}
+    int getBar() const { return d_bar; }
   };
 
   struct PtrAttributeId {};
@@ -175,6 +176,8 @@ public:
     TS_ASSERT(!node->getAttribute(cdattr, data2));
     node->setAttribute(cdattr, val);
     TS_ASSERT(node->getAttribute(cdattr, data3));
+    TS_ASSERT(data3 != NULL);
+    TS_ASSERT_EQUALS(63489, data3->getBar());
     TS_ASSERT_EQUALS(data3, val);
     delete node;
     delete val;
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index a83e53780..194aec0b1 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -22,7 +22,7 @@
 #include "base/exception.h"
 #include "expr/expr_manager.h"
 #include "expr/expr.h"
-#include "smt/smt_options_handler.h"
+#include "options/options.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -32,7 +32,6 @@ class ExprPublic : public CxxTest::TestSuite {
 private:
 
   Options opts;
-  smt::SmtOptionsHandler* d_handler;
 
   ExprManager* d_em;
 
@@ -55,12 +54,11 @@ public:
 
   void setUp() {
     try {
-      d_handler = new smt::SmtOptionsHandler(NULL);
 
       char *argv[2];
       argv[0] = strdup("");
       argv[1] = strdup("--output-language=ast");
-      opts.parseOptions(2, argv, d_handler);
+      opts.parseOptions(2, argv);
       free(argv[0]);
       free(argv[1]);
 
@@ -102,7 +100,6 @@ public:
       delete c_bool_and;
       delete b_bool;
       delete a_bool;
-      delete d_handler;
 
       delete d_em;
     } catch(Exception e) {
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 3a24057b2..7d6ee523a 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -25,7 +25,6 @@
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
 #include "expr/node.h"
-#include "smt/smt_options_handler.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -35,7 +34,6 @@ class NodeBlack : public CxxTest::TestSuite {
 private:
 
   Options opts;
-  smt::SmtOptionsHandler* d_handler;
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
   TypeNode* d_booleanType;
@@ -44,13 +42,10 @@ private:
 public:
 
   void setUp() {
-#warning "TODO: Discuss the effects of this change with Clark."
-    d_handler = new smt::SmtOptionsHandler(NULL);
-
     char *argv[2];
     argv[0] = strdup("");
     argv[1] = strdup("--output-language=ast");
-    opts.parseOptions(2, argv, d_handler);
+    opts.parseOptions(2, argv);
     free(argv[0]);
     free(argv[1]);
 
@@ -64,7 +59,6 @@ public:
     delete d_booleanType;
     delete d_scope;
     delete d_nodeManager;
-    delete d_handler;
   }
 
   bool imp(bool a, bool b) const {
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 0736ec052..f76a1e4d3 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -160,7 +160,7 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     d_satSolver = new FakeSatSolver();
     d_cnfStream = new CVC4::prop::TseitinCnfStream(
         d_satSolver, new theory::TheoryRegistrar(d_theoryEngine),
-        new context::Context(), d_smt->globals());
+        new context::Context(), d_smt->channels());
   }
 
   void tearDown() {
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 4313a9b64..49231071b 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -115,7 +115,7 @@ public:
     d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL;
 
     d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL),
-                              d_logicInfo, d_smt->globals());
+                              d_logicInfo);
 
     preregistered = new std::set<Node>();
 
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 62ed96900..e72b2cf4d 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -123,8 +123,8 @@ class FakeTheory : public Theory {
   // static std::deque<RewriteItem> s_expected;
 
 public:
-  FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) :
-      Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, globals)
+  FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+      Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
   { }
 
   /** Register an expected rewrite call */
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index daa98855a..9a0cbeea4 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -126,8 +126,8 @@ public:
   vector<Node> d_getSequence;
 
   DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out,
-              Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals)
-      : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, globals)
+              Valuation valuation, const LogicInfo& logicInfo)
+      : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo)
   {}
 
   void registerTerm(TNode n) {
@@ -204,7 +204,7 @@ public:
     d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL;
 
     d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL),
-                              *d_logicInfo, d_smt->globals());
+                              *d_logicInfo);
     d_outputChannel.clear();
     atom0 = d_nm->mkConst(true);
     atom1 = d_nm->mkConst(false);
diff --git a/test/unit/util/configuration_black.h b/test/unit/util/configuration_black.h
index 2d7378a67..f07763595 100644
--- a/test/unit/util/configuration_black.h
+++ b/test/unit/util/configuration_black.h
@@ -16,7 +16,7 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include "util/configuration.h"
+#include "base/configuration.h"
 
 using namespace CVC4;
 using namespace std;
diff --git a/test/unit/util/listener_black.h b/test/unit/util/listener_black.h
index cd3a08d4e..682a7c67b 100644
--- a/test/unit/util/listener_black.h
+++ b/test/unit/util/listener_black.h
@@ -64,7 +64,7 @@ public:
     ListenerCollection collection;
     std::string expected[1] = {"a"};
     {
-      RegisterListener a(&collection, new EventListener(d_events, "a"));
+      ListenerCollection::Registration a(&collection, new EventListener(d_events, "a"));
       collection.notify();
       TS_ASSERT(not collection.empty());
     }
@@ -77,7 +77,7 @@ public:
     // registering a single event.
     ListenerCollection* collection = new ListenerCollection;
     {
-      RegisterListener a(collection, new EventListener(d_events, "a"));
+      ListenerCollection::Registration a(collection, new EventListener(d_events, "a"));
       TS_ASSERT(not collection->empty());
       // The destructor for a now runs.
     }
@@ -88,11 +88,11 @@ public:
   void testMultipleCollection() {
     ListenerCollection* collection = new ListenerCollection;
     {
-      RegisterListener c(collection, new EventListener(d_events, "c"));
+      ListenerCollection::Registration c(collection, new EventListener(d_events, "c"));
       collection->notify();
       // d_events == {"c"}
-      RegisterListener b(collection, new EventListener(d_events, "b"));
-      RegisterListener a(collection, new EventListener(d_events, "a"));
+      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());
@@ -107,10 +107,10 @@ public:
     // registering several events.
     ListenerCollection* collection = new ListenerCollection;
     {
-      RegisterListener a(collection, new EventListener(d_events, "a"));
-      RegisterListener* b =
-          new RegisterListener(collection, new EventListener(d_events, "b"));
-      RegisterListener c(collection, new EventListener(d_events, "c"));
+      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;
@@ -128,17 +128,17 @@ public:
     // This tests adds and notify multiple times.
     ListenerCollection collection;
 
-    std::vector<RegisterListener*> listeners;
+    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 RegisterListener(&collection, listener));
+      listeners.push_back(new ListenerCollection::Registration(&collection, listener));
       collection.notify();
     }
 
     TS_ASSERT(not collection.empty());
     for(int i=0; i < listeners.size(); ++i){
-      RegisterListener* at_i = listeners[i];
+      ListenerCollection::Registration* at_i = listeners[i];
       delete at_i;
     }
     listeners.clear();
diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
index 87423f026..369f5b673 100644
--- a/test/unit/util/output_black.h
+++ b/test/unit/util/output_black.h
@@ -36,12 +36,12 @@ class OutputBlack : public CxxTest::TestSuite {
 public:
 
   void setUp() {
-    DebugChannel.setStream(d_debugStream);
-    TraceChannel.setStream(d_traceStream);
-    NoticeChannel.setStream(d_noticeStream);
-    ChatChannel.setStream(d_chatStream);
-    MessageChannel.setStream(d_messageStream);
-    WarningChannel.setStream(d_warningStream);
+    DebugChannel.setStream(&d_debugStream);
+    TraceChannel.setStream(&d_traceStream);
+    NoticeChannel.setStream(&d_noticeStream);
+    ChatChannel.setStream(&d_chatStream);
+    MessageChannel.setStream(&d_messageStream);
+    WarningChannel.setStream(&d_warningStream);
 
     d_debugStream.str("");
     d_traceStream.str("");