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

34 files changed, 181 insertions, 146 deletions

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 877546da8..2c8fa9bcd 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -75,25 +75,22 @@
 #ifndef __CVC4__THEORY__ARITH__CONSTRAINT_H
 #define __CVC4__THEORY__ARITH__CONSTRAINT_H
 
-#include "expr/node.h"
-#include "proof/proof.h"
+#include <ext/hash_map>
+#include <list>
+#include <set>
+#include <vector>
 
-#include "context/context.h"
+#include "base/configuration_private.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
-
+#include "context/context.h"
+#include "expr/node.h"
+#include "proof/proof.h"
 #include "theory/arith/arithvar.h"
-#include "theory/arith/delta_rational.h"
+#include "theory/arith/callbacks.h"
 #include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint_forward.h"
-#include "theory/arith/callbacks.h"
-
-#include "util/configuration_private.h"
-
-#include <vector>
-#include <list>
-#include <set>
-#include <ext/hash_map>
+#include "theory/arith/delta_rational.h"
 
 namespace CVC4 {
 namespace theory {
@@ -107,7 +104,7 @@ namespace theory {
 namespace arith {
 
 /**
- * Logs the types of different proofs. 
+ * Logs the types of different proofs.
  * Current, proof types:
  * - NoAP             : This constraint is not known to be true.
  * - AssumeAP         : This is an input assertion. There is no proof.
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 054ab01e7..82d45871f 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -234,7 +234,7 @@ std::ostream& operator<<(std::ostream& os, const NodeLog& nl);
 class ApproximateSimplex;
 class TreeLog {
 private:
-  ApproximateSimplex* d_generator CVC4_UNUSED;
+  ApproximateSimplex* d_generator;
 
   int next_exec_ord;
   typedef std::map<int, NodeLog> ToNodeMap;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 843feed01..3c7a767c6 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -31,8 +31,8 @@ namespace arith {
 
 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
                          OutputChannel& out, Valuation valuation,
-                         const LogicInfo& logicInfo, SmtGlobals* globals)
-    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals)
+                         const LogicInfo& logicInfo)
+    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
     , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
     , d_ppRewriteTimer("theory::arith::ppRewriteTimer")
 {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index c54414109..b69d51966 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -47,8 +47,7 @@ private:
 
 public:
   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
-              Valuation valuation, const LogicInfo& logicInfo,
-              SmtGlobals* globals);
+              Valuation valuation, const LogicInfo& logicInfo);
   virtual ~TheoryArith();
 
   /**
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index cbcccd734..f9e036aa3 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -55,9 +55,8 @@ const bool d_solveWrite2 = false;
 
 TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
                            OutputChannel& out, Valuation valuation,
-                           const LogicInfo& logicInfo, SmtGlobals* globals,
-                           std::string name)
-  : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals, name),
+                           const LogicInfo& logicInfo, std::string name)
+    : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, name),
       d_numRow(name + "theory::arrays::number of Row lemmas", 0),
       d_numExt(name + "theory::arrays::number of Ext lemmas", 0),
       d_numProp(name + "theory::arrays::number of propagations", 0),
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 88d83bfb9..eba6c000e 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -93,7 +93,7 @@ class TheoryArrays : public Theory {
   // MISC
   /////////////////////////////////////////////////////////////////////////////
 
-  private:
+ private:
 
   /** True node for predicates = true */
   Node d_true;
@@ -124,11 +124,11 @@ class TheoryArrays : public Theory {
   /** conflicts in setModelVal */
   IntStat d_numSetModelValConflicts;
 
-  public:
+ public:
 
   TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
                Valuation valuation, const LogicInfo& logicInfo,
-               SmtGlobals* globals, std::string name = ""); 
+               std::string instanceName = "");
   ~TheoryArrays();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
@@ -139,7 +139,7 @@ class TheoryArrays : public Theory {
   // PREPROCESSING
   /////////////////////////////////////////////////////////////////////////////
 
-  private:
+ private:
 
   // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used
   class PPNotifyClass {
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 246f1e7e8..dc42fc281 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -29,9 +29,8 @@ namespace booleans {
 class TheoryBool : public Theory {
 public:
   TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out,
-             Valuation valuation, const LogicInfo& logicInfo,
-             SmtGlobals* globals)
-      : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, globals)
+             Valuation valuation, const LogicInfo& logicInfo)
+      : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
   {}
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 2fbc0e402..facc10c67 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -29,8 +29,8 @@ class TheoryBuiltin : public Theory {
 public:
   TheoryBuiltin(context::Context* c, context::UserContext* u,
                 OutputChannel& out, Valuation valuation,
-                const LogicInfo& logicInfo, SmtGlobals* globals)
-      : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, globals) {}
+                const LogicInfo& logicInfo)
+      : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {}
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */
 
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();
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index d49974df2..e33b4d05c 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -40,10 +40,8 @@ namespace theory {
 namespace datatypes {
 
 TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
-                                 Valuation valuation,
-                                 const LogicInfo& logicInfo,
-                                 SmtGlobals* globals)
-    : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, globals),
+                                 Valuation valuation, const LogicInfo& logicInfo)
+    : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
       //d_cycle_check(c),
       d_hasSeenCycle(c, false),
       d_infer(c),
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 212b9d7cf..82306b863 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -215,7 +215,7 @@ protected:
 public:
   TheoryDatatypes(context::Context* c, context::UserContext* u,
                   OutputChannel& out, Valuation valuation,
-                  const LogicInfo& logicInfo, SmtGlobals* globals);
+                  const LogicInfo& logicInfo);
   ~TheoryDatatypes();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 9a8d77844..18bf993ad 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -7,44 +7,52 @@ namespace theory {
 namespace fp {
 
 namespace removeToFPGeneric {
-  
+
   Node removeToFPGeneric (TNode node) {
     Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
-    
-    FloatingPointToFPGeneric info = node.getOperator().getConst<FloatingPointToFPGeneric>();
-    
+
+    FloatingPointToFPGeneric info =
+        node.getOperator().getConst<FloatingPointToFPGeneric>();
+
     size_t children = node.getNumChildren();
-    
+
     Node op;
-    
+
     if (children == 1) {
-      op = NodeManager::currentNM()->mkConst(FloatingPointToFPIEEEBitVector(info.t.exponent(),
-									    info.t.significand()));
+      op = NodeManager::currentNM()->mkConst(
+          FloatingPointToFPIEEEBitVector(info.t.exponent(),
+                                         info.t.significand()));
       return NodeManager::currentNM()->mkNode(op, node[0]);
-      
+
     } else {
       Assert(children == 2);
       Assert(node[0].getType().isRoundingMode());
-      
+
       TypeNode t = node[1].getType();
-      
+
       if (t.isFloatingPoint()) {
-	op = NodeManager::currentNM()->mkConst(FloatingPointToFPFloatingPoint(info.t.exponent(),
-									      info.t.significand()));
+	op = NodeManager::currentNM()->mkConst(
+            FloatingPointToFPFloatingPoint(info.t.exponent(),
+                                           info.t.significand()));
       } else if (t.isReal()) {
-	op = NodeManager::currentNM()->mkConst(FloatingPointToFPReal(info.t.exponent(),
-								     info.t.significand()));
+	op = NodeManager::currentNM()->mkConst(
+            FloatingPointToFPReal(info.t.exponent(),
+                                  info.t.significand()));
       } else if (t.isBitVector()) {
-	op = NodeManager::currentNM()->mkConst(FloatingPointToFPSignedBitVector(info.t.exponent(),
-										info.t.significand()));
-	
+	op = NodeManager::currentNM()->mkConst(
+            FloatingPointToFPSignedBitVector(info.t.exponent(),
+                                             info.t.significand()));
+
       } else {
-	throw TypeCheckingExceptionPrivate(node, "cannot rewrite to_fp generic due to incorrect type of second argument");
+	throw TypeCheckingExceptionPrivate(
+            node,
+            "cannot rewrite to_fp generic due to incorrect type of second "
+            "argument");
       }
-      
+
       return NodeManager::currentNM()->mkNode(op, node[0], node[1]);
     }
-    
+
     Unreachable("to_fp generic not rewritten");
   }
 }
@@ -53,8 +61,8 @@ namespace removeToFPGeneric {
 /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
 TheoryFp::TheoryFp(context::Context* c, context::UserContext* u,
                    OutputChannel& out, Valuation valuation,
-                   const LogicInfo& logicInfo, SmtGlobals* globals)
-    : Theory(THEORY_FP, c, u, out, valuation, logicInfo, globals)
+                   const LogicInfo& logicInfo)
+    : Theory(THEORY_FP, c, u, out, valuation, logicInfo)
 {}/* TheoryFp::TheoryFp() */
 
 
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index fe3c377af..ac2c68ac4 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -17,8 +17,7 @@ public:
            context::UserContext* u,
            OutputChannel& out,
            Valuation valuation,
-           const LogicInfo& logicInfo,
-           SmtGlobals* globals);
+           const LogicInfo& logicInfo);
 
   Node expandDefinition(LogicRequest &, Node node);
 
diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index 8cba51c8f..815f5e76a 100644
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -32,8 +32,8 @@ namespace idl {
 
 TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u,
                      OutputChannel& out, Valuation valuation,
-                     const LogicInfo& logicInfo, SmtGlobals* globals)
-    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals)
+                     const LogicInfo& logicInfo)
+    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
     , d_model(c)
     , d_assertionsDB(c)
 {}
diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
index aa7267eb7..7c879e722 100644
--- a/src/theory/idl/theory_idl.h
+++ b/src/theory/idl/theory_idl.h
@@ -45,8 +45,7 @@ public:
 
   /** Theory constructor. */
   TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
-            Valuation valuation, const LogicInfo& logicInfo,
-            SmtGlobals* globals);
+            Valuation valuation, const LogicInfo& logicInfo);
 
   /** Pre-processing of input atoms */
   Node ppRewrite(TNode atom);
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 02eeefcaf..fb689609d 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -24,8 +24,6 @@
 #include "base/cvc4_assert.h"
 #include "expr/kind.h"
 
-#warning "TODO: Remove logic_info_forward.h"
-
 
 using namespace std;
 using namespace CVC4::theory;
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index 54b735114..6d7297c63 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -24,7 +24,6 @@
 #include <string>
 #include <vector>
 #include "expr/kind.h"
-#include "options/logic_info_forward.h"
 
 namespace CVC4 {
 
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index b6162ec38..9107eb72d 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -128,7 +128,7 @@ function alternate {
 "
 
   eval "alternate_for_$1=\"\${alternate_for_$1}
-      if(options::theoryAlternates()[\\\"$2\\\"]) {
+      if(engine->useTheoryAlternative(\\\"$2\\\")) {
         engine->addTheory< $3 >($1);
         return;
       }\""
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index b808f4cd5..86fc057ea 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -34,8 +34,8 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) :
-    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, globals),
+TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
   d_masterEqualityEngine(0)
 {
   d_numInstantiations = 0;
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 63f3379b8..6335349b1 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -53,7 +53,7 @@ private:
 public:
   TheoryQuantifiers(context::Context* c, context::UserContext* u,
                     OutputChannel& out, Valuation valuation,
-                    const LogicInfo& logicInfo, SmtGlobals* globals);
+                    const LogicInfo& logicInfo);
   ~TheoryQuantifiers();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 82ebb5bf8..1280ad58d 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -25,9 +25,8 @@ TheorySets::TheorySets(context::Context* c,
                        context::UserContext* u,
                        OutputChannel& out,
                        Valuation valuation,
-                       const LogicInfo& logicInfo,
-                       SmtGlobals* globals)
-    : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, globals),
+                       const LogicInfo& logicInfo)
+    : Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
       d_internal(new TheorySetsPrivate(*this, c, u))
 {}
 
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 7ff8abec6..bc39fcbbd 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -41,8 +41,7 @@ public:
    * contexts.
    */
   TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out,
-             Valuation valuation, const LogicInfo& logicInfo,
-             SmtGlobals* globals);
+             Valuation valuation, const LogicInfo& logicInfo);
 
   ~TheorySets();
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 07a170a08..c0a892926 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -58,8 +58,8 @@ Node TheoryStrings::TermIndex::add( Node n, unsigned index, TheoryStrings* t, No
 
 TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
                              OutputChannel& out, Valuation valuation,
-                             const LogicInfo& logicInfo, SmtGlobals* globals)
-    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, globals),
+                             const LogicInfo& logicInfo)
+    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
       RMAXINT(LONG_MAX),
       d_notify( *this ),
       d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true),
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index ddb800ee1..fef2983fd 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -54,7 +54,7 @@ class TheoryStrings : public Theory {
 public:
   TheoryStrings(context::Context* c, context::UserContext* u,
                 OutputChannel& out, Valuation valuation,
-                const LogicInfo& logicInfo, SmtGlobals* globals);
+                const LogicInfo& logicInfo);
   ~TheoryStrings();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 45c9b1936..ee5efc8db 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -17,6 +17,9 @@
 #include "theory/theory.h"
 
 #include <vector>
