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

5 files changed, 16 insertions, 19 deletions

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 66eea0997..9c6c4af9b 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -26,7 +26,6 @@
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "prop/sat_solver.h"
-#include "smt/smt_globals.h"
 #include "theory/theory_registrar.h"
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 2e4f06c38..dd561667c 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -43,16 +43,13 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   d_bitblastingRegistrar = new BitblastingRegistrar(this);
   d_nullContext = new context::Context();
 
-  d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext,
-                                                      smtStatisticsRegistry(),
-                                                      "EagerBitblaster");
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
-                                           d_bitblastingRegistrar,
-                                           d_nullContext,
-                                           d_bv->globals(),
-                                           options::proof(),
-                                           "EagerBitblaster");
-  
+  d_satSolver = prop::SatSolverFactory::createMinisat(
+      d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
+
+  d_cnfStream = new prop::TseitinCnfStream(
+      d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(),
+      "EagerBitblaster");
+
   MinisatEmptyNotify* notify = new MinisatEmptyNotify();
   d_satSolver->setNotify(notify);
   d_bvp = NULL;
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 9268e2152..ca21e98c4 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -56,13 +56,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
                                            d_nullRegistrar,
                                            d_nullContext,
-                                           d_bv->globals(),
                                            options::proof(),
                                            "LazyBitblaster");
 
   d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
-    (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this);
+    (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv,
+                                                            this);
 
   d_satSolver->setNotify(d_satSolverNotify);
 }
@@ -526,11 +526,12 @@ void TLazyBitblaster::clearSolver() {
   d_satSolver = prop::SatSolverFactory::createMinisat(
       d_ctx, smtStatisticsRegistry());
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
-                                           d_nullContext, d_bv->globals());
+                                           d_nullContext);
 
   d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
-    (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this);
+    (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv,
+                                                            this);
   d_satSolver->setNotify(d_satSolverNotify);
 }
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 8f7e975cd..191f70638 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -44,8 +44,8 @@ namespace bv {
 
 TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
                    OutputChannel& out, Valuation valuation,
-                   const LogicInfo& logicInfo, SmtGlobals* globals)
-    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, globals),
+                   const LogicInfo& logicInfo)
+    : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
       d_context(c),
       d_alreadyPropagatedSet(c),
       d_sharedTermsSet(c),
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 27138abfc..1da15abf8 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -22,7 +22,6 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/context.h"
-#include "smt/smt_globals.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
@@ -56,7 +55,8 @@ class TheoryBV : public Theory {
 
 public:
 
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals);
+  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
+           Valuation valuation, const LogicInfo& logicInfo);
 
   ~TheoryBV();