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, 6 insertions, 8 deletions

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 8c34370d7..0b377fb11 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -11,17 +11,13 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief Common utilities for testing theories
  **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** Common utilities for testing theories.
  **/
 
-
-
 #include "cvc4_public.h"
 
-
 #ifndef __CVC4__THEORY__THEORY_TEST_UTILS_H
 #define __CVC4__THEORY__ITHEORY_TEST_UTILS_H
 
@@ -48,7 +44,7 @@ enum OutputChannelCallType {
   AUG_LEMMA,
   LEMMA,
   EXPLANATION
-};
+};/* enum OutputChannelCallType */
 
 }/* CVC4::theory namespace */
 
@@ -121,9 +117,11 @@ public:
   }
 
 private:
+
   void push(OutputChannelCallType call, TNode n) {
-    d_callHistory.push_back(std::make_pair(call,n));
+    d_callHistory.push_back(std::make_pair(call, n));
   }
+
 };/* class TestOutputChannel */
 
 }/* CVC4::theory namespace */