+#include <sstream>
+#include <iostream>
+#include <string>
 
 #include "base/cvc4_assert.h"
 #include "smt/smt_statistics_registry.h"
@@ -48,9 +51,11 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){
   return os;
 }/* ostream& operator<<(ostream&, Theory::Effort) */
 
-Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
-               OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
-               SmtGlobals* globals, std::string name) throw()
+
+Theory::Theory(TheoryId id, context::Context* satContext,
+               context::UserContext* userContext, OutputChannel& out,
+               Valuation valuation, const LogicInfo& logicInfo,
+               std::string name) throw()
     : d_id(id)
     , d_instanceName(name)
     , d_satContext(satContext)
@@ -67,7 +72,6 @@ Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext*
     , d_out(&out)
     , d_valuation(valuation)
     , d_proofsEnabled(false)
-    , d_globals(globals)
 {
   smtStatisticsRegistry()->registerStat(&d_checkTime);
   smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
@@ -204,7 +208,8 @@ void Theory::debugPrintFacts() const{
 
 std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
   std::hash_set<TNode, TNodeHashFunction> currentlyShared;
-  for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){
+  for (shared_terms_iterator i = shared_terms_begin(),
+           i_end = shared_terms_end(); i != i_end; ++i) {
     currentlyShared.insert (*i);
   }
   return currentlyShared;
@@ -242,18 +247,21 @@ void Theory::computeRelevantTerms(set<Node>& termSet) const
 }
 
 
-Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstitutions)
+Theory::PPAssertStatus Theory::ppAssert(TNode in,
+                                        SubstitutionMap& outSubstitutions)
 {
   if (in.getKind() == kind::EQUAL) {
     // (and (= x t) phi) can be replaced by phi[x/t] if
     // 1) x is a variable
     // 2) x is not in the term t
     // 3) x : T and t : S, then S <: T
-    if (in[0].isVar() && !in[1].hasSubterm(in[0]) && (in[1].getType()).isSubtypeOf(in[0].getType()) ){
+    if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
+        (in[1].getType()).isSubtypeOf(in[0].getType()) ){
       outSubstitutions.addSubstitution(in[0], in[1]);
       return PP_ASSERT_STATUS_SOLVED;
     }
-    if (in[1].isVar() && !in[0].hasSubterm(in[1]) && (in[0].getType()).isSubtypeOf(in[1].getType())){
+    if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
+        (in[0].getType()).isSubtypeOf(in[1].getType())){
       outSubstitutions.addSubstitution(in[1], in[0]);
       return PP_ASSERT_STATUS_SOLVED;
     }
@@ -267,9 +275,10 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstituti
   return PP_ASSERT_STATUS_UNSOLVED;
 }
 
-std::pair<bool, Node> Theory::entailmentCheck(TNode lit,
-                                              const EntailmentCheckParameters* params,
-                                              EntailmentCheckSideEffects* out){
+std::pair<bool, Node> Theory::entailmentCheck(
+    TNode lit,
+    const EntailmentCheckParameters* params,
+    EntailmentCheckSideEffects* out) {
   return make_pair(false, Node::null());
 }
 
@@ -277,6 +286,12 @@ EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
   : d_tid(tid) {
 }
 
+std::string Theory::getFullInstanceName() const {
+  std::stringstream ss;
+  ss << "theory<" << d_id << ">" << d_instanceName;
+  return ss.str();
+}
+
 EntailmentCheckParameters::~EntailmentCheckParameters(){}
 
 TheoryId EntailmentCheckParameters::getTheoryId() const {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 2c3c66d8b..9849dd0b9 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -20,9 +20,8 @@
 #define __CVC4__THEORY__THEORY_H
 
 #include <ext/hash_set>
-#include <iostream>
+#include <iosfwd>
 #include <string>
-#include <strings.h>
 
 #include "context/cdlist.h"
 #include "context/cdo.h"
@@ -33,7 +32,6 @@
 #include "options/theory_options.h"
 #include "options/theoryof_mode.h"
 #include "smt/logic_request.h"
-#include "smt/smt_globals.h"
 #include "smt_util/command.h"
 #include "smt_util/dump.h"
 #include "theory/logic_info.h"
@@ -140,9 +138,9 @@ private:
   friend class ::CVC4::TheoryEngine;
 
   // Disallow default construction, copy, assignment.
-  Theory() CVC4_UNUSED;
-  Theory(const Theory&) CVC4_UNUSED;
-  Theory& operator=(const Theory&) CVC4_UNUSED;
+  Theory() CVC4_UNDEFINED;
+  Theory(const Theory&) CVC4_UNDEFINED;
+  Theory& operator=(const Theory&) CVC4_UNDEFINED;
 
   /**
    * An integer identifying the type of the theory
@@ -153,7 +151,7 @@ private:
    * an unique string identifier for each instance of a Theory class. We need
    * this to ensure unique statistics names over multiple theory instances. */
   std::string d_instanceName;
-  
+
   /**
    * The SAT search context for the Theory.
    */
@@ -243,10 +241,14 @@ protected:
 
   /**
    * Construct a Theory.
+   *
+   * The pair <id, instance> is assumed to uniquely identify this Theory
+   * w.r.t. the SmtEngine.
    */
-  Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
-         OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
-         SmtGlobals* globals, std::string name = "") throw(); // taking : No default.
+  Theory(TheoryId id, context::Context* satContext,
+         context::UserContext* userContext, OutputChannel& out,
+         Valuation valuation, const LogicInfo& logicInfo,
+         std::string instance = "") throw();  // taking : No default.
 
   /**
    * This is called at shutdown time by the TheoryEngine, just before
@@ -295,7 +297,11 @@ protected:
   void printFacts(std::ostream& os) const;
   void debugPrintFacts() const;
 
-  SmtGlobals* d_globals;
+  /**
+   * Whether proofs are enabled
+   *
+   */
+  bool d_proofEnabled;
 
 public:
 
@@ -415,13 +421,13 @@ public:
     return d_id;
   }
 
-  std::string getFullInstanceName() const {
-    std::stringstream ss;
-    ss << "theory<" << d_id << ">" << d_instanceName;
-    return ss.str();
-  }
+  /**
+   * Returns a string that uniquely identifies this theory solver w.r.t. the
+   * SmtEngine.
+   */
+  std::string getFullInstanceName() const;
+
 
-  
   /**
    * Get the SAT context associated to this Theory.
    */
@@ -865,9 +871,6 @@ public:
    * Turn on proof-production mode.
    */
   void produceProofs() { d_proofsEnabled = true; }
-  
-  /** Returns a pointer to the globals copy the theory is using. */
-  SmtGlobals* globals() { return d_globals; }
 
 };/* class Theory */
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index be2a89dbc..60716146e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -104,7 +104,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
                            RemoveITE& iteRemover,
                            const LogicInfo& logicInfo,
