Eliminate static options access for central ee (#8823)

Also refactors TheoryEngine to not maintain its own reference to logic info and an accessor to it.

Towards eliminating option scopes.

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 9847725c880a5aac891b9819c55cf9191c15a32d..07755344f371f656072d948022279dd4b7c23680 100644 (file)
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -35,7 +35,7 @@ CombinationEngine::CombinationEngine(Env& env,
       d_te(te),
       d_valuation(&te),
       d_pnm(env.isTheoryProofProducing() ? env.getProofNodeManager() : nullptr),
-      d_logicInfo(te.getLogicInfo()),
+      d_logicInfo(env.getLogicInfo()),
       d_paraTheories(paraTheories),
       d_eemanager(nullptr),
       d_mmanager(nullptr),

diff --git a/src/theory/ee_manager_central.cpp b/src/theory/ee_manager_central.cpp
index cef387f3c529727e3fe15b72a0cd3009bbd402ef..02488604e9e9532a7833b7975213f7ca99fc84c8 100644 (file)
--- a/src/theory/ee_manager_central.cpp
+++ b/src/theory/ee_manager_central.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/ee_manager_central.h"
 
+#include "options/arith_options.h"
+#include "options/theory_options.h"
 #include "smt/env.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/shared_solver.h"
@@ -70,7 +72,7 @@ void EqEngineManagerCentral::initializeTheories()
   std::map<TheoryId, EeSetupInfo> esiMap;
   // set of theories that need equality engines
   std::unordered_set<TheoryId> eeTheories;
-  const LogicInfo& logicInfo = d_te.getLogicInfo();
+  const LogicInfo& linfo = logicInfo();
   for (TheoryId theoryId = theory::THEORY_FIRST;
        theoryId != theory::THEORY_LAST;
        ++theoryId)
@@ -91,8 +93,8 @@ void EqEngineManagerCentral::initializeTheories()
     // if the logic has a theory that does not use central equality engine,
     // we can't use the central equality engine for the master equality
     // engine
-    if (theoryId != THEORY_QUANTIFIERS && logicInfo.isTheoryEnabled(theoryId)
-        && !Theory::usesCentralEqualityEngine(theoryId))
+    if (theoryId != THEORY_QUANTIFIERS && linfo.isTheoryEnabled(theoryId)
+        && !usesCentralEqualityEngine(options(), theoryId))
     {
       Trace("ee-central") << "Must use separate master equality engine due to "
                           << theoryId << std::endl;
@@ -102,7 +104,7 @@ void EqEngineManagerCentral::initializeTheories()
 
   // initialize the master equality engine, which may be the central equality
   // engine
-  if (logicInfo.isQuantified())
+  if (linfo.isQuantified())
   {
     // construct the master equality engine
     Assert(d_masterEqualityEngine == nullptr);
@@ -155,12 +157,12 @@ void EqEngineManagerCentral::initializeTheories()
     eq::EqualityEngineNotify* notify = esi.d_notify;
     d_theoryNotify[theoryId] = notify;
     // split on whether integrated, or whether asked for master
-    if (t->usesCentralEqualityEngine())
+    if (usesCentralEqualityEngine(options(), t->getId()))
     {
       Trace("ee-central") << "...uses central" << std::endl;
       // the theory uses the central equality engine
       eet.d_usedEe = &d_centralEqualityEngine;
-      if (logicInfo.isTheoryEnabled(theoryId))
+      if (linfo.isTheoryEnabled(theoryId))
       {
         // add to vectors for the kinds of notifications
         if (esi.needsNotifyNewClass())
@@ -196,6 +198,24 @@ void EqEngineManagerCentral::initializeTheories()
   }
 }
 
+bool EqEngineManagerCentral::usesCentralEqualityEngine(const Options& opts,
+                                                       TheoryId id)
+{
+  Assert(opts.theory.eeMode == options::EqEngineMode::CENTRAL);
+  if (id == THEORY_BUILTIN)
+  {
+    return true;
+  }
+  if (id == THEORY_ARITH)
+  {
+    // conditional on whether we are using the equality solver
+    return opts.arith.arithEqSolver;
+  }
+  return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS
+         || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS
+         || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV;
+}
+
 void EqEngineManagerCentral::notifyBuildingModel() {}
 
 EqEngineManagerCentral::CentralNotifyClass::CentralNotifyClass(

diff --git a/src/theory/ee_manager_central.h b/src/theory/ee_manager_central.h
index 2b9677573b710bfa8b073c001464375234fd3ee0..536ab1505ef94269086aca22d6f075cb119775ec 100644 (file)
--- a/src/theory/ee_manager_central.h
+++ b/src/theory/ee_manager_central.h
@@ -64,6 +64,12 @@ class EqEngineManagerCentral : public EqEngineManager
   /** Notify this class that we are building the model. */
   void notifyBuildingModel();
 
+  /**
+   * Return true if the theory with the given id uses central equality engine
+   * with the given options.
+   */
+  static bool usesCentralEqualityEngine(const Options& opts, TheoryId id);
+
  private:
   /**
    * Notify class for central equality engine. This class dispatches

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 5345c59594bc7f4d99257cd7a440ddc777512f92..81bf7c1c289d6cdb93058101dd5e155ed8288a30 100644 (file)
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -194,16 +194,9 @@ void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
     // guaranteed to be initialized.
     if (!te->isTheoryEnabled(id))
     {
-      const LogicInfo& l = te->getLogicInfo();
-      LogicInfo newLogicInfo = l.getUnlockedCopy();
-      newLogicInfo.enableTheory(id);
-      newLogicInfo.lock();
       std::stringstream ss;
-      ss << "The logic was specified as " << l.getLogicString()
-         << ", which doesn't include " << id
-         << ", but found a term in that theory." << std::endl
-         << "You might want to extend your logic to "
-         << newLogicInfo.getLogicString() << std::endl;
+      ss << "The logic doesn't include theory " << id
+         << ", but found a term in that theory." << std::endl;
       throw LogicException(ss.str());
     }
   }

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9ba9ad028b7e6b0ef5b7441a8f5fd9eb4f5e2768..35f2af16be8ed1b44f2dd9fb5d909e9f22028225 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -672,34 +672,9 @@ eq::EqualityEngine* Theory::getEqualityEngine()
   return d_equalityEngine;
 }
 
-bool Theory::usesCentralEqualityEngine() const
-{
-  return usesCentralEqualityEngine(d_id);
-}
-
-bool Theory::usesCentralEqualityEngine(TheoryId id)
-{
-  if (id == THEORY_BUILTIN)
-  {
-    return true;
-  }
-  if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
-  {
-    return false;
-  }
-  if (id == THEORY_ARITH)
-  {
-    // conditional on whether we are using the equality solver
-    return options::arithEqSolver();
-  }
-  return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS
-         || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS
-         || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV;
-}
-
 bool Theory::expUsingCentralEqualityEngine(TheoryId id)
 {
-  return id != THEORY_ARITH && usesCentralEqualityEngine(id);
+  return id != THEORY_ARITH;
 }
 
 theory::Assertion Theory::get()

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1001db7ee48cf82c749a598a6ebbb28678af553f..5267e0f53f5b713eb0534108bf8c2ca11984cbf7 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -787,11 +787,10 @@ class Theory : protected EnvObj
    */
   virtual std::pair<bool, Node> entailmentCheck(TNode lit);
 
-  /** Return true if this theory uses central equality engine */
-  bool usesCentralEqualityEngine() const;
-  /** uses central equality engine (static) */
-  static bool usesCentralEqualityEngine(TheoryId id);
-  /** Explains/propagates via central equality engine only */
+  /**
+   * Return true if this theory explains and propagates via central equality
+   * engine only when the theory uses the central equality engine.
+   */
   static bool expUsingCentralEqualityEngine(TheoryId id);
 
  private:

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index fed582cc5d0e10d3704fcd4ed2c9ba1e5faed95e..e38839530d06cd32a7861b31dee6e1bd09158070 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -35,6 +35,7 @@
 #include "smt/logic_exception.h"
 #include "theory/combination_care_graph.h"
 #include "theory/decision_manager.h"
+#include "theory/ee_manager_central.h"
 #include "theory/partition_generator.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers_engine.h"
@@ -136,7 +137,7 @@ void TheoryEngine::finishInit()
 #endif
 #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY)   \
   if (theory::TheoryTraits<THEORY>::isParametric \
-      && d_logicInfo.isTheoryEnabled(THEORY))    \
+      && isTheoryEnabled(THEORY))    \
   {                                              \
     paraTheories.push_back(theoryOf(THEORY));    \
   }
@@ -161,7 +162,7 @@ void TheoryEngine::finishInit()
   }
 
   // initialize the quantifiers engine
-  if (d_logicInfo.isQuantified())
+  if (logicInfo().isQuantified())
   {
     // get the quantifiers engine, which is initialized by the quantifiers
     // theory
@@ -171,7 +172,7 @@ void TheoryEngine::finishInit()
   // finish initializing the quantifiers engine, which must come before
   // initializing theory combination, since quantifiers engine may have a
   // special model builder object
-  if (d_logicInfo.isQuantified())
+  if (logicInfo().isQuantified())
   {
     d_quantEngine->finishInit(this);
   }
@@ -214,7 +215,6 @@ void TheoryEngine::finishInit()
 TheoryEngine::TheoryEngine(Env& env)
     : EnvObj(env),
       d_propEngine(nullptr),
-      d_logicInfo(env.getLogicInfo()),
       d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
                                            : nullptr),
       d_lazyProof(
@@ -320,7 +320,8 @@ void TheoryEngine::printAssertions(const char* tag) {
 
     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
       Theory* theory = d_theoryTable[theoryId];
-      if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
+      if (theory && isTheoryEnabled(theoryId))
+      {
         Trace(tag) << "--------------------------------------------" << endl;
         Trace(tag) << "Assertions of " << theory->getId() << ": " << endl;
         {
@@ -341,7 +342,8 @@ void TheoryEngine::printAssertions(const char* tag) {
           }
         }
 
-        if (d_logicInfo.isSharingEnabled()) {
+        if (logicInfo().isSharingEnabled())
+        {
           Trace(tag) << "Shared terms of " << theory->getId() << ": " << endl;
           context::CDList<TNode>::const_iterator
               it = theory->shared_terms_begin(),
@@ -370,7 +372,7 @@ void TheoryEngine::check(Theory::Effort effort) {
 #endif
 #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY)                      \
   if (theory::TheoryTraits<THEORY>::hasCheck                        \
-      && d_logicInfo.isTheoryEnabled(THEORY))                       \
+      && isTheoryEnabled(THEORY))                       \
   {                                                                 \
     theoryOf(THEORY)->check(effort);                                \
     if (d_inConflict)                                               \
@@ -442,7 +444,7 @@ void TheoryEngine::check(Theory::Effort effort) {
       propagate(effort);
 
       // We do combination if all has been processed and we are in fullcheck
-      if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled()
+      if (Theory::fullEffort(effort) && logicInfo().isSharingEnabled()
           && !d_factsAsserted && !needCheck() && !d_inConflict)
       {
         // Do the combination
@@ -451,7 +453,8 @@ void TheoryEngine::check(Theory::Effort effort) {
           TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
           d_tc->combineTheories();
         }
-        if(d_logicInfo.isQuantified()){
+        if (logicInfo().isQuantified())
+        {
           d_quantEngine->notifyCombineTheories();
         }
       }
@@ -469,7 +472,8 @@ void TheoryEngine::check(Theory::Effort effort) {
       for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
         if( theoryId!=THEORY_QUANTIFIERS ){
           Theory* theory = d_theoryTable[theoryId];
-          if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
+          if (theory && isTheoryEnabled(theoryId))
+          {
             if( theory->needsCheckLastEffort() ){
               if (!d_tc->buildModel())
               {
@@ -482,7 +486,8 @@ void TheoryEngine::check(Theory::Effort effort) {
       }
       if (!d_inConflict)
       {
-        if(d_logicInfo.isQuantified()) {
+        if (logicInfo().isQuantified())
+        {
           // quantifiers engine must check at last call effort
           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
         }
@@ -532,7 +537,7 @@ void TheoryEngine::propagate(Theory::Effort effort)
 #endif
 #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY)   \
   if (theory::TheoryTraits<THEORY>::hasPropagate \
-      && d_logicInfo.isTheoryEnabled(THEORY))    \
+      && isTheoryEnabled(THEORY))    \
   {                                              \
     theoryOf(THEORY)->propagate(effort);         \
   }
@@ -626,6 +631,24 @@ bool TheoryEngine::buildModel()
   return d_tc->buildModel();
 }
 
+bool TheoryEngine::isTheoryEnabled(theory::TheoryId theoryId) const
+{
+  return logicInfo().isTheoryEnabled(theoryId);
+}
+
+theory::TheoryId TheoryEngine::theoryExpPropagation(theory::TheoryId tid) const
+{
+  if (options().theory.eeMode == options::EqEngineMode::CENTRAL)
+  {
+    if (EqEngineManagerCentral::usesCentralEqualityEngine(options(), tid)
+        && Theory::expUsingCentralEqualityEngine(tid))
+    {
+      return THEORY_BUILTIN;
+    }
+  }
+  return tid;
+}
+
 bool TheoryEngine::presolve() {
   // Reset the interrupt flag
   d_interrupted = false;
@@ -696,7 +719,7 @@ void TheoryEngine::notifyRestart() {
 #endif
 #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY)       \
   if (theory::TheoryTraits<THEORY>::hasNotifyRestart \
-      && d_logicInfo.isTheoryEnabled(THEORY))        \
+      && isTheoryEnabled(THEORY))        \
   {                                                  \
     theoryOf(THEORY)->notifyRestart();               \
   }
@@ -746,10 +769,10 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
 
   theory::TheoryId tid = d_env.theoryOf(atom);
-  if (!d_logicInfo.isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
+  if (!isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
   {
     stringstream ss;
-    ss << "The logic was specified as " << d_logicInfo.getLogicString()
+    ss << "The logic was specified as " << logicInfo().getLogicString()
        << ", which doesn't include " << tid
        << ", but got a preprocessing-time fact for that theory." << endl
        << "The fact:" << endl
@@ -839,10 +862,11 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
   Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl;
 
   Assert(toTheoryId != fromTheoryId);
-  if(toTheoryId != THEORY_SAT_SOLVER &&
-     ! d_logicInfo.isTheoryEnabled(toTheoryId)) {
+  if (toTheoryId != THEORY_SAT_SOLVER
+      && !isTheoryEnabled(toTheoryId))
+  {
     stringstream ss;
-    ss << "The logic was specified as " << d_logicInfo.getLogicString()
+    ss << "The logic was specified as " << logicInfo().getLogicString()
        << ", which doesn't include " << toTheoryId
        << ", but got an asserted fact to that theory." << endl
        << "The fact:" << endl
@@ -855,7 +879,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
   }
 
   // If sharing is disabled, things are easy
-  if (!d_logicInfo.isSharingEnabled()) {
+  if (!logicInfo().isSharingEnabled())
+  {
     Assert(assertion == originalAssertion);
     if (fromTheoryId == THEORY_SAT_SOLVER) {
       // Send to the apropriate theory
@@ -885,9 +910,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
 
   // determine the actual theory that will process/explain the fact, which is
   // THEORY_BUILTIN if the theory uses the central equality engine
-  TheoryId toTheoryIdProp = (Theory::expUsingCentralEqualityEngine(toTheoryId))
-                                ? THEORY_BUILTIN
-                                : toTheoryId;
+  TheoryId toTheoryIdProp = theoryExpPropagation(toTheoryId);
   // If sending to the shared solver, it's also simple
   if (toTheoryId == THEORY_BUILTIN) {
     if (markPropagation(
@@ -998,7 +1021,8 @@ void TheoryEngine::assertFact(TNode literal)
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
 
-  if (d_logicInfo.isSharingEnabled()) {
+  if (logicInfo().isSharingEnabled())
+  {
     // If any shared terms, it's time to do sharing work
     d_sharedSolver->preNotifySharedFact(atom);
 
@@ -1035,7 +1059,9 @@ void TheoryEngine::assertFact(TNode literal)
                      /* to */ d_env.theoryOf(atom),
                      /* from */ THEORY_SAT_SOLVER);
     }
-  } else {
+  }
+  else
+  {
     // Assert the fact to the appropriate theory directly
     assertToTheory(literal,
                    literal,
@@ -1057,7 +1083,8 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
 
-  if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) {
+  if (logicInfo().isSharingEnabled() && atom.getKind() == kind::EQUAL)
+  {
     if (d_propEngine->isSatLiteral(literal)) {
       // We propagate SAT literals to SAT
       assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
@@ -1066,7 +1093,9 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
       // Assert to the shared terms database
       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
     }
-  } else {
+  }
+  else
+  {
     // Just send off to the SAT solver
     Assert(d_propEngine->isSatLiteral(literal));
     assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
@@ -1075,8 +1104,6 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
   return !d_inConflict;
 }
 
-const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
-
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b)
 {
   Assert(a.getType() == b.getType());
@@ -1126,7 +1153,7 @@ TrustNode TheoryEngine::getExplanation(TNode node)
   TNode atom = polarity ? node : node[0];
 
   // If we're not in shared mode, explanations are simple
-  if (!d_logicInfo.isSharingEnabled())
+  if (!logicInfo().isSharingEnabled())
   {
     Trace("theory::explain")
         << "TheoryEngine::getExplanation: sharing is NOT enabled. "
@@ -1371,7 +1398,8 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId)
   markInConflict();
 
   // In the multiple-theories case, we need to reconstruct the conflict
-  if (d_logicInfo.isSharingEnabled()) {
+  if (logicInfo().isSharingEnabled())
+  {
     // Create the workplace for explanations
     std::vector<NodeTheoryPair> vec;
     vec.push_back(
@@ -1454,7 +1482,9 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId)
       tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing");
     }
     lemma(tconf, LemmaProperty::REMOVABLE);
-  } else {
+  }
+  else
+  {
     // When only one theory, the conflict should need no processing
     Assert(properConflict(conflict));
     // pass the trust node that was sent from the theory
@@ -1477,10 +1507,8 @@ TrustNode TheoryEngine::getExplanation(
   Node conclusion = explanationVector[0].d_node;
   // if the theory explains using the central equality engine, we always start
   // with THEORY_BUILTIN.
-  if (Theory::expUsingCentralEqualityEngine(explanationVector[0].d_theory))
-  {
-    explanationVector[0].d_theory = THEORY_BUILTIN;
-  }
+  explanationVector[0].d_theory =
+      theoryExpPropagation(explanationVector[0].d_theory);
   std::shared_ptr<LazyCDProof> lcp;
   if (isProofEnabled())
   {
@@ -1827,7 +1855,8 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
   }
   for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
     Theory* theory = d_theoryTable[theoryId];
-    if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
+    if (theory && isTheoryEnabled(theoryId))
+    {
       for (context::CDList<Assertion>::const_iterator
                it = theory->facts_begin(),
                it_end = theory->facts_end();

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7391fd60f757e75261399f660a06db017456271f..3f25eefcd0778be7a7f2df57d6df5a01bbe38e67 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -333,12 +333,9 @@ class TheoryEngine : protected EnvObj
     return d_theoryTable[theoryId];
   }
 
-  bool isTheoryEnabled(theory::TheoryId theoryId) const
-  {
-    return d_logicInfo.isTheoryEnabled(theoryId);
-  }
-  /** get the logic info used by this theory engine */
-  const LogicInfo& getLogicInfo() const;
+  bool isTheoryEnabled(theory::TheoryId theoryId) const;
+  /** return the theory that should explain a propagation from TheoryId */
+  theory::TheoryId theoryExpPropagation(theory::TheoryId tid) const;
 
   /**
    * Returns the equality status of the two terms, from the theory
@@ -501,15 +498,6 @@ class TheoryEngine : protected EnvObj
    */
   theory::Theory* d_theoryTable[theory::THEORY_LAST];
 
-  /**
-   * 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
-   * because we can optimize for single-theory runs (no sharing), can reduce
-   * the cost of walking the DAG on registration, etc.
-   */
-  const LogicInfo& d_logicInfo;
-
   //--------------------------------- new proofs
   /** Proof node manager used by this theory engine, if proofs are enabled */
   ProofNodeManager* d_pnm;