New LogicInfo functionality.

src/theory/logic_info.{h,cpp} contains the CVC4::LogicInfo class, which keeps
track of which theories are active (which should remain constant throughout
the life of an SmtEngine) and other details (like integers, reals,
linear/nonlinear, etc.).

This class has a default constructor which is the most all-inclusive logic.
Alternatively, this class can be constructed from an SMT-LIB logic string
(the empty string gives the same as "QF_SAT").  Once constructed, theories
can be enabled or disabled, quantifiers flipped on and off, integers flipped
on and off, etc.  At any point an SMT-LIB-like logic string can be extracted.  

The SmtEngine keeps a LogicInfo for itself and shares with the TheoryEngine
(and, in turn, the theories) only a const reference to it.  This ensures that
the logic info doesn't mutate over the course of the run.

As part of this commit, the TheoryEngine's old notion of "active theories"
has been completely removed.  As a result, SMT benchmarks that are incorrectly
tagged with a logic will assert-fail or worse.  (We should probably fail
more gracefully in this case.)  One such example was bug303.smt2,
which used UF reasoning but was tagged QF_LIA.  This has been fixed.

10 files changed, 544 insertions, 51 deletions

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 973163d62..fb76c1857 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -124,6 +124,8 @@ namespace theory {
 
 enum TheoryId {
 ${theory_enum}
+  THEORY_QUANTIFIERS,
+  THEORY_REWRITERULES,
   THEORY_LAST
 };
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c95b9d197..4b3410cf7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -57,6 +57,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/datatypes/theory_datatypes.h"
 #include "theory/theory_traits.h"
+#include "theory/logic_info.h"
 #include "util/ite_removal.h"
 
 using namespace std;
@@ -230,7 +231,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_definedFunctions(NULL),
   d_assertionList(NULL),
   d_assignments(NULL),
-  d_logic(""),
+  d_logic(),
+  d_logicIsSet(false),
   d_problemExtended(false),
   d_queryMade(false),
   d_needPostsolve(false),
@@ -256,7 +258,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
 
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine = new TheoryEngine(d_context, d_userContext);
+  d_theoryEngine = new TheoryEngine(d_context, d_userContext, const_cast<const LogicInfo&>(d_logic));
 
   // Add the theories
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -356,36 +358,44 @@ SmtEngine::~SmtEngine() throw() {
   }
 }
 
-void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
+void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
   NodeManagerScope nms(d_nodeManager);
 
-  if(d_logic != "") {
+  if(d_logicIsSet) {
     throw ModalException("logic already set");
   }
 
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetBenchmarkLogicCommand(s);
+    Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
   }
 
-  setLogicInternal(s);
+  setLogicInternal(logic);
+}
+
+void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
+  NodeManagerScope nms(d_nodeManager);
+
+  setLogic(LogicInfo(s));
 }
 