-                           SmtGlobals* globals)
+                           LemmaChannels* channels)
 : d_propEngine(NULL),
   d_decisionEngine(NULL),
   d_context(context),
@@ -133,16 +133,20 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_false(),
   d_interrupted(false),
   d_resourceManager(NodeManager::currentResourceManager()),
-  d_globals(globals),
+  d_channels(channels),
   d_inPreregister(false),
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms),
   d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)),
   d_bvToBoolPreprocessor(),
+  d_theoryAlternatives(),
+  d_attr_handle(),
   d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
 {
-  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
+  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
+      ++ theoryId)
+  {
     d_theoryTable[theoryId] = NULL;
     d_theoryOut[theoryId] = NULL;
   }
@@ -155,7 +159,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
-  PROOF (ProofManager::currentPM()->initTheoryProofEngine(d_globals); );
+  PROOF (ProofManager::currentPM()->initTheoryProofEngine(); );
 
   d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
 
@@ -1398,8 +1402,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // Share with other portfolio threads
-  if(d_globals->getLemmaOutputChannel() != NULL) {
-    d_globals->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
+  if(d_channels->getLemmaOutputChannel() != NULL) {
+    d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
   }
 
   // Run theory preprocessing, maybe
@@ -1769,6 +1773,18 @@ void TheoryEngine::spendResource(unsigned ammount) {
   d_resourceManager->spendResource(ammount);
 }
 
+void TheoryEngine::enableTheoryAlternative(const std::string& name){
+  Debug("TheoryEngine::enableTheoryAlternative")
+      << "TheoryEngine::enableTheoryAlternative(" << name << ")" << std::endl;
+
+  d_theoryAlternatives.insert(name);
+}
+
+bool TheoryEngine::useTheoryAlternative(const std::string& name) {
+  return d_theoryAlternatives.find(name) != d_theoryAlternatives.end();
+}
+
+
 TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
     conflicts(mkName("theory<", theory, ">::conflicts"), 0),
     propagations(mkName("theory<", theory, ">::propagations"), 0),
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0bf00c079..cdd05c096 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -20,6 +20,7 @@
 #define __CVC4__THEORY_ENGINE_H
 
 #include <deque>
+#include <set>
 #include <vector>
 #include <utility>
 
@@ -29,8 +30,8 @@
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "prop/prop_engine.h"
-#include "smt/smt_globals.h"
 #include "smt_util/command.h"
+#include "smt_util/lemma_channels.h"
 #include "theory/atom_requests.h"
 #include "theory/bv/bv_to_bool.h"
 #include "theory/interrupted.h"
@@ -467,14 +468,15 @@ class TheoryEngine {
   bool d_interrupted;
   ResourceManager* d_resourceManager;
 
-  /** Container for misc. globals. */
-  SmtGlobals* d_globals;
+  /** Container for lemma input and output channels. */
+  LemmaChannels* d_channels;
 
 public:
 
   /** Constructs a theory engine */
   TheoryEngine(context::Context* context, context::UserContext* userContext,
-               RemoveITE& iteRemover, const LogicInfo& logic, SmtGlobals* globals);
+               RemoveITE& iteRemover, const LogicInfo& logic,
+               LemmaChannels* channels);
 
   /** Destroys a theory engine */
   ~TheoryEngine();
@@ -495,7 +497,7 @@ public:
     d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
     d_theoryTable[theoryId] =
         new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId],
