Remove staticrmStatic

53 files changed, 742 insertions, 386 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6943c5546..07150f794 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -30,13 +30,17 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
-                         OutputChannel& out, Valuation valuation,
+TheoryArith::TheoryArith(Environment* env,
+                         context::Context* c,
+                         context::UserContext* u,
+                         OutputChannel& out,
+                         Valuation valuation,
                          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")
-    , d_proofRecorder(nullptr)
+    : Theory(THEORY_ARITH, env, c, u, out, valuation, logicInfo),
+      d_internal(
+          new TheoryArithPrivate(env, *this, c, u, out, valuation, logicInfo)),
+      d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
+      d_proofRecorder(nullptr)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
   if (options::nlExt()) {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index b39ab961f..5bfb44d22 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -34,7 +34,7 @@ namespace arith {
  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  */
 class TheoryArith : public Theory {
-private:
+ private:
   friend class TheoryArithPrivate;
 
   TheoryArithPrivate* d_internal;
@@ -47,59 +47,63 @@ private:
   proof::ArithProofRecorder * d_proofRecorder;
 
 public:
-  TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
-              Valuation valuation, const LogicInfo& logicInfo);
-  virtual ~TheoryArith();
-
-  /**
-   * Does non-context dependent setup for a node connected to a theory.
-   */
-  void preRegisterTerm(TNode n) override;
-
-  Node expandDefinition(LogicRequest& logicRequest, Node node) override;
-
-  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
-
-  void check(Effort e) override;
-  bool needsCheckLastEffort() override;
-  void propagate(Effort e) override;
-  Node explain(TNode n) override;
-  bool getCurrentSubstitution(int effort,
-                              std::vector<Node>& vars,
-                              std::vector<Node>& subs,
-                              std::map<Node, std::vector<Node> >& exp) override;
-  bool isExtfReduced(int effort,
-                     Node n,
-                     Node on,
-                     std::vector<Node>& exp) override;
-
-  bool collectModelInfo(TheoryModel* m) override;
-
-  void shutdown() override {}
-
-  void presolve() override;
-  void notifyRestart() override;
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
-  Node ppRewrite(TNode atom) override;
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
-
-  std::string identify() const override { return std::string("TheoryArith"); }
-
-  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-
-  void addSharedTerm(TNode n) override;
-
-  Node getModelValue(TNode var) override;
-
-  std::pair<bool, Node> entailmentCheck(
-      TNode lit,
-      const EntailmentCheckParameters* params,
-      EntailmentCheckSideEffects* out) override;
-
-  void setProofRecorder(proof::ArithProofRecorder * proofRecorder)
-  {
-    d_proofRecorder = proofRecorder;
-  }
+ TheoryArith(Environment* env,
+             context::Context* c,
+             context::UserContext* u,
+             OutputChannel& out,
+             Valuation valuation,
+             const LogicInfo& logicInfo);
+ virtual ~TheoryArith();
+
+ /**
+  * Does non-context dependent setup for a node connected to a theory.
+  */
+ void preRegisterTerm(TNode n) override;
+
+ Node expandDefinition(LogicRequest& logicRequest, Node node) override;
+
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+
+ void check(Effort e) override;
+ bool needsCheckLastEffort() override;
+ void propagate(Effort e) override;
+ Node explain(TNode n) override;
+ bool getCurrentSubstitution(int effort,
+                             std::vector<Node>& vars,
+                             std::vector<Node>& subs,
+                             std::map<Node, std::vector<Node> >& exp) override;
+ bool isExtfReduced(int effort,
+                    Node n,
+                    Node on,
+                    std::vector<Node>& exp) override;
+
+ bool collectModelInfo(TheoryModel* m) override;
+
+ void shutdown() override {}
+
+ void presolve() override;
+ void notifyRestart() override;
+ PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+ Node ppRewrite(TNode atom) override;
+ void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+
+ std::string identify() const override { return std::string("TheoryArith"); }
+
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+
+ void addSharedTerm(TNode n) override;
+
+ Node getModelValue(TNode var) override;
+
+ std::pair<bool, Node> entailmentCheck(
+     TNode lit,
+     const EntailmentCheckParameters* params,
+     EntailmentCheckSideEffects* out) override;
+
+ void setProofRecorder(proof::ArithProofRecorder* proofRecorder)
+ {
+   d_proofRecorder = proofRecorder;
+ }
 
 };/* class TheoryArith */
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 62be1fcc1..6bcc14c94 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -81,13 +81,15 @@ namespace arith {
 static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum);
 static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap);
 
-TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
+TheoryArithPrivate::TheoryArithPrivate(Environment* env,
+                                       TheoryArith& containing,
                                        context::Context* c,
                                        context::UserContext* u,
                                        OutputChannel& out,
                                        Valuation valuation,
                                        const LogicInfo& logicInfo)
-    : d_containing(containing),
+    : d_env(env),
+      d_containing(containing),
       d_nlIncomplete(false),
       d_rowTracking(),
       d_constraintDatabase(
@@ -1173,7 +1175,8 @@ Node TheoryArithPrivate::getModelValue(TNode term) {
 }
 
 Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
-  if(Theory::theoryOf(n) != THEORY_ARITH) {
+  if (d_env->theoryOf(n) != THEORY_ARITH)
+  {
     return n;
   }
 
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 03cb81785..5e933ea49 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -17,9 +17,10 @@
 
 #pragma once
 
+#include <stdint.h>
+
 #include <map>
 #include <queue>
-#include <stdint.h>
 #include <vector>
 
 #include "context/cdhashset.h"
@@ -32,18 +33,16 @@
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "options/arith_options.h"
+#include "smt/environment.h"
 #include "smt/logic_exception.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/arith/arith_rewriter.h"
-#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/attempt_solution_simplex.h"
 #include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint.h"
-#include "theory/arith/constraint.h"
-#include "theory/arith/delta_rational.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/dio_solver.h"
 #include "theory/arith/dual_simplex.h"
@@ -51,10 +50,8 @@
 #include "theory/arith/infer_bounds.h"
 #include "theory/arith/linear_equality.h"
 #include "theory/arith/matrix.h"
-#include "theory/arith/matrix.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/partial_model.h"
 #include "theory/arith/simplex.h"
 #include "theory/arith/soi_simplex.h"
 #include "theory/arith/theory_arith.h"
@@ -91,10 +88,11 @@ class NonlinearExtension;
  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  */
 class TheoryArithPrivate {
-private:
-
+ private:
   static const uint32_t RESET_START = 2;
 
+  Environment* d_env;
+
   TheoryArith& d_containing;
 
   bool d_nlIncomplete;
@@ -423,47 +421,57 @@ private:
   Node ppRewriteTerms(TNode atom);
 
 public:
-  TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
-  ~TheoryArithPrivate();
-
-  /**
-   * Does non-context dependent setup for a node connected to a theory.
-   */
-  void preRegisterTerm(TNode n);
-  Node expandDefinition(LogicRequest &logicRequest, Node node);
-
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ TheoryArithPrivate(Environment* env,
+                    TheoryArith& containing,
+                    context::Context* c,
+                    context::UserContext* u,
+                    OutputChannel& out,
+                    Valuation valuation,
+                    const LogicInfo& logicInfo);
+ ~TheoryArithPrivate();
 
-  void check(Theory::Effort e);
-  bool needsCheckLastEffort();
-  void propagate(Theory::Effort e);
-  Node explain(TNode n);
-  bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
-  bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp );
+ /**
+  * Does non-context dependent setup for a node connected to a theory.
+  */
+ void preRegisterTerm(TNode n);
+ Node expandDefinition(LogicRequest& logicRequest, Node node);
 
-  Rational deltaValueForTotalOrder() const;
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
 
-  bool collectModelInfo(TheoryModel* m);
+ void check(Theory::Effort e);
+ bool needsCheckLastEffort();
+ void propagate(Theory::Effort e);
+ Node explain(TNode n);
+ bool getCurrentSubstitution(int effort,
+                             std::vector<Node>& vars,
+                             std::vector<Node>& subs,
+                             std::map<Node, std::vector<Node> >& exp);
+ bool isExtfReduced(int effort, Node n, Node on, std::vector<Node>& exp);
 
-  void shutdown(){ }
+ Rational deltaValueForTotalOrder() const;
 
-  void presolve();
-  void notifyRestart();
-  Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-  Node ppRewrite(TNode atom);
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
+ bool collectModelInfo(TheoryModel* m);
 
-  std::string identify() const { return std::string("TheoryArith"); }
+ void shutdown() {}
 
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
+ void presolve();
+ void notifyRestart();
+ Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ Node ppRewrite(TNode atom);
+ void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 
-  void addSharedTerm(TNode n);
+ std::string identify() const { return std::string("TheoryArith"); }
 
-  Node getModelValue(TNode var);
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+ void addSharedTerm(TNode n);
 
-  std::pair<bool, Node> entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out);
+ Node getModelValue(TNode var);
 
+ std::pair<bool, Node> entailmentCheck(
+     TNode lit,
+     const ArithEntailmentCheckParameters& params,
+     ArithEntailmentCheckSideEffects& out);
 
 private:
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f2beec0b8..67af54488 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -56,13 +56,14 @@ const bool d_solveWrite2 = false;
   //bool d_lazyRIntro1 = true;
   //bool d_eagerIndexSplitting = false;
 
-TheoryArrays::TheoryArrays(context::Context* c,
+TheoryArrays::TheoryArrays(Environment* env,
+                           context::Context* c,
                            context::UserContext* u,
                            OutputChannel& out,
                            Valuation valuation,
                            const LogicInfo& logicInfo,
                            std::string name)
-    : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, name),
+    : Theory(THEORY_ARRAYS, env, 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 3d6d0692e..e694dcf5e 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -138,9 +138,12 @@ class TheoryArrays : public Theory {
   unsigned d_reasonExt;
 
  public:
-
-  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
-               Valuation valuation, const LogicInfo& logicInfo,
+  TheoryArrays(Environment* env,
+               context::Context* c,
+               context::UserContext* u,
+               OutputChannel& out,
+               Valuation valuation,
+               const LogicInfo& logicInfo,
                std::string name = "");
   ~TheoryArrays();
 
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index abe024282..d400868bc 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -27,11 +27,16 @@ namespace theory {
 namespace booleans {
 
 class TheoryBool : public Theory {
-public:
-  TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out,
-             Valuation valuation, const LogicInfo& logicInfo)
-      : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
-  {}
+ public:
+  TheoryBool(Environment* env,
+             context::Context* c,
+             context::UserContext* u,
+             OutputChannel& out,
+             Valuation valuation,
+             const LogicInfo& logicInfo)
+      : Theory(THEORY_BOOL, env, c, u, out, valuation, logicInfo)
+  {
+  }
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 8a7d1bf7b..d11f3b246 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -26,11 +26,16 @@ namespace theory {
 namespace builtin {
 
 class TheoryBuiltin : public Theory {
-public:
-  TheoryBuiltin(context::Context* c, context::UserContext* u,
-                OutputChannel& out, Valuation valuation,
+ public:
+  TheoryBuiltin(Environment* env,
+                context::Context* c,
+                context::UserContext* u,
+                OutputChannel& out,
+                Valuation valuation,
                 const LogicInfo& logicInfo)
-      : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {}
+      : Theory(THEORY_BUILTIN, env, c, u, out, valuation, logicInfo)
+  {
+  }
   std::string identify() const override { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */
 
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index c2bc9e6e8..c86b6888d 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -135,8 +135,8 @@ Abc_Aig_t* AigBitblaster::currentAigM() {
   return (Abc_Aig_t*)(currentAigNtk()->pManFunc);
 }
 
-AigBitblaster::AigBitblaster()
-    : TBitblaster<Abc_Obj_t*>(),
+AigBitblaster::AigBitblaster(Environment* env)
+    : TBitblaster<Abc_Obj_t*>(env),
       d_nullContext(new context::Context()),
       d_aigCache(),
       d_bbAtoms(),
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 4e11c0f36..0d420e473 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -43,7 +43,7 @@ namespace bv {
 class AigBitblaster : public TBitblaster<Abc_Obj_t*>
 {
  public:
-  AigBitblaster();
+  AigBitblaster(Environment* env);
   ~AigBitblaster();
 
   void makeVariable(TNode node, Bits& bits) override;
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index df7cc4f11..9684d1248 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -27,12 +27,12 @@
 #include "proof/bitvector_proof.h"
 #include "prop/bv_sat_solver_notify.h"
 #include "prop/sat_solver_types.h"
+#include "smt/environment.h"
 #include "theory/bv/bitblast/bitblast_strategies_template.h"
 #include "theory/theory_registrar.h"
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
 
-
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -58,6 +58,8 @@ class TBitblaster
   typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster<T>*);
   typedef T (*AtomBBStrategy)(TNode, TBitblaster<T>*);
 
+  Environment* d_env;
+
   // caches and mappings
   TermDefMap d_termCache;
   ModelCache d_modelCache;
@@ -79,7 +81,7 @@ class TBitblaster
 
 
  public:
-  TBitblaster();
+  TBitblaster(Environment* env);
   virtual ~TBitblaster() {}
   virtual void bbAtom(TNode node) = 0;
   virtual void bbTerm(TNode node, Bits& bits) = 0;
@@ -181,8 +183,9 @@ void TBitblaster<T>::initTermBBStrategies()
 }
 
 template <class T>
-TBitblaster<T>::TBitblaster()
-    : d_termCache(),
+TBitblaster<T>::TBitblaster(Environment* env)
+    : d_env(env),
+      d_termCache(),
       d_modelCache(),
       d_nullContext(new context::Context()),
       d_cnfStream(),
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 9d43355cc..86696cfe4 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -29,8 +29,10 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
-    : TBitblaster<Node>(),
+EagerBitblaster::EagerBitblaster(Environment* env,
+                                 TheoryBV* theory_bv,
+                                 context::Context* c)
+    : TBitblaster<Node>(env),
       d_context(c),
       d_satSolver(),
       d_bitblastingRegistrar(new BitblastingRegistrar(this)),
@@ -63,12 +65,12 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
     default: Unreachable() << "Unknown SAT solver type";
   }
   d_satSolver.reset(solver);
-  d_cnfStream.reset(
-      new prop::TseitinCnfStream(d_satSolver.get(),
-                                 d_bitblastingRegistrar.get(),
-                                 d_nullContext.get(),
-                                 options::proof(),
-                                 "EagerBitblaster"));
+  d_cnfStream.reset(new prop::TseitinCnfStream(d_env,
+                                               d_satSolver.get(),
+                                               d_bitblastingRegistrar.get(),
+                                               d_nullContext.get(),
+                                               options::proof(),
+                                               "EagerBitblaster"));
 }
 
 EagerBitblaster::~EagerBitblaster() {}
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index d407b8131..cc97f14ee 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -38,7 +38,9 @@ class TheoryBV;
 class EagerBitblaster : public TBitblaster<Node>
 {
  public:
-  EagerBitblaster(TheoryBV* theory_bv, context::Context* context);
+  EagerBitblaster(Environment* env,
+                  TheoryBV* theory_bv,
+                  context::Context* context);
   ~EagerBitblaster();
 
   void addAtom(TNode atom);
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 2018590f7..afb0578be 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -58,11 +58,12 @@ uint64_t numNodes(TNode node, utils::NodeSet& seen)
 }
 }
 
-TLazyBitblaster::TLazyBitblaster(context::Context* c,
+TLazyBitblaster::TLazyBitblaster(Environment* env,
+                                 context::Context* c,
                                  bv::TheoryBV* bv,
                                  const std::string name,
                                  bool emptyNotify)
-    : TBitblaster<Node>(),
+    : TBitblaster<Node>(env),
       d_bv(bv),
       d_ctx(c),
       d_nullRegistrar(new prop::NullRegistrar()),
@@ -79,12 +80,12 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
   d_satSolver.reset(
       prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name));
 
-  d_cnfStream.reset(
-      new prop::TseitinCnfStream(d_satSolver.get(),
-                                 d_nullRegistrar.get(),
-                                 d_nullContext.get(),
-                                 options::proof(),
-                                 "LazyBitblaster"));
+  d_cnfStream.reset(new prop::TseitinCnfStream(d_env,
+                                               d_satSolver.get(),
+                                               d_nullRegistrar.get(),
+                                               d_nullContext.get(),
+                                               options::proof(),
+                                               "LazyBitblaster"));
 
   d_satSolverNotify.reset(
       d_emptyNotify
@@ -545,7 +546,7 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
     if (d_variables.find(var) == d_variables.end())
       continue;
 
-    Assert(Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
+    Assert(d_env->theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
     // only shared terms could not have been bit-blasted
     Assert(hasBBTerm(var) || isSharedTerm(var));
 
@@ -579,7 +580,7 @@ void TLazyBitblaster::clearSolver() {
   d_satSolver.reset(
       prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
   d_cnfStream.reset(new prop::TseitinCnfStream(
-      d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get()));
+      d_env, d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get()));
   d_satSolverNotify.reset(
       d_emptyNotify
           ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index ac5cd5c7f..d2a497bdd 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -45,7 +45,8 @@ class TLazyBitblaster : public TBitblaster<Node>
   void storeBBTerm(TNode node, const Bits& bits) override;
   bool hasBBAtom(TNode atom) const override;
 
-  TLazyBitblaster(context::Context* c,
+  TLazyBitblaster(Environment* env,
+                  context::Context* c,
                   TheoryBV* bv,
                   const std::string name = "",
                   bool emptyNotify = false);
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index dd0458a70..d725026cd 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -26,8 +26,11 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-EagerBitblastSolver::EagerBitblastSolver(context::Context* c, TheoryBV* bv)
-    : d_assertionSet(c),
+EagerBitblastSolver::EagerBitblastSolver(Environment* env,
+                                         context::Context* c,
+                                         TheoryBV* bv)
+    : d_env(env),
+      d_assertionSet(c),
       d_assumptionSet(c),
       d_context(c),
       d_bitblaster(),
@@ -49,12 +52,12 @@ void EagerBitblastSolver::initialize() {
   Assert(!isInitialized());
   if (d_useAig) {
 #ifdef CVC4_USE_ABC
-    d_aigBitblaster.reset(new AigBitblaster());
+    d_aigBitblaster.reset(new AigBitblaster(d_env));
 #else
     Unreachable();
 #endif
   } else {
-    d_bitblaster.reset(new EagerBitblaster(d_bv, d_context));
+    d_bitblaster.reset(new EagerBitblaster(d_env, d_bv, d_context));
     THEORY_PROOF(if (d_bvp) {
       d_bitblaster->setProofLog(d_bvp);
       d_bvp->setBitblaster(d_bitblaster.get());
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 8e42d5cab..1d7f2e0bd 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -24,6 +24,7 @@
 
 #include "expr/node.h"
 #include "proof/resolution_bitvector_proof.h"
+#include "smt/environment.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
 
@@ -39,7 +40,9 @@ class AigBitblaster;
  */
 class EagerBitblastSolver {
  public:
-  EagerBitblastSolver(context::Context* c, theory::bv::TheoryBV* bv);
+  EagerBitblastSolver(Environment* env,
+                      context::Context* c,
+                      theory::bv::TheoryBV* bv);
   ~EagerBitblastSolver();
   bool checkSat();
   void assertFormula(TNode formula);
@@ -51,6 +54,8 @@ class EagerBitblastSolver {
   void setProofLog(proof::BitVectorProof* bvp);
 
  private:
+  Environment* d_env;
+
   context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
   context::CDHashSet<Node, NodeHashFunction> d_assumptionSet;
   context::Context* d_context;
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index dbdeccfe5..8efda195e 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -26,11 +26,13 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-BVQuickCheck::BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv)
-  : d_ctx()
-  , d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true))
-  , d_conflict()
-  , d_inConflict(&d_ctx, false)
+BVQuickCheck::BVQuickCheck(Environment* env,
+                           const std::string& name,
+                           theory::bv::TheoryBV* bv)
+    : d_ctx(),
+      d_bitblaster(new TLazyBitblaster(env, &d_ctx, bv, name, true)),
+      d_conflict(),
+      d_inConflict(&d_ctx, false)
 {}
 
 
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 75f39b6e0..04ed0cd2c 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -19,12 +19,13 @@
 #ifndef CVC4__BV_QUICK_CHECK_H
 #define CVC4__BV_QUICK_CHECK_H
 
-#include <vector>
 #include <unordered_set>
+#include <vector>
 
 #include "context/cdo.h"
 #include "expr/node.h"
 #include "prop/sat_solver_types.h"
+#include "smt/environment.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 
@@ -45,34 +46,36 @@ class BVQuickCheck {
   context::CDO<bool> d_inConflict;
   void setConflict();
 
-public:
-  BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv);
+ public:
+  BVQuickCheck(Environment* env,
+               const std::string& name,
+               theory::bv::TheoryBV* bv);
   ~BVQuickCheck();
   bool inConflict();
   Node getConflict() { return d_conflict; }
-  /** 
+  /**
    * Checks the satisfiability for a given set of assumptions.
-   * 
+   *
    * @param assumptions literals assumed true
    * @param budget max number of conflicts
-   * 
-   * @return 
+   *
+   * @return
    */
   prop::SatValue checkSat(std::vector<Node>& assumptions, unsigned long budget);
-  /** 
+  /**
    * Checks the satisfiability of given assertions.
-   * 
+   *
    * @param budget max number of conflicts
-   * 
-   * @return 
+   *
+   * @return
    */
   prop::SatValue checkSat(unsigned long budget);
-  
-  /** 
+
+  /**
    * Convert to CNF and assert the given literal.
-   * 
+   *
    * @param assumption bv literal
-   * 
+   *
    * @return false if a conflict has been found via bcp.
    */
   bool addAssertion(TNode assumption);
@@ -80,31 +83,31 @@ public:
   void push();
   void pop();
   void popToZero();
-  /** 
+  /**
    * Deletes the SAT solver and CNF stream, but maintains the
-   * bit-blasting term cache. 
-   * 
+   * bit-blasting term cache.
+   *
    */
-  void clearSolver(); 
+  void clearSolver();
 
-  /** 
+  /**
    * Computes the size of the circuit required to bit-blast
-   * atom, by not recounting the nodes in seen. 
-   * 
-   * @param node 
-   * @param seen 
-   * 
-   * @return 
+   * atom, by not recounting the nodes in seen.
+   *
+   * @param node
+   * @param seen
+   *
+   * @return
    */
   uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
   bool collectModelInfo(theory::TheoryModel* model, bool fullModel);
 
-  typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
-  vars_iterator beginVars(); 
-  vars_iterator endVars(); 
-
-  Node getVarValue(TNode var, bool fullModel); 
+  typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator
+      vars_iterator;
+  vars_iterator beginVars();
+  vars_iterator endVars();
 
+  Node getVarValue(TNode var, bool fullModel);
 };
 
 
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 60660eda9..8dcc1835b 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -69,12 +69,15 @@ using AssertionQueue = context::CDQueue<Node>;
  */
 class SubtheorySolver {
  public:
-  SubtheorySolver(context::Context* c, TheoryBV* bv)
-      : d_context(c),
+  SubtheorySolver(Environment* env, context::Context* c, TheoryBV* bv)
+      : d_env(env),
+        d_context(c),
         d_bv(bv),
         d_bvp(nullptr),
         d_assertionQueue(c),
-        d_assertionIndex(c, 0) {}
+        d_assertionIndex(c, 0)
+  {
+  }
   virtual ~SubtheorySolver() {}
   virtual bool check(Theory::Effort e) = 0;
   virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
@@ -102,6 +105,8 @@ class SubtheorySolver {
   }
 
  protected:
+  Environment* d_env;
+
   /** The context we are using */
   context::Context* d_context;
 
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 6f8804042..bfedced51 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -227,10 +227,12 @@ void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) {
   d_cache[from] = SubstitutionElement(to, reason);
 }
 
-AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
-    : SubtheorySolver(c, bv),
+AlgebraicSolver::AlgebraicSolver(Environment* env,
+                                 context::Context* c,
+                                 TheoryBV* bv)
+    : SubtheorySolver(env, c, bv),
       d_modelMap(),
-      d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv)),
+      d_quickSolver(new BVQuickCheck(env, "theory::bv::algebraic", bv)),
       d_isComplete(c, false),
       d_isDifficult(c, false),
       d_budget(options::bitvectorAlgebraicBudget()),
@@ -723,9 +725,10 @@ bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
   std::vector<Node> values;
   for (set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
     TNode term = *it;
-    if (term.getType().isBitVector() &&
-        (term.getMetaKind() == kind::metakind::VARIABLE ||
-         Theory::theoryOf(term) != THEORY_BV)) {
+    if (term.getType().isBitVector()
+        && (term.getMetaKind() == kind::metakind::VARIABLE
+            || d_env->theoryOf(term) != THEORY_BV))
+    {
       variables.push_back(term);
       values.push_back(term);
     }
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index de75ad859..8baa208c1 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -220,8 +220,8 @@ class AlgebraicSolver : public SubtheorySolver {
    */
   bool quickCheck(std::vector<Node>& facts);
 
-public:
-  AlgebraicSolver(context::Context* c, TheoryBV* bv);
+ public:
+  AlgebraicSolver(Environment* env, context::Context* c, TheoryBV* bv);
   ~AlgebraicSolver();
 
   void preRegister(TNode node) override {}
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 94dfdee14..25a45236b 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -33,9 +33,11 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
-    : SubtheorySolver(c, bv),
-      d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
+BitblastSolver::BitblastSolver(Environment* env,
+                               context::Context* c,
+                               TheoryBV* bv)
+    : SubtheorySolver(env, c, bv),
+      d_bitblaster(new TLazyBitblaster(env, c, bv, "theory::bv::lazy")),
       d_bitblastQueue(c),
       d_statistics(),
       d_validModelCache(c, true),
@@ -47,7 +49,7 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
 {
   if (options::bitvectorQuickXplain())
   {
-    d_quickCheck.reset(new BVQuickCheck("bb", bv));
+    d_quickCheck.reset(new BVQuickCheck(env, "bb", bv));
     d_quickXplain.reset(new QuickXPlain("bb", d_quickCheck.get()));
   }
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 0b0a9521b..50cd1cb5d 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -65,8 +65,9 @@ class BitblastSolver : public SubtheorySolver {
   std::unique_ptr<QuickXPlain> d_quickXplain;
   //  Node getModelValueRec(TNode node);
   void setConflict(TNode conflict);
-public:
-  BitblastSolver(context::Context* c, TheoryBV* bv);
+
+ public:
+  BitblastSolver(Environment* env, context::Context* c, TheoryBV* bv);
   ~BitblastSolver();
 
   void preRegister(TNode node) override;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index bf9bfa480..bc796e7ab 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -32,17 +32,17 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 using namespace CVC4::theory::bv::utils;
 
-CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
-  : SubtheorySolver(c, bv),
-    d_notify(*this),
-    d_equalityEngine(d_notify, c, "theory::bv::ee", true),
-    d_slicer(new Slicer()),
-    d_isComplete(c, true),
-    d_lemmaThreshold(16),
-    d_useSlicer(false),
-    d_preregisterCalled(false),
-    d_checkCalled(false),
-    d_reasons(c)
+CoreSolver::CoreSolver(Environment* env, context::Context* c, TheoryBV* bv)
+    : SubtheorySolver(env, c, bv),
+      d_notify(*this),
+      d_equalityEngine(d_notify, c, "theory::bv::ee", true),
+      d_slicer(new Slicer()),
+      d_isComplete(c, true),
+      d_lemmaThreshold(16),
+      d_useSlicer(false),
+      d_preregisterCalled(false),
+      d_checkCalled(false),
+      d_reasons(c)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
@@ -417,10 +417,9 @@ void CoreSolver::eqNotifyNewClass(TNode t) {
 }
 
 bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
-  if (d_useSlicer)
-    return utils::isCoreTerm(term, seen);
-  
-  return utils::isEqualityTerm(term, seen); 
+  if (d_useSlicer) return utils::isCoreTerm(d_env, term, seen);
+
+  return utils::isEqualityTerm(d_env, term, seen);
 }
 
 bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index e2026d4a5..b70518ab4 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -100,11 +100,12 @@ class CoreSolver : public SubtheorySolver {
   Node getBaseDecomposition(TNode a);
   bool isCompleteForTerm(TNode term, TNodeBoolMap& seen);
   Statistics d_statistics;
-public:
-  CoreSolver(context::Context* c, TheoryBV* bv);
+
+ public:
+  CoreSolver(Environment* env, context::Context* c, TheoryBV* bv);
   ~CoreSolver();
   bool isComplete() override { return d_isComplete; }
-  void  setMasterEqualityEngine(eq::EqualityEngine* eq);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
   void preRegister(TNode node) override;
   bool check(Theory::Effort e) override;
   void explain(TNode literal, std::vector<TNode>& assumptions) override;
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index e18c886df..f114b890e 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -23,6 +23,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/attribute.h"
+#include "smt/environment.h"
 #include "theory/bv/bv_inequality_graph.h"
 #include "theory/bv/bv_subtheory.h"
 
@@ -57,16 +58,21 @@ class InequalitySolver : public SubtheorySolver
   bool isInequalityOnly(TNode node);
   bool addInequality(TNode a, TNode b, bool strict, TNode fact);
   Statistics d_statistics;
-public:
-  InequalitySolver(context::Context* c, context::Context* u, TheoryBV* bv)
-    : SubtheorySolver(c, bv),
-      d_assertionSet(c),
-      d_inequalityGraph(c, u),
-      d_explanations(c),
-      d_isComplete(c, true),
-      d_ineqTerms(),
-      d_statistics()
-  {}
+
+ public:
+  InequalitySolver(Environment* env,
+                   context::Context* c,
+                   context::Context* u,
+                   TheoryBV* bv)
+      : SubtheorySolver(env, c, bv),
+        d_assertionSet(c),
+        d_inequalityGraph(c, u),
+        d_explanations(c),
+        d_isComplete(c, true),
+        d_ineqTerms(),
+        d_statistics()
+  {
+  }
 
   bool check(Theory::Effort e) override;
   void propagate(Theory::Effort e) override;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 23ffabcd1..aa1aab6a6 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -44,13 +44,14 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-TheoryBV::TheoryBV(context::Context* c,
+TheoryBV::TheoryBV(Environment* env,
+                   context::Context* c,
                    context::UserContext* u,
                    OutputChannel& out,
                    Valuation valuation,
                    const LogicInfo& logicInfo,
                    std::string name)
-    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
+    : Theory(THEORY_BV, env, c, u, out, valuation, logicInfo, name),
       d_context(c),
       d_alreadyPropagatedSet(c),
       d_sharedTermsSet(c),
@@ -78,29 +79,29 @@ TheoryBV::TheoryBV(context::Context* c,
   getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
   getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_eagerSolver.reset(new EagerBitblastSolver(c, this));
+    d_eagerSolver.reset(new EagerBitblastSolver(env, c, this));
     return;
   }
 
   if (options::bitvectorEqualitySolver() && !options::proof())
   {
-    d_subtheories.emplace_back(new CoreSolver(c, this));
+    d_subtheories.emplace_back(new CoreSolver(env, c, this));
     d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
   }
 
   if (options::bitvectorInequalitySolver() && !options::proof())
   {
-    d_subtheories.emplace_back(new InequalitySolver(c, u, this));
+    d_subtheories.emplace_back(new InequalitySolver(env, c, u, this));
     d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
   }
 
   if (options::bitvectorAlgebraicSolver() && !options::proof())
   {
-    d_subtheories.emplace_back(new AlgebraicSolver(c, this));
+    d_subtheories.emplace_back(new AlgebraicSolver(env, c, this));
     d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
   }
 
-  BitblastSolver* bb_solver = new BitblastSolver(c, this);
+  BitblastSolver* bb_solver = new BitblastSolver(env, c, this);
   if (options::bvAbstraction())
   {
     bb_solver->setAbstraction(d_abstractionModule.get());
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 7ca98f2ea..08325fc0e 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -64,10 +64,13 @@ class TheoryBV : public Theory {
   std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
   std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
 
-public:
-
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
-           Valuation valuation, const LogicInfo& logicInfo,
+ public:
+  TheoryBV(Environment* env,
+           context::Context* c,
+           context::UserContext* u,
+           OutputChannel& out,
+           Valuation valuation,
+           const LogicInfo& logicInfo,
            std::string name = "");
 
   ~TheoryBV();
@@ -97,7 +100,7 @@ public:
   bool getCurrentSubstitution(int effort,
                               std::vector<Node>& vars,
                               std::vector<Node>& subs,
-                              std::map<Node, std::vector<Node> >& exp) override;
+                              std::map<Node, std::vector<Node>>& exp) override;
   int getReduction(int effort, Node n, Node& nr) override;
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
@@ -110,14 +113,15 @@ public:
 
   void presolve() override;
 
-  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+  bool applyAbstraction(const std::vector<Node>& assertions,
+                        std::vector<Node>& new_assertions);
 
   void setProofLog(proof::BitVectorProof* bvp);
 
  private:
-
-  class Statistics {
-  public:
+  class Statistics
+  {
+   public:
     AverageStat d_avgConflictSize;
     IntStat     d_solveSubstitutions;
     TimerStat   d_solveTimer;
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index c0df9f35c..bd3f961e4 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -134,7 +134,10 @@ bool isBVPredicate(TNode node)
          || k == kind::BITVECTOR_REDAND;
 }
 
-static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
+static bool isCoreEqTerm(Environment* env,
+                         bool iseq,
+                         TNode term,
+                         TNodeBoolMap& cache)
 {
   TNode t = term.getKind() == kind::NOT ? term[0] : term;
 
@@ -156,8 +159,7 @@ static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
       continue;
     }
 
-    if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, n)
-        == theory::THEORY_BV)
+    if (env->theoryOf(theory::THEORY_OF_TERM_BASED, n) == theory::THEORY_BV)
     {
       Kind k = n.getKind();
       Assert(k != kind::CONST_BITVECTOR);
@@ -196,14 +198,14 @@ static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
   return cache[t];
 }
 
-bool isCoreTerm(TNode term, TNodeBoolMap& cache)
+bool isCoreTerm(Environment* env, TNode term, TNodeBoolMap& cache)
 {
-  return isCoreEqTerm(false, term, cache);
+  return isCoreEqTerm(env, false, term, cache);
 }
 
-bool isEqualityTerm(TNode term, TNodeBoolMap& cache)
+bool isEqualityTerm(Environment* env, TNode term, TNodeBoolMap& cache)
 {
-  return isCoreEqTerm(true, term, cache);
+  return isCoreEqTerm(env, true, term, cache);
 }
 
 bool isBitblastAtom(Node lit)
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 23eaab3f8..dfb6686d4 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -25,6 +25,7 @@
 #include <vector>
 
 #include "expr/node_manager.h"
+#include "smt/environment.h"
 
 namespace CVC4 {
 namespace theory {
@@ -76,11 +77,11 @@ bool isBVPredicate(TNode node);
  *   - not a THEORY_BV term
  *   - a THEORY_BV \Sigma_core term, where
  *     \Sigma_core = { concat, extract, =, bv constants, bv variables } */
-bool isCoreTerm(TNode term, TNodeBoolMap& cache);
+bool isCoreTerm(Environment* env, TNode term, TNodeBoolMap& cache);
 
 /* Returns true if given term is a THEORY_BV \Sigma_equality term.
  * \Sigma_equality = { =, bv constants, bv variables }  */
-bool isEqualityTerm(TNode term, TNodeBoolMap& cache);
+bool isEqualityTerm(Environment* env, TNode term, TNodeBoolMap& cache);
 
 /* Returns true if given node is an atom that is bit-blasted.  */
 bool isBitblastAtom(Node lit);
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 2d6aeae60..5961ab5de 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -39,12 +39,13 @@ namespace CVC4 {
 namespace theory {
 namespace datatypes {
 
-TheoryDatatypes::TheoryDatatypes(Context* c,
+TheoryDatatypes::TheoryDatatypes(Environment* env,
+                                 Context* c,
                                  UserContext* u,
                                  OutputChannel& out,
                                  Valuation valuation,
                                  const LogicInfo& logicInfo)
-    : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
+    : Theory(THEORY_DATATYPES, env, c, u, out, valuation, logicInfo),
       d_infer(c),
       d_infer_exp(c),
       d_term_sk(u),
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index ba09ce89e..c417a399a 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -26,6 +26,7 @@
 #include "expr/attribute.h"
 #include "expr/datatype.h"
 #include "expr/node_trie.h"
+#include "smt/environment.h"
 #include "theory/datatypes/sygus_extension.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -266,8 +267,11 @@ private:
   void computeCareGraph() override;
 
  public:
-  TheoryDatatypes(context::Context* c, context::UserContext* u,
-                  OutputChannel& out, Valuation valuation,
+  TheoryDatatypes(Environment* env,
+                  context::Context* c,
+                  context::UserContext* u,
+                  OutputChannel& out,
+                  Valuation valuation,
                   const LogicInfo& logicInfo);
   ~TheoryDatatypes();
 
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index fa143a1d0..cfc75d671 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -99,12 +99,13 @@ Node buildConjunct(const std::vector<TNode> &assumptions) {
 }  // namespace helper
 
 /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-TheoryFp::TheoryFp(context::Context *c,
-                   context::UserContext *u,
-                   OutputChannel &out,
+TheoryFp::TheoryFp(Environment* env,
+                   context::Context* c,
+                   context::UserContext* u,
+                   OutputChannel& out,
                    Valuation valuation,
-                   const LogicInfo &logicInfo)
-    : Theory(THEORY_FP, c, u, out, valuation, logicInfo),
+                   const LogicInfo& logicInfo)
+    : Theory(THEORY_FP, env, c, u, out, valuation, logicInfo),
       d_notification(*this),
       d_equalityEngine(d_notification, c, "theory::fp::ee", true),
       d_registeredTerms(u),
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index ad093f924..6aae5fbe2 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -35,8 +35,12 @@ namespace fp {
 class TheoryFp : public Theory {
  public:
   /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-  TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
-           Valuation valuation, const LogicInfo& logicInfo);
+  TheoryFp(Environment* env,
+           context::Context* c,
+           context::UserContext* u,
+           OutputChannel& out,
+           Valuation valuation,
+           const LogicInfo& logicInfo);
 
   Node expandDefinition(LogicRequest& lr, Node node) override;
 
diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index 12ac1e802..82056a6d4 100644
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -30,12 +30,15 @@ namespace CVC4 {
 namespace theory {
 namespace idl {
 
-TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u,
-                     OutputChannel& out, Valuation valuation,
+TheoryIdl::TheoryIdl(Environment* env,
+                     context::Context* c,
+                     context::UserContext* u,
+                     OutputChannel& out,
+                     Valuation valuation,
                      const LogicInfo& logicInfo)
-    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
-    , d_model(c)
-    , d_assertionsDB(c)
+    : Theory(THEORY_ARITH, env, c, u, out, valuation, logicInfo),
+      d_model(c),
+      d_assertionsDB(c)
 {}
 
 Node TheoryIdl::ppRewrite(TNode atom) {
diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
index 1d48d0785..851226942 100644
--- a/src/theory/idl/theory_idl.h
+++ b/src/theory/idl/theory_idl.h
@@ -41,11 +41,14 @@ class TheoryIdl : public Theory {
   /** Process a new assertion, returns false if in conflict */
   bool processAssertion(const IDLAssertion& assertion);
 
-public:
-
+ public:
   /** Theory constructor. */
-  TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
-            Valuation valuation, const LogicInfo& logicInfo);
+  TheoryIdl(Environment* env,
+            context::Context* c,
+            context::UserContext* u,
+            OutputChannel& out,
+            Valuation valuation,
+            const LogicInfo& logicInfo);
 
   /** Pre-processing of input atoms */
   Node ppRewrite(TNode atom) override;
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 1682b4d0c..512c903c9 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -34,8 +34,13 @@ 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) :
-    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo)
+TheoryQuantifiers::TheoryQuantifiers(Environment* env,
+                                     Context* c,
+                                     context::UserContext* u,
+                                     OutputChannel& out,
+                                     Valuation valuation,
+                                     const LogicInfo& logicInfo)
+    : Theory(THEORY_QUANTIFIERS, env, c, u, out, valuation, logicInfo)
 {
   out.handleUserAttribute( "axiom", this );
   out.handleUserAttribute( "conjecture", this );
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index b5b07f2e6..ea688af96 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -34,8 +34,11 @@ namespace quantifiers {
 
 class TheoryQuantifiers : public Theory {
  public:
-  TheoryQuantifiers(context::Context* c, context::UserContext* u,
-                    OutputChannel& out, Valuation valuation,
+  TheoryQuantifiers(Environment* env,
+                    context::Context* c,
+                    context::UserContext* u,
+                    OutputChannel& out,
+                    Valuation valuation,
                     const LogicInfo& logicInfo);
   ~TheoryQuantifiers();
 
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 1392f8fab..6a8b4771b 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -38,16 +38,21 @@ namespace CVC4 {
 namespace theory {
 namespace sep {
 
-TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
-  d_lemmas_produced_c(u),
-  d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::sep::ee", true),
-  d_conflict(c, false),
-  d_reduce(u),
-  d_infer(c),
-  d_infer_exp(c),
-  d_spatial_assertions(c)
+TheorySep::TheorySep(Environment* env,
+                     context::Context* c,
+                     context::UserContext* u,
+                     OutputChannel& out,
+                     Valuation valuation,
+                     const LogicInfo& logicInfo)
+    : Theory(THEORY_SEP, env, c, u, out, valuation, logicInfo),
+      d_lemmas_produced_c(u),
+      d_notify(*this),
+      d_equalityEngine(d_notify, c, "theory::sep::ee", true),
+      d_conflict(c, false),
+      d_reduce(u),
+      d_infer(c),
+      d_infer_exp(c),
+      d_spatial_assertions(c)
 {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index ae044f6d7..dd3658fce 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -63,7 +63,12 @@ class TheorySep : public Theory {
                         bool pol, bool hasPol, bool underSpatial );
 
  public:
-  TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheorySep(Environment* env,
+            context::Context* c,
+            context::UserContext* u,
+            OutputChannel& out,
+            Valuation valuation,
+            const LogicInfo& logicInfo);
   ~TheorySep();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 869cb8926..8e063219d 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -21,12 +21,13 @@ namespace CVC4 {
 namespace theory {
 namespace sets {
 
-TheorySets::TheorySets(context::Context* c,
+TheorySets::TheorySets(Environment* env,
+                       context::Context* c,
                        context::UserContext* u,
                        OutputChannel& out,
                        Valuation valuation,
                        const LogicInfo& logicInfo)
-    : Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
+    : Theory(THEORY_SETS, env, c, u, out, valuation, logicInfo),
       d_internal(new TheorySetsPrivate(*this, c, u))
 {
   // Do not move me to the header.
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 4c145aedb..7e5d23142 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -35,7 +35,8 @@ class TheorySets : public Theory
 {
  public:
   /** Constructs a new instance of TheorySets w.r.t. the provided contexts. */
-  TheorySets(context::Context* c,
+  TheorySets(Environment* env,
+             context::Context* c,
              context::UserContext* u,
              OutputChannel& out,
              Valuation valuation,
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9fad39b6b..13d91bd17 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -85,12 +85,13 @@ Node TheoryStrings::TermIndex::add(TNode n,
   }
 }
 
-TheoryStrings::TheoryStrings(context::Context* c,
+TheoryStrings::TheoryStrings(Environment* env,
+                             context::Context* c,
                              context::UserContext* u,
                              OutputChannel& out,
                              Valuation valuation,
                              const LogicInfo& logicInfo)
-    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
+    : Theory(THEORY_STRINGS, env, c, u, out, valuation, logicInfo),
       d_notify(*this),
       d_equalityEngine(d_notify, c, "theory::strings", true),
       d_state(c, d_equalityEngine, d_valuation),
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 8e2af8434..f016d9d72 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -97,8 +97,11 @@ class TheoryStrings : public Theory {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  TheoryStrings(context::Context* c, context::UserContext* u,
-                OutputChannel& out, Valuation valuation,
+  TheoryStrings(Environment* env,
+                context::Context* c,
+                context::UserContext* u,
+                OutputChannel& out,
+                Valuation valuation,
                 const LogicInfo& logicInfo);
   ~TheoryStrings();
 
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 3b11d8e54..3787ca8af 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -47,8 +47,8 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
     return true;
   }
 
-  TheoryId currentTheoryId = Theory::theoryOf(current);
-  TheoryId parentTheoryId = Theory::theoryOf(parent);
+  TheoryId currentTheoryId = d_engine->theoryIdOf(current);
+  TheoryId parentTheoryId = d_engine->theoryIdOf(parent);
 
   d_theories = Theory::setInsert(currentTheoryId, d_theories);
   d_theories = Theory::setInsert(parentTheoryId, d_theories);
@@ -62,10 +62,10 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
       TypeNode type = current.getType();
       useType = true;
-      typeTheoryId = Theory::theoryOf(type);
+      typeTheoryId = d_engine->theoryIdOf(type);
     } else {
       TypeNode type = current.getType();
-      typeTheoryId = Theory::theoryOf(type);
+      typeTheoryId = d_engine->theoryIdOf(type);
       if (typeTheoryId != currentTheoryId) {
         if (type.isInterpretedFinite()) {
           useType = true;
@@ -88,7 +88,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
     // The current theory has already visited it, so now it depends on the parent and the type
     if (Theory::setContains(parentTheoryId, visitedTheories)) {
       if (useType) {
-        TheoryId typeTheoryId = Theory::theoryOf(current.getType());
+        TheoryId typeTheoryId = d_engine->theoryIdOf(current.getType());
         d_theories = Theory::setInsert(typeTheoryId, d_theories);
         return Theory::setContains(typeTheoryId, visitedTheories);
       } else {
@@ -110,8 +110,8 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
   }
 
   // Get the theories of the terms
-  TheoryId currentTheoryId = Theory::theoryOf(current);
-  TheoryId parentTheoryId  = Theory::theoryOf(parent);
+  TheoryId currentTheoryId = d_engine->theoryIdOf(current);
+  TheoryId parentTheoryId = d_engine->theoryIdOf(parent);
 
   // Should we use the theory of the type
   bool useType = false;
@@ -122,10 +122,10 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
       TypeNode type = current.getType();
       useType = true;
-      typeTheoryId = Theory::theoryOf(type);
+      typeTheoryId = d_engine->theoryIdOf(type);
     } else {
       TypeNode type = current.getType();
-      typeTheoryId = Theory::theoryOf(type);
+      typeTheoryId = d_engine->theoryIdOf(type);
       if (typeTheoryId != currentTheoryId) {
         if (type.isInterpretedFinite()) {
           useType = true;
@@ -199,8 +199,8 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 
   Theory::Set theories = (*find).second;
 
-  TheoryId currentTheoryId = Theory::theoryOf(current);
-  TheoryId parentTheoryId  = Theory::theoryOf(parent);
+  TheoryId currentTheoryId = d_engine->theoryIdOf(current);
+  TheoryId parentTheoryId = d_engine->theoryIdOf(parent);
 
   // Should we use the theory of the type
   bool useType = false;
@@ -211,10 +211,10 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
       TypeNode type = current.getType();
       useType = true;
-      typeTheoryId = Theory::theoryOf(type);
+      typeTheoryId = d_engine->theoryIdOf(type);
     } else {
       TypeNode type = current.getType();
-      typeTheoryId = Theory::theoryOf(type);
+      typeTheoryId = d_engine->theoryIdOf(type);
       if (typeTheoryId != currentTheoryId) {
         if (type.isInterpretedFinite()) {
           useType = true;
@@ -227,10 +227,10 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
       TypeNode type = current.getType();
       useType = true;
-      typeTheoryId = Theory::theoryOf(type);
+      typeTheoryId = d_engine->theoryIdOf(type);
     } else {
       TypeNode type = current.getType();
-      typeTheoryId = Theory::theoryOf(type);
+      typeTheoryId = d_engine->theoryIdOf(type);
       if (typeTheoryId != currentTheoryId) {
         if (type.isInterpretedFinite()) {
           useType = true;
@@ -262,8 +262,8 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
   }
 
   // Get the theories of the terms
-  TheoryId currentTheoryId = Theory::theoryOf(current);
-  TheoryId parentTheoryId  = Theory::theoryOf(parent);
+  TheoryId currentTheoryId = d_engine->theoryIdOf(current);
+  TheoryId parentTheoryId = d_engine->theoryIdOf(parent);
 
   // Should we use the theory of the type
   bool useType = false;
@@ -274,10 +274,10 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
       TypeNode type = current.getType();
       useType = true;
-      typeTheoryId = Theory::theoryOf(type);
+      typeTheoryId = d_engine->theoryIdOf(type);
     } else {
       TypeNode type = current.getType();
-      typeTheoryId = Theory::theoryOf(type);
+      typeTheoryId = d_engine->theoryIdOf(type);
       if (typeTheoryId != currentTheoryId) {
         if (type.isInterpretedFinite()) {
           useType = true;
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index cdb411c16..13a14881b 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -98,32 +98,13 @@ public:
  * been visited already, we need to visit it again, since we need to associate it with both atoms.
  */
 class SharedTermsVisitor {
-
-  /** The shared terms database */
-  SharedTermsDatabase& d_sharedTerms;
-
-  /**
-   * Cache from preprocessing of atoms.
-   */
-  typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
-  TNodeVisitedMap d_visited;
-
-  /**
-   * String representation of the visited map, for debugging purposes.
-   */
-  std::string toString() const;
-
-  /** 
-   * The initial atom.
-   */
-  TNode d_atom; 
-    
 public:
-
   typedef void return_type;
 
-  SharedTermsVisitor(SharedTermsDatabase& sharedTerms)
-  : d_sharedTerms(sharedTerms) {}
+  SharedTermsVisitor(TheoryEngine* engine, SharedTermsDatabase& sharedTerms)
+      : d_engine(engine), d_sharedTerms(sharedTerms)
+  {
+  }
 
   /**
    * Returns true is current has already been pre-registered with both current and parent theories.
@@ -149,7 +130,29 @@ public:
    * Clears the internal state.
    */   
   void clear();
-};
 
+ private:
+  /** The engine */
+  TheoryEngine* d_engine;
+
+  /** The shared terms database */
+  SharedTermsDatabase& d_sharedTerms;
+
+  /**
+   * Cache from preprocessing of atoms.
+   */
+  typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction>
+      TNodeVisitedMap;
+  TNodeVisitedMap d_visited;
 
+  /**
+   * String representation of the visited map, for debugging purposes.
+   */
+  std::string toString() const;
+
+  /**
+   * The initial atom.
+   */
+  TNode d_atom;
+};
 }
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 719239806..140f0de63 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -53,6 +53,7 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){
 }/* ostream& operator<<(ostream&, Theory::Effort) */
 
 Theory::Theory(TheoryId id,
+               Environment* env,
                context::Context* satContext,
                context::UserContext* userContext,
                OutputChannel& out,
@@ -71,6 +72,7 @@ Theory::Theory(TheoryId id,
       d_quantEngine(NULL),
       d_decManager(nullptr),
       d_extTheory(NULL),
+      d_env(env),
       d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
       d_computeCareGraphTime(getStatsPrefix(id) + name
                              + "::computeCareGraphTime"),
diff --git a/src/theory/theory.h b/src/theory/theory.h
index b133b878e..cc42e9788 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -139,7 +139,7 @@ private:
   ExtTheory* d_extTheory;
 
  protected:
-
+  Environment* d_env;
 
   // === STATISTICS ===
   /** time spent in check calls */
@@ -196,6 +196,7 @@ private:
    * w.r.t. the SmtEngine.
    */
   Theory(TheoryId id,
+         Environment* env,
          context::Context* satContext,
          context::UserContext* userContext,
          OutputChannel& out,
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7a72367de..e7b044f81 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -310,15 +310,18 @@ void TheoryEngine::eqNotifyNewClass(TNode t){
   }
 }
 
-TheoryEngine::TheoryEngine(context::Context* context,
+TheoryEngine::TheoryEngine(Environment* env,
+                           context::Context* context,
                            context::UserContext* userContext,
                            RemoveTermFormulas& iteRemover,
                            const LogicInfo& logicInfo,
                            LemmaChannels* channels)
-    : d_propEngine(nullptr),
+    : d_env(env),
+      d_propEngine(nullptr),
       d_decisionEngine(nullptr),
       d_context(context),
       d_userContext(userContext),
+      d_uninterpretedSortOwner(THEORY_UF),
       d_logicInfo(logicInfo),
       d_sharedTerms(this, context),
       d_masterEqualityEngine(nullptr),
@@ -352,7 +355,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_inPreregister(false),
       d_factsAsserted(context, false),
       d_preRegistrationVisitor(this, context),
-      d_sharedTermsVisitor(d_sharedTerms),
+      d_sharedTermsVisitor(this, d_sharedTerms),
       d_theoryAlternatives(),
       d_attr_handle(),
       d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
@@ -432,7 +435,8 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
       theories = Theory::setRemove(THEORY_BOOL, theories);
       // Remove the top theory, if any more that means multiple theories were involved
-      bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories);
+      bool multipleTheories =
+          Theory::setRemove(theoryIdOf(preprocessed), theories);
       TheoryId i;
       // These checks don't work with finite model finding, because it
       // uses Rational constants to represent cardinality constraints,
@@ -1070,11 +1074,12 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
 
-  if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) &&
-     Theory::theoryOf(atom) != THEORY_SAT_SOLVER) {
+  if (!d_logicInfo.isTheoryEnabled(theoryIdOf(atom))
+      && theoryIdOf(atom) != THEORY_SAT_SOLVER)
+  {
     stringstream ss;
     ss << "The logic was specified as " << d_logicInfo.getLogicString()
-       << ", which doesn't include " << Theory::theoryOf(atom)
+       << ", which doesn't include " << theoryIdOf(atom)
        << ", but got a preprocessing-time fact for that theory." << endl
        << "The fact:" << endl
        << literal;
@@ -1164,11 +1169,12 @@ Node TheoryEngine::preprocess(TNode assertion) {
       continue;
     }
 
-    if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(current)) &&
-       Theory::theoryOf(current) != THEORY_SAT_SOLVER) {
+    if (!d_logicInfo.isTheoryEnabled(theoryIdOf(current))
+        && theoryIdOf(current) != THEORY_SAT_SOLVER)
+    {
       stringstream ss;
       ss << "The logic was specified as " << d_logicInfo.getLogicString()
-         << ", which doesn't include " << Theory::theoryOf(current)
+         << ", which doesn't include " << theoryIdOf(current)
          << ", but got a preprocessing-time fact for that theory." << endl
          << "The fact:" << endl
          << current;
@@ -1176,7 +1182,8 @@ Node TheoryEngine::preprocess(TNode assertion) {
     }
 
     // If this is an atom, we preprocess its terms with the theory ppRewriter
-    if (Theory::theoryOf(current) != THEORY_BOOL) {
+    if (theoryIdOf(current) != THEORY_BOOL)
+    {
       Node ppRewritten = ppTheoryRewrite(current);
       d_ppCache[current] = ppRewritten;
       Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]);
@@ -1332,7 +1339,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
     // We know that this is normalized, so just send it off to the theory
     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
       // Is it preregistered
-      bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
+      bool preregistered = d_propEngine->isSatLiteral(assertion)
+                           && theoryIdOf(assertion) == toTheoryId;
       // We assert it
       theoryOf(toTheoryId)->assertFact(assertion, preregistered);
       // Mark that we have more information
@@ -1379,7 +1387,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
   // Try and assert (note that we assert the non-normalized one)
   if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
     // Check if has been pre-registered with the theory
-    bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
+    bool preregistered = d_propEngine->isSatLiteral(assertion)
+                         && theoryIdOf(assertion) == toTheoryId;
     // Assert away
     theoryOf(toTheoryId)->assertFact(assertion, preregistered);
     d_factsAsserted = true;
@@ -1427,7 +1436,10 @@ void TheoryEngine::assertFact(TNode literal)
     // to the assert the equality to the interested theories
     if (atom.getKind() == kind::EQUAL) {
       // Assert it to the the owning theory
-      assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
+      assertToTheory(literal,
+                     literal,
+                     /* to */ theoryIdOf(atom),
+                     /* from */ THEORY_SAT_SOLVER);
       // Shared terms manager will assert to interested theories directly, as the terms become shared
       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
 
@@ -1443,11 +1455,17 @@ void TheoryEngine::assertFact(TNode literal)
 
     } else {
       // Not an equality, just assert to the appropriate theory
-      assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
+      assertToTheory(literal,
+                     literal,
+                     /* to */ theoryIdOf(atom),
+                     /* from */ THEORY_SAT_SOLVER);
     }
   } else {
     // Assert the fact to the appropriate theory directly
-    assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
+    assertToTheory(literal,
+                   literal,
+                   /* to */ theoryIdOf(atom),
+                   /* from */ THEORY_SAT_SOLVER);
   }
 }
 
@@ -1504,6 +1522,159 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
   return !d_inConflict;
 }
 
+theory::TheoryId TheoryEngine::theoryIdOf(TypeNode typeNode) const
+{
+  Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl;
+  TheoryId id;
+  if (typeNode.getKind() == kind::TYPE_CONSTANT)
+  {
+    id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
+  }
+  else
+  {
+    id = kindToTheoryId(typeNode.getKind());
+  }
+  if (id == THEORY_BUILTIN)
+  {
+    Trace("theory::internal")
+        << "theoryOf(" << typeNode << ") == " << d_uninterpretedSortOwner
+        << std::endl;
+    return d_uninterpretedSortOwner;
+  }
+  return id;
+}
+
+TheoryId TheoryEngine::theoryIdOf(TheoryOfMode mode, TNode node) const
+{
+  TheoryId tid = THEORY_BUILTIN;
+  switch (mode)
+  {
+    case THEORY_OF_TYPE_BASED:
+      // Constants, variables, 0-ary constructors
+      if (node.isVar())
+      {
+        if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+        {
+          tid = THEORY_UF;
+        }
+        else
+        {
+          tid = theoryIdOf(node.getType());
+        }
+      }
+      else if (node.isConst())
+      {
+        tid = theoryIdOf(node.getType());
+      }
+      else if (node.getKind() == kind::EQUAL)
+      {
+        // Equality is owned by the theory that owns the domain
+        tid = theoryIdOf(node[0].getType());
+      }
+      else
+      {
+        // Regular nodes are owned by the kind
+        tid = kindToTheoryId(node.getKind());
+      }
+      break;
+    case THEORY_OF_TERM_BASED:
+      // Variables
+      if (node.isVar())
+      {
+        if (theoryIdOf(node.getType()) != theory::THEORY_BOOL)
+        {
+          // We treat the variables as uninterpreted
+          tid = d_uninterpretedSortOwner;
+        }
+        else
+        {
+          if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+          {
+            // Boolean vars go to UF
+            tid = THEORY_UF;
+          }
+          else
+          {
+            // Except for the Boolean ones
+            tid = THEORY_BOOL;
+          }
+        }
+      }
+      else if (node.isConst())
+      {
+        // Constants go to the theory of the type
+        tid = theoryIdOf(node.getType());
+      }
+      else if (node.getKind() == kind::EQUAL)
+      {  // Equality
+        // If one of them is an ITE, it's irelevant, since they will get
+        // replaced out anyhow
+        if (node[0].getKind() == kind::ITE)
+        {
+          tid = theoryIdOf(node[0].getType());
+        }
+        else if (node[1].getKind() == kind::ITE)
+        {
+          tid = theoryIdOf(node[1].getType());
+        }
+        else
+        {
+          TNode l = node[0];
+          TNode r = node[1];
+          TypeNode ltype = l.getType();
+          TypeNode rtype = r.getType();
+          if (ltype != rtype)
+          {
+            tid = theoryIdOf(l.getType());
+          }
+          else
+          {
+            // If both sides belong to the same theory the choice is easy
+            TheoryId T1 = theoryIdOf(l);
+            TheoryId T2 = theoryIdOf(r);
+            if (T1 == T2)
+            {
+              tid = T1;
+            }
+            else
+            {
+              TheoryId T3 = theoryIdOf(ltype);
+              // This is a case of
+              // * x*y = f(z) -> UF
+              // * x = c      -> UF
+              // * f(x) = read(a, y) -> either UF or ARRAY
+              // at least one of the theories has to be parametric, i.e. theory
+              // of the type is different from the theory of the term
+              if (T1 == T3)
+              {
+                tid = T2;
+              }
+              else if (T2 == T3)
+              {
+                tid = T1;
+              }
+              else
+              {
+                // If both are parametric, we take the smaller one (arbitrary)
+                tid = T1 < T2 ? T1 : T2;
+              }
+            }
+          }
+        }
+      }
+      else
+      {
+        // Regular nodes are owned by the kind
+        tid = kindToTheoryId(node.getKind());
+      }
+      break;
+    default: Unreachable();
+  }
+  Trace("theory::internal")
+      << "theoryIdOf(" << mode << ", " << node << ") -> " << tid << std::endl;
+  return tid;
+}
+
 const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
 
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
@@ -1516,7 +1687,7 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
       return EQUALITY_FALSE_AND_PROPAGATED;
     }
   }
-  return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
+  return theoryOf(theoryIdOf(a.getType()))->getEqualityStatus(a, b);
 }
 
 Node TheoryEngine::getModelValue(TNode var) {
@@ -1526,7 +1697,7 @@ Node TheoryEngine::getModelValue(TNode var) {
     return var;
   }
   Assert(d_sharedTerms.isShared(var));
-  return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
+  return theoryOf(theoryIdOf(var.getType()))->getModelValue(var);
 }
 
 
@@ -1733,25 +1904,28 @@ Node TheoryEngine::getExplanation(TNode node) {
 }
 
 struct AtomsCollect {
-
+  const TheoryEngine* d_te;
   std::vector<TNode> d_atoms;
   std::unordered_set<TNode, TNodeHashFunction> d_visited;
 
 public:
+ AtomsCollect(const TheoryEngine* te) : d_te(te) {}
 
-  typedef void return_type;
+ typedef void return_type;
 
-  bool alreadyVisited(TNode current, TNode parent) {
-    // Check if already visited
-    if (d_visited.find(current) != d_visited.end()) return true;
-    // Don't visit non-boolean
-    if (!current.getType().isBoolean()) return true;
-    // New node
-    return false;
-  }
+ bool alreadyVisited(TNode current, TNode parent)
+ {
+   // Check if already visited
+   if (d_visited.find(current) != d_visited.end()) return true;
+   // Don't visit non-boolean
+   if (!current.getType().isBoolean()) return true;
+   // New node
+   return false;
+ }
 
   void visit(TNode current, TNode parent) {
-    if (Theory::theoryOf(current) != theory::THEORY_BOOL) {
+    if (d_te->theoryIdOf(current) != theory::THEORY_BOOL)
+    {
       d_atoms.push_back(current);
     }
     d_visited.insert(current);
@@ -1823,7 +1997,8 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
 
     // If the theory is asking about a different form, or the form is ok but if will go to a different theory
     // then we must figure it out
-    if (eqNormalized != eq || Theory::theoryOf(eq) != atomsTo) {
+    if (eqNormalized != eq || theoryIdOf(eq) != atomsTo)
+    {
       // If you get eqNormalized, send atoms[i] to atomsTo
       d_atomRequests.add(eqNormalized, eq, atomsTo);
     }
@@ -1842,7 +2017,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   // Do we need to check atoms
   if (atomsTo != theory::THEORY_LAST) {
     Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl;
-    AtomsCollect collectAtoms;
+    AtomsCollect collectAtoms(this);
     NodeVisitor<AtomsCollect>::run(collectAtoms, node);
     ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo);
   }
@@ -2026,7 +2201,8 @@ void TheoryEngine::staticInitializeBVOptions(
     bv::utils::TNodeBoolMap cache;
     for (unsigned i = 0; i < assertions.size(); ++i)
     {
-      useSlicer = useSlicer && bv::utils::isCoreTerm(assertions[i], cache);
+      useSlicer =
+          useSlicer && bv::utils::isCoreTerm(d_env, assertions[i], cache);
     }
   }
 
@@ -2290,7 +2466,7 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T
     return std::pair<bool, Node>(false, Node::null());
   }else{
     //it is a theory atom
-    theory::TheoryId tid = theory::Theory::theoryOf(mode, atom);
+    theory::TheoryId tid = theoryIdOf(mode, atom);
     theory::Theory* th = theoryOf(tid);
 
     Assert(th != NULL);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index dd34ae16b..ca999f569 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -23,8 +23,8 @@
 #include <memory>
 #include <set>
 #include <unordered_map>
-#include <vector>
 #include <utility>
+#include <vector>
 
 #include "base/check.h"
 #include "context/cdhashset.h"
@@ -33,6 +33,7 @@
 #include "options/smt_options.h"
 #include "prop/prop_engine.h"
 #include "smt/command.h"
+#include "smt/environment.h"
 #include "smt_util/lemma_channels.h"
 #include "theory/atom_requests.h"
 #include "theory/decision_manager.h"
@@ -113,6 +114,8 @@ class TheoryEngine {
   friend class SharedTermsDatabase;
   friend class theory::quantifiers::TermDb;
 
+  Environment* d_env;
+
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;
 
@@ -132,6 +135,11 @@ class TheoryEngine {
   theory::Theory* d_theoryTable[theory::THEORY_LAST];
 
   /**
+   * The theory that owns the uninterpreted sort.
+   */
+  theory::TheoryId d_uninterpretedSortOwner;
+
+  /**
    * A collection of theories that are "active" for the current run.
    * This set is provided by the user (as a logic string, say, in SMT-LIBv2
    * format input), or else by default it's all-inclusive.  This is important
@@ -467,11 +475,13 @@ class TheoryEngine {
   /** Container for lemma input and output channels. */
   LemmaChannels* d_channels;
 
-public:
-
+ public:
   /** Constructs a theory engine */
-  TheoryEngine(context::Context* context, context::UserContext* userContext,
-               RemoveTermFormulas& iteRemover, const LogicInfo& logic,
+  TheoryEngine(Environment* env,
+               context::Context* context,
+               context::UserContext* userContext,
+               RemoveTermFormulas& iteRemover,
+               const LogicInfo& logic,
                LemmaChannels* channels);
 
   /** Destroys a theory engine */
@@ -487,12 +497,16 @@ public:
    * there is another theory it will be deleted.
    */
   template <class TheoryClass>
-  inline void addTheory(theory::TheoryId theoryId) {
+  inline void addTheory(theory::TheoryId theoryId)
+  {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
     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_theoryTable[theoryId] = new TheoryClass(d_env,
+                                              d_context,
+                                              d_userContext,
+                                              *d_theoryOut[theoryId],
+                                              theory::Valuation(this),
+                                              d_logicInfo);
   }
 
   inline void setPropEngine(prop::PropEngine* propEngine) {
@@ -509,6 +523,22 @@ public:
   void finishInit();
 
   /**
+   * Set the owner of the uninterpreted sort.
+   */
+  void setUninterpretedSortOwner(theory::TheoryId theory)
+  {
+    d_uninterpretedSortOwner = theory;
+  }
+
+  /**
+   * Get the owner of the uninterpreted sort.
+   */
+  theory::TheoryId getUninterpretedSortOwner()
+  {
+    return d_uninterpretedSortOwner;
+  }
+
+  /**
    * Get a pointer to the underlying propositional engine.
    */
   inline prop::PropEngine* getPropEngine() const {
@@ -793,7 +823,7 @@ public:
    * of built-in type.
    */
   inline theory::Theory* theoryOf(TNode node) const {
-    return d_theoryTable[theory::Theory::theoryOf(node)];
+    return d_theoryTable[theoryIdOf(node)];
   }
 
   /**
@@ -806,6 +836,24 @@ public:
     return d_theoryTable[theoryId];
   }
 
+  /**
+   * Return the ID of the theory responsible for the given type.
+   */
+  theory::TheoryId theoryIdOf(TypeNode typeNode) const;
+
+  /**
+   * Returns the ID of the theory responsible for the given node.
+   */
+  theory::TheoryId theoryIdOf(theory::TheoryOfMode mode, TNode node) const;
+
+  /**
+   * Returns the ID of the theory responsible for the given node.
+   */
+  theory::TheoryId theoryIdOf(TNode node) const
+  {
+    return theoryIdOf(options::theoryOfMode(), node);
+  }
+
   inline bool isTheoryEnabled(theory::TheoryId theoryId) const {
     return d_logicInfo.isTheoryEnabled(theoryId);
   }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 95e3f702b..be07334b7 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -40,13 +40,14 @@ namespace theory {
 namespace uf {
 
 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-TheoryUF::TheoryUF(context::Context* c,
+TheoryUF::TheoryUF(Environment* env,
+                   context::Context* c,
                    context::UserContext* u,
                    OutputChannel& out,
                    Valuation valuation,
                    const LogicInfo& logicInfo,
                    std::string instanceName)
-    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, instanceName),
+    : Theory(THEORY_UF, env, 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. */
@@ -127,7 +128,8 @@ void TheoryUF::check(Effort level) {
     TNode fact = assertion.assertion;
 
     Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
-    Debug("uf") << "Term's theory: " << theory::Theory::theoryOf(fact.toExpr()) << std::endl;
+    Debug("uf") << "Term's theory: " << d_env->theoryOf(fact.toExpr())
+                << std::endl;
 
     if (d_thss != NULL) {
       bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index dd69b2ee2..b7ef40e7d 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -186,8 +186,12 @@ private:
  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,
+  TheoryUF(Environment* env,
+           context::Context* c,
+           context::UserContext* u,
+           OutputChannel& out,
+           Valuation valuation,
+           const LogicInfo& logicInfo,
            std::string instanceName = "");
 
   ~TheoryUF();