Weekend work. The main points:

* Type::getCardinality() returns the cardinality for for all types.
  Theories give a cardinality in the their kinds file.  For
  cardinalities that depend on a type argument, a "cardinality
  computer" function is named in the kinds file, which takes a
  TypeNode and returns its cardinality.

* There's a bitmap for the set of "active theories" in the
  TheoryEngine.  Theories become "active" when a term that is owned by
  them, or whose type is owned by them, is pre-registered (run CVC4
  with --verbose to see theory activation).  Non-active theories don't
  get any calls for check() or propagate() or anything, and if we're
  running in single-theory mode, the shared term manager doesn't have
  to get involved.  This is really important for get() performance
  (which can only skimp on walking the entire sub-DAG only if the
  theory doesn't require it AND the shared term manager doesn't
  require it).

* TheoryEngine now does not call presolve(), registerTerm(),
  notifyRestart(), etc., on a Theory if that theory doesn't declare
  that property in its kinds file.  To avoid coding errors,
  mktheorytraits greps the theory header and gives warnings if:
  + the theory appears to declare one of the functions (check,
    propagate, etc.) that isn't listed among its kinds file properties
    (but probably should be)
  + the theory appears NOT to declare one of the functions listed in
    its kinds file properties

* some bounded token stream work

1 files changed, 53 insertions, 20 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d37916515..b4d6654b1 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -117,7 +117,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
        * twice. */
       // FIXME when ExprSets are online, use one of those to avoid
       // duplicates in the above?
-      // Actually, that doesn't work because you have to make sure 
+      // Actually, that doesn't work because you have to make sure
       // that the *last* occurrence is the one that gets processed first @CB
       // This could be a big performance problem though because it requires
       // traversing a DAG as a tree and that can really blow up @CB
@@ -132,6 +132,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
 TheoryEngine::TheoryEngine(context::Context* ctxt) :
   d_propEngine(NULL),
   d_context(ctxt),
+  d_activeTheories(0),
   d_theoryOut(this, ctxt),
   d_hasShutDown(false),
   d_incomplete(ctxt, false),
@@ -139,6 +140,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) :
 
   for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
     d_theoryTable[theoryId] = NULL;
+    d_theoryIsActive[theoryId] = false;
   }
 
   Rewriter::init();
@@ -150,7 +152,7 @@ TheoryEngine::~TheoryEngine() {
   Assert(d_hasShutDown);
 
   for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
-    if(d_theoryTable[theoryId]) {
+    if(d_theoryTable[theoryId] != NULL) {
       delete d_theoryTable[theoryId];
     }
   }
@@ -163,7 +165,7 @@ struct preprocess_stack_element {
   bool children_added;
   preprocess_stack_element(TNode node)
   : node(node), children_added(false) {}
-};
+};/* struct preprocess_stack_element */
 
 Node TheoryEngine::preprocess(TNode node) {
   // Make sure the node is type-checked first (some rewrites depend on
@@ -198,24 +200,29 @@ void TheoryEngine::preRegister(TNode preprocessed) {
         if (current.getKind() == kind::EQUAL) {
           TheoryId theoryLHS = Theory::theoryOf(current[0]);
           Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl;
+          markActive(theoryLHS);
           d_theoryTable[theoryLHS]->preRegisterTerm(current);
 //          TheoryId theoryRHS = Theory::theoryOf(current[1]);
 //          if (theoryLHS != theoryRHS) {
+//            markActive(theoryRHS);
 //            d_theoryTable[theoryRHS]->preRegisterTerm(current);
 //            Debug("register") << "preregistering " << current << " with " << theoryRHS << std::endl;
 //          }
 //          TheoryId typeTheory = Theory::theoryOf(current[0].getType());
 //          if (typeTheory != theoryLHS && typeTheory != theoryRHS) {
+//            markActive(typeTheory);
 //            d_theoryTable[typeTheory]->preRegisterTerm(current);
 //            Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl;
 //          }
         } else {
           TheoryId theory = Theory::theoryOf(current);
           Debug("register") << "preregistering " << current << " with " << theory << std::endl;
+          markActive(theory);
           d_theoryTable[theory]->preRegisterTerm(current);
           TheoryId typeTheory = Theory::theoryOf(current.getType());
           if (theory != typeTheory) {
             Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl;
+            markActive(typeTheory);
             d_theoryTable[typeTheory]->preRegisterTerm(current);
           }
         }
@@ -248,7 +255,7 @@ bool TheoryEngine::check(theory::Theory::Effort effort) {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasCheck) { \
+  if (theory::TheoryTraits<THEORY>::hasCheck && d_theoryIsActive[THEORY]) { \
      reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \
      if (!d_theoryOut.d_conflictNode.get().isNull()) { \
        return false; \
@@ -271,7 +278,7 @@ void TheoryEngine::propagate() {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasPropagate) { \
+  if (theory::TheoryTraits<THEORY>::hasPropagate && d_theoryIsActive[THEORY]) { \
       reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \
   }
 
@@ -359,13 +366,22 @@ Node TheoryEngine::getValue(TNode node) {
 bool TheoryEngine::presolve() {
   d_theoryOut.d_conflictNode = Node::null();
   d_theoryOut.d_propagatedLiterals.clear();
+
   try {
-    for(unsigned i = 0; i < THEORY_LAST; ++ i) {
-        d_theoryTable[i]->presolve();
-        if(!d_theoryOut.d_conflictNode.get().isNull()) {
-          return true;
-	}
-     }
+    // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+    if (theory::TheoryTraits<THEORY>::hasPresolve && d_theoryIsActive[THEORY]) { \
+      reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \
+      if(!d_theoryOut.d_conflictNode.get().isNull()) { \
+        return true; \
+      } \
+    }
+
+    // Presolve for each theory using the statement above
+    CVC4_FOR_EACH_THEORY
   } catch(const theory::Interrupted&) {
     Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl;
   }
@@ -375,20 +391,37 @@ bool TheoryEngine::presolve() {
 
 
 void TheoryEngine::notifyRestart() {
-  for(unsigned i = 0; i < THEORY_LAST; ++ i) {
-    if (d_theoryTable[i]) {
-      d_theoryTable[i]->notifyRestart();
-    }
+  // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+  if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_theoryIsActive[THEORY]) { \
+    reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->notifyRestart(); \
   }
-}
 
+  // notify each theory using the statement above
+  CVC4_FOR_EACH_THEORY
+}
 
 void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
-  for(unsigned i = 0; i < THEORY_LAST; ++ i) {
-    if (d_theoryTable[i]) {
-      d_theoryTable[i]->staticLearning(in, learned);
-    }
+  // NOTE that we don't look at d_theoryIsActive[] here.  First of
+  // all, we haven't done any pre-registration yet, so we don't know
+  // which theories are active.  Second, let's give each theory a shot
+  // at doing something with the input formula, even if it wouldn't
+  // otherwise be active.
+
+  // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+  if (theory::TheoryTraits<THEORY>::hasStaticLearning) { \
+    reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->staticLearning(in, learned); \
   }
+
+  // notify each theory using the statement above
+  CVC4_FOR_EACH_THEORY
 }