-                        theory::Valuation(this), d_logicInfo, d_globals);
+                        theory::Valuation(this), d_logicInfo);
   }
 
   inline void setPropEngine(prop::PropEngine* propEngine) {
@@ -832,7 +834,15 @@ public:
   /** Prints the assertions to the debug stream */
   void printAssertions(const char* tag);
 
+  /** Theory alternative is in use. */
+  bool useTheoryAlternative(const std::string& name);
+
+  /** Enables using a theory alternative by name. */
+  void enableTheoryAlternative(const std::string& name);
+
 private:
+  std::set< std::string > d_theoryAlternatives;
+
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
 public:
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 93a920f82..e58c11aca 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -36,18 +36,19 @@ namespace uf {
 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
 TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
                    OutputChannel& out, Valuation valuation,
-                   const LogicInfo& logicInfo, SmtGlobals* globals, std::string name)
-    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals, name),
+                   const LogicInfo& logicInfo, std::string instanceName)
+    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, instanceName),
       d_notify(*this),
       /* The strong theory solver can be notified by EqualityEngine::init(),
        * so make sure it's initialized first. */
       d_thss(NULL),
-      d_equalityEngine(d_notify, c, name + "theory::uf::TheoryUF", true),
+      d_equalityEngine(d_notify, c, instanceName + "theory::uf::TheoryUF",
+                       true),
       d_conflict(c, false),
       d_literalsToPropagate(c),
       d_literalsToPropagateIndex(c, 0),
       d_functionsTerms(c),
-      d_symb(u, name)
+      d_symb(u, instanceName)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index bd0016be7..e29b923f9 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -169,7 +169,7 @@ public:
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
   TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out,
            Valuation valuation, const LogicInfo& logicInfo,
-           SmtGlobals* globals, std::string name = "");
+           std::string instanceName = "");
 
   ~TheoryUF();