-void SmtEngine::setLogicInternal(const std::string& s) throw() {
-  d_logic = s;
+void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
+  d_logic = logic;
 
   // by default, symmetry breaker is on only for QF_UF
   if(! Options::current()->ufSymmetryBreakerSetByUser) {
-    Trace("smt") << "setting uf symmetry breaker to " << (s == "QF_UF") << std::endl;
-    NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = (s == "QF_UF");
+    bool qf_uf = logic.isPure(theory::THEORY_UF) && !logic.isQuantified();
+    Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl;
+    NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = qf_uf;
   }
   // by default, nonclausal simplification is off for QF_SAT
   if(! Options::current()->simplificationModeSetByUser) {
-    Trace("smt") << "setting simplification mode to <" << s << "> " << (s != "QF_SAT") << std::endl;
-    NodeManager::currentNM()->getOptions()->simplificationMode = (s == "QF_SAT" ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
+    bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
+    Trace("smt") << "setting simplification mode to <" << logic.getLogicString() << "> " << (!qf_sat) << std::endl;
+    NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
   }
 
   // If in arrays, set the UF handler to arrays
-  if(s == "QF_AX") {
+  if(logic.isPure(theory::THEORY_ARRAY) && !logic.isQuantified()) {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY);
   } else {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF);
@@ -513,7 +523,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
   } else {
     // The following options can only be set at the beginning; we throw
     // a ModalException if someone tries.
-    if(d_logic != "") {
+    if(d_logicIsSet) {
       throw ModalException("logic already set; cannot set options");
     }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 7feaa7e61..43d3e1125 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -37,6 +37,7 @@
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/stats.h"
+#include "theory/logic_info.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -131,7 +132,12 @@ class CVC4_PUBLIC SmtEngine {
   /**
    * The logic we're in.
    */
-  std::string d_logic;
+  LogicInfo d_logic;
+
+  /**
+   * Whether the logic has been set yet.
+   */
+  bool d_logicIsSet;
 
   /**
    * Whether or not we have added any assertions/declarations/definitions
@@ -212,7 +218,7 @@ class CVC4_PUBLIC SmtEngine {
   /**
    * Internally handle the setting of a logic.
    */
-  void setLogicInternal(const std::string& logic) throw();
+  void setLogicInternal(const LogicInfo& logic) throw();
 
   friend class ::CVC4::smt::SmtEnginePrivate;
 
@@ -226,7 +232,6 @@ class CVC4_PUBLIC SmtEngine {
   /** how the SMT engine got the answer -- SAT solver or DE */
   BackedStat<std::string> d_statResultSource;
 
-
 public:
 
   /**
@@ -245,6 +250,11 @@ public:
   void setLogic(const std::string& logic) throw(ModalException);
 
   /**
+   * Set the logic of the script.
+   */
+  void setLogic(const LogicInfo& logic) throw(ModalException);
+
+  /**
    * Set information about the script executing.
    */
   void setInfo(const std::string& key, const SExpr& value)
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index eb289937f..4a077450c 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -9,6 +9,8 @@ DIST_SUBDIRS = $(SUBDIRS) example
 noinst_LTLIBRARIES = libtheory.la
 
 libtheory_la_SOURCES = \
+	logic_info.h \
+	logic_info.cpp \
 	output_channel.h \
 	interrupted.h \
 	theory_engine.h \
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
new file mode 100644
index 000000000..ba7119071
--- /dev/null
+++ b/src/theory/logic_info.cpp
@@ -0,0 +1,285 @@
+/*********************                                                        */
+/*! \file logic_info.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009--2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class giving information about a logic (group a theory modules
+ ** and configuration information)
+ **
+ ** A class giving information about a logic (group of theory modules and
+ ** configuration information).
+ **/
+
+#include <string>
+#include <cstring>
+#include <sstream>
+
+#include "expr/kind.h"
+#include "theory/logic_info.h"
+#include "util/Assert.h"
+
+using namespace std;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+
+LogicInfo::LogicInfo() :
+  d_logicString(""),
+  d_theories(),
+  d_sharingTheories(0),
+  d_integers(true),
+  d_reals(true),
+  d_linear(false) {
+
+  for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
+    d_theories[id] = false;// ensure it's cleared
+    enableTheory(id);
+  }
+}
+
+LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
+  d_logicString(""),
+  d_theories(),
+  d_sharingTheories(0),
+  d_integers(false),
+  d_reals(false),
+  d_linear(false) {
+  setLogicString(logicString);
+}
+
+std::string LogicInfo::getLogicString() const {
+  if(d_logicString == "") {
+    size_t seen = 0; // make sure we support all the active theories
+
+    stringstream ss;
+    if(!isQuantified()) {
+      ss << "QF_";
+    }
+    if(d_theories[THEORY_ARRAY]) {
+      ss << (d_sharingTheories == 1 ? "AX" : "A");
+      ++seen;
+    }
+    if(d_theories[THEORY_UF]) {
+      ss << "UF";
+      ++seen;
+    }
+    if(d_theories[THEORY_BV]) {
+      ss << "BV";
+      ++seen;
+    }
+    if(d_theories[THEORY_DATATYPES]) {
+      ss << "DT";
+      ++seen;
+    }
+    if(d_theories[THEORY_ARITH]) {
+      if(isDifferenceLogic()) {
+        ss << (areIntegersUsed() ? "I" : "");
+        ss << (areRealsUsed() ? "R" : "");
+        ss << "DL";
+      } else {
+        ss << (isLinear() ? "L" : "N");
+        ss << (areIntegersUsed() ? "I" : "");
+        ss << (areRealsUsed() ? "R" : "");
+        ss << "A";
+      }
+      ++seen;
+    }
+
+    if(seen != d_sharingTheories) {
+      Unhandled("can't extract a logic string from LogicInfo; at least one "
+                "active theory is unknown to LogicInfo::getLogicString() !");
+    }
+
+    if(seen == 0) {
+      ss << "SAT";
+    }
+
+    d_logicString = ss.str();
+  }
+  return d_logicString;
+}
+
+void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
+  for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
+    d_theories[id] = false;// ensure it's cleared
+  }
+  d_sharingTheories = 0;
+
+  // Below, ONLY use enableTheory()/disableTheory() rather than
+  // accessing d_theories[] directly.  This makes sure to set up
+  // sharing properly.
+
+  enableTheory(THEORY_BUILTIN);
+  enableTheory(THEORY_BOOL);
+
+  const char* p = logicString.c_str();
+  if(!strcmp(p, "QF_SAT") || *p == '\0') {
+    // propositional logic only; we're done.
+    p += 6;
+  } else {
+    if(!strncmp(p, "QF_", 3)) {
+      disableQuantifiers();
+      p += 3;
+    } else {
+      enableQuantifiers();
+    }
+    if(!strncmp(p, "AX", 2)) {
+      enableTheory(THEORY_ARRAY);
+      p += 2;
+    } else {
+      if(*p == 'A') {
+        enableTheory(THEORY_ARRAY);
+        ++p;
+      }
+      if(!strncmp(p, "UF", 2)) {
+        enableTheory(THEORY_UF);
+        p += 2;
+      }
+      if(!strncmp(p, "BV", 2)) {
+        enableTheory(THEORY_BV);
+        p += 2;
+      }
+      if(!strncmp(p, "DT", 2)) {
+        enableTheory(THEORY_DATATYPES);
+        p += 2;
+      }
+      if(!strncmp(p, "IDL", 3)) {
+        enableIntegers();
+        disableReals();
+        arithOnlyDifference();
+        p += 3;
+      } else if(!strncmp(p, "RDL", 3)) {
+        disableIntegers();
+        enableReals();
+        arithOnlyDifference();
+        p += 3;
+      } else if(!strncmp(p, "IRDL", 4)) {
+        // "IRDL" ?! --not very useful, but getLogicString() can produce
+        // that string, so we really had better be able to read it back in.
+        enableIntegers();
+        enableReals();
+        arithOnlyDifference();
+        p += 4;
+      } else if(!strncmp(p, "LIA", 3)) {
+        enableIntegers();
+        disableReals();
+        arithOnlyLinear();
+        p += 3;
+      } else if(!strncmp(p, "LRA", 3)) {
+        disableIntegers();
+        enableReals();
+        arithOnlyLinear();
+        p += 3;
+      } else if(!strncmp(p, "LIRA", 4)) {
+        enableIntegers();
+        enableReals();
+        arithOnlyLinear();
+        p += 4;
+      } else if(!strncmp(p, "NIA", 3)) {
+        enableIntegers();
+        disableReals();
+        arithNonLinear();
+        p += 3;
+      } else if(!strncmp(p, "NRA", 3)) {
+        disableIntegers();
+        enableReals();
+        arithNonLinear();
+        p += 3;
+      } else if(!strncmp(p, "NIRA", 4)) {
+        enableIntegers();
+        enableReals();
+        arithNonLinear();
+        p += 4;
+      }
+    }
+  }
+  if(*p != '\0') {
+    stringstream err;
+    err << "LogicInfo::setLogicString(): junk (\"" << p << "\") at end of logic string: " << logicString;
+    IllegalArgument(logicString, err.str().c_str());
+  }
+
+  // ensure a getLogic() returns the same thing as was set
+  d_logicString = logicString;
+}
+
+void LogicInfo::enableTheory(theory::TheoryId theory) {
+  if(!d_theories[theory]) {
+    if(isTrueTheory(theory)) {
+      ++d_sharingTheories;
+    }
+    d_logicString = "";
+    d_theories[theory] = true;
+  }
+}
+
+void LogicInfo::disableTheory(theory::TheoryId theory) {
+  if(d_theories[theory]) {
+    if(isTrueTheory(theory)) {
+      Assert(d_sharingTheories > 0);
+      --d_sharingTheories;
+    }
+    if(theory == THEORY_BUILTIN ||
+       theory == THEORY_BOOL) {
+      return;
+    }
+    d_logicString = "";
+    d_theories[theory] = false;
+  }
+}
+
+void LogicInfo::enableIntegers() {
+  d_logicString = "";
+  enableTheory(THEORY_ARITH);
+  d_integers = true;
+}
+
+void LogicInfo::disableIntegers() {
+  d_logicString = "";
+  d_integers = false;
+  if(!d_reals) {
+    disableTheory(THEORY_ARITH);
+  }
+}
+
+void LogicInfo::enableReals() {
+  d_logicString = "";
+  enableTheory(THEORY_ARITH);
+  d_reals = true;
+}
+
+void LogicInfo::disableReals() {
+  d_logicString = "";
+  d_reals = false;
+  if(!d_integers) {
+    disableTheory(THEORY_ARITH);
+  }
+}
+
+void LogicInfo::arithOnlyDifference() {
+  d_logicString = "";
+  d_linear = true;
+  d_differenceLogic = true;
+}
+
+void LogicInfo::arithOnlyLinear() {
+  d_logicString = "";
+  d_linear = true;
+  d_differenceLogic = false;
+}
+
+void LogicInfo::arithNonLinear() {
+  d_logicString = "";
+  d_linear = false;
+  d_differenceLogic = false;
+}
+
+}/* CVC4 namespace */
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
new file mode 100644
index 000000000..560b72509
--- /dev/null
+++ b/src/theory/logic_info.h
@@ -0,0 +1,188 @@
+/*********************                                                        */
+/*! \file logic_info.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009--2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class giving information about a logic (group a theory modules
+ ** and configuration information)
+ **
+ ** A class giving information about a logic (group of theory modules and
+ ** configuration information).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LOGIC_INFO_H
+#define __CVC4__LOGIC_INFO_H
+
+#include <string>
+#include "expr/kind.h"
+
+namespace CVC4 {
+
+/**
+ * A LogicInfo instance describes a collection of theory modules and some
+ * basic configuration about them.  Conceptually, it provides a background
+ * context for all operations in CVC4.  Typically, when CVC4's SmtEngine
+ * is created, it is issued a setLogic() command indicating features of the
+ * assertions and queries to follow---for example, whether quantifiers are
+ * used, whether integers or reals (or both) will be used, etc.
+ *
+ * Most places in CVC4 will only ever need to access a const reference to an
+ * instance of this class.  Such an instance is generally set by the SmtEngine
+ * when setLogic() is called.  However, mutating member functions are also
+ * provided by this class so that it can be used as a more general mechanism
+ * (e.g., for communicating to the SmtEngine which theories should be used,
+ * rather than having to provide an SMT-LIB string).
+ */
+class LogicInfo {
+  mutable std::string d_logicString; /**< an SMT-LIB-like logic string */
+  bool d_theories[theory::THEORY_LAST]; /**< set of active theories */
+  size_t d_sharingTheories; /**< count of theories that need sharing */
+
+  // for arithmetic
+  bool d_integers; /**< are integers used in this logic? */
+  bool d_reals; /**< are reals used in this logic? */
+  bool d_linear; /**< linear-only arithmetic in this logic? */
+  bool d_differenceLogic; /**< difference-only arithmetic in this logic? */
+
+  /**
+   * Returns true iff this is a "true" theory (one that must be worried
+   * about for sharing
+   */
+  static inline bool isTrueTheory(theory::TheoryId theory) {
+    switch(theory) {
+    case theory::THEORY_BUILTIN:
+    case theory::THEORY_BOOL:
+    case theory::THEORY_QUANTIFIERS:
+    case theory::THEORY_REWRITERULES:
+      return false;
+    default:
+      return true;
+    }
+  }
+
+public:
+
+  /**
+   * Constructs a LogicInfo for the most general logic (quantifiers, all
+   * background theory modules, ...).
+   */
+  LogicInfo();
+
+  /**
+   * Construct a LogicInfo from an SMT-LIB-like logic string.
+   * Throws an IllegalArgumentException if the logic string cannot
+   * be interpreted.
+   */
+  LogicInfo(std::string logicString) throw(IllegalArgumentException);
+
+  // ACCESSORS
+
+  /**
+   * Get an SMT-LIB-like logic string.  These are only guaranteed to
+   * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
+   * the constructor and no mutating functions were called.
+   */
+  std::string getLogicString() const;
+
+  /** Is sharing enabled for this logic? */
+  bool isSharingEnabled() const { return d_sharingTheories > 1; }
+  /** Is the given theory module active in this logic? */
+  bool isTheoryEnabled(theory::TheoryId theory) const { return d_theories[theory]; }
+
+  /** Is this a quantified logic? */
+  bool isQuantified() const {
+    return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
+  }
+
+  /**
+   * Is this a pure logic (only one "true" background theory).  Quantifiers
+   * can exist in such logics though; to test for quantifier-free purity,
+   * use "isPure(theory) && !isQuantified()".
+   */
+  bool isPure(theory::TheoryId theory) const {
+    // the third conjuct is really just to rule out the misleading case where you ask
+    // isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
+    return isTheoryEnabled(theory) && !isSharingEnabled() &&
+      ( !isTrueTheory(theory) || d_sharingTheories == 1 );
+  }
+
+  // these are for arithmetic
+
+  /** Are integers in this logic? */
+  bool areIntegersUsed() const { return d_integers; }
+  /** Are reals in this logic? */
+  bool areRealsUsed() const { return d_reals; }
+  /** Does this logic only linear arithmetic? */
+  bool isLinear() const { return d_linear || d_differenceLogic; }
+  /** Does this logic only permit difference reasoning? (implies linear) */
+  bool isDifferenceLogic() const { return d_differenceLogic; }
+
+  // MUTATORS
+
+  /**
+   * Initialize the LogicInfo with an SMT-LIB-like logic string.
+   * Throws an IllegalArgumentException if the string can't be
+   * interpreted.
+   */
+  void setLogicString(std::string logicString) throw(IllegalArgumentException);
+
+  /**
+   * Enable the given theory module.
+   */
+  void enableTheory(theory::TheoryId theory);
+
+  /**
+   * Disable the given theory module.  THEORY_BUILTIN and THEORY_BOOL cannot
+   * be disabled (and if given here, the request will be silently ignored).
+   */
+  void disableTheory(theory::TheoryId theory);
+
+  /**
+   * Quantifiers are a special case, since two theory modules handle them.
+   */
+  void enableQuantifiers() {
+    enableTheory(theory::THEORY_QUANTIFIERS);
+    enableTheory(theory::THEORY_REWRITERULES);
+  }
+
+  /**
+   * Quantifiers are a special case, since two theory modules handle them.
+   */
+  void disableQuantifiers() {
+    disableTheory(theory::THEORY_QUANTIFIERS);
+    disableTheory(theory::THEORY_REWRITERULES);
+  }
+
+  // these are for arithmetic
+
+  /** Enable the use of integers in this logic. */
+  void enableIntegers();
+  /** Disable the use of integers in this logic. */
+  void disableIntegers();
+  /** Enable the use of reals in this logic. */
+  void enableReals();
+  /** Disable the use of reals in this logic. */
+  void disableReals();
+  /** Only permit difference arithmetic in this logic. */
+  void arithOnlyDifference();
+  /** Only permit linear arithmetic in this logic. */
+  void arithOnlyLinear();
+  /** Permit nonlinear arithmetic in this logic. */
+  void arithNonLinear();
+
+};/* class LogicInfo */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LOGIC_INFO_H */
+
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 1e7222532..db95edfa0 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -93,7 +93,6 @@ void PreRegisterVisitor::start(TNode node) {
 }
 
 bool PreRegisterVisitor::done(TNode node) {
-  d_engine->markActive(d_theories);
   return d_multipleTheories;
 }
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 2b91da3b2..d0218236d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -27,6 +27,7 @@
 #include "theory/valuation.h"
 #include "theory/substitutions.h"
 #include "theory/output_channel.h"
+#include "theory/logic_info.h"
 #include "context/context.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
@@ -139,6 +140,11 @@ private:
   context::UserContext* d_userContext;
 
   /**
+   * Information about the logic we're operating within.
+   */
+  const LogicInfo* d_logicInfo;
+
+  /**
    * The assertFact() queue.
    *
    * These can not be TNodes as some atoms (such as equalities) are sent
@@ -257,6 +263,10 @@ protected:
     return fact;
   }
 
+  const LogicInfo& getLogicInfo() const {
+    return *d_logicInfo;
+  }
+
   /**
    * The theory that owns the uninterpreted sort.
    */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 46a9f5855..d5616221d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -38,11 +38,12 @@ using namespace CVC4;
 using namespace CVC4::theory;
 
 TheoryEngine::TheoryEngine(context::Context* context,
-                           context::UserContext* userContext)
+                           context::UserContext* userContext,
+                           const LogicInfo& logicInfo)
 : d_propEngine(NULL),
   d_context(context),
   d_userContext(userContext),
-  d_activeTheories(context, 0),
+  d_logicInfo(logicInfo),
   d_notify(*this),
   d_sharedTerms(d_notify, context),
   d_ppCache(),
@@ -110,7 +111,7 @@ void TheoryEngine::check(Theory::Effort effort) {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-    if (theory::TheoryTraits<THEORY>::hasCheck && isActive(THEORY)) { \
+    if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
        reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->check(effort); \
        if (d_inConflict) { \
          break; \
@@ -135,9 +136,9 @@ void TheoryEngine::check(Theory::Effort effort) {
       Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;
 
       if (Debug.isOn("theory::assertions")) {
-        for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++ theoryId) {
+        for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
           Theory* theory = d_theoryTable[theoryId];
-          if (theory && Theory::setContains((TheoryId)theoryId, d_activeTheories)) {
+          if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
             Debug("theory::assertions") << "--------------------------------------------" << std::endl;
             Debug("theory::assertions") << "Assertions of " << theory->getId() << ": " << std::endl;
             context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
@@ -248,7 +249,7 @@ void TheoryEngine::combineTheories() {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::isParametric && isActive(THEORY)) { \
+  if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
      reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->getCareGraph(careGraph); \
   }
 
@@ -309,7 +310,7 @@ void TheoryEngine::propagate(Theory::Effort effort) {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasPropagate && isActive(THEORY)) { \
+  if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
     reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->propagate(effort); \
   }
 
@@ -447,7 +448,7 @@ void TheoryEngine::notifyRestart() {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasNotifyRestart && isActive(THEORY)) { \
+  if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
     reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->notifyRestart(); \
   }
 
@@ -482,7 +483,7 @@ void TheoryEngine::shutdown() {
   d_hasShutDown = true;
 
   // Shutdown all the theories
-  for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
+  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
     if(d_theoryTable[theoryId]) {
       theoryOf(static_cast<TheoryId>(theoryId))->shutdown();
     }
@@ -642,7 +643,6 @@ void TheoryEngine::assertFact(TNode node)
           }
         }
         d_sharedTerms.markNotified(term, theories);
-        markActive(theories);
       }
     }
 
@@ -665,7 +665,7 @@ void TheoryEngine::assertFact(TNode node)
       // TODO: have processSharedLiteral propagate disequalities?
       if (node.getKind() == kind::EQUAL) {
         // Don't have to assert it - this will be taken care of by processSharedLiteral
-        Assert(isActive(theory->getId()));
+        Assert(d_logicInfo.isTheoryEnabled(theory->getId()));
         return;
       }
     }
@@ -678,7 +678,7 @@ void TheoryEngine::assertFact(TNode node)
 
   // Assert the fact to the appropriate theory and mark it active
   theory->assertFact(node, true);
-  markActive(Theory::setInsert(theory->getId()));
+  Assert(d_logicInfo.isTheoryEnabled(theory->getId()));
 }
 
 void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index faa6bbd26..5dfc4c36c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -90,13 +90,13 @@ class TheoryEngine {
   theory::Theory* d_theoryTable[theory::THEORY_LAST];
 
   /**
-   * A bitmap of theories that are "active" for the current run.  We
-   * mark a theory active when we first see a term or type belonging to
-   * it.  This is important because we can optimize for single-theory
-   * runs (no sharing), can reduce the cost of walking the DAG on
-   * registration, etc.
+   * 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.
    */
-  context::CDO<theory::Theory::Set> d_activeTheories;
+  const LogicInfo& d_logicInfo;
 
   // NotifyClass: template helper class for Shared Terms Database
   class NotifyClass :public SharedTermsDatabase::SharedTermsNotifyClass {
@@ -309,13 +309,6 @@ class TheoryEngine {
     d_propEngine->spendResource();
   }
 
-  /**
-   * Is the theory active.
-   */
-  bool isActive(theory::TheoryId theory) {
-    return theory::Theory::setContains(theory, d_activeTheories);
-  }
-
   struct SharedLiteral {
     /** The node/theory pair for the assertion */
     /** THEORY_LAST indicates this is a SAT literal and should be sent to the SAT solver */
@@ -469,7 +462,7 @@ class TheoryEngine {
 public:
 
   /** Constructs a theory engine */
-  TheoryEngine(context::Context* context, context::UserContext* userContext);
+  TheoryEngine(context::Context* context, context::UserContext* userContext, const LogicInfo& logic);
 
   /** Destroys a theory engine */
   ~TheoryEngine();
@@ -483,6 +476,7 @@ public:
     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_theoryTable[theoryId]->d_logicInfo = &d_logicInfo;
   }
 
   /**
@@ -491,13 +485,6 @@ public:
    */
   void setLogic(std::string logic);
 
-  /**
-   * Mark a theory active if it's not already.
-   */
-  void markActive(theory::Theory::Set theories) {
-    d_activeTheories = theory::Theory::setUnion(d_activeTheories, theories);
-  }
-
   inline void setPropEngine(prop::PropEngine* propEngine) {
     Assert(d_propEngine == NULL);
     d_propEngine = propEngine;