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

2 files changed, 2 insertions, 11 deletions

diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index 25ca1cfe3..ce7c9111a 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -6,11 +6,11 @@
 
 theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h"
 
-properties finite  
+properties finite
 
 rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h"
 
-sort BOOLEAN_TYPE "Boolean type"
+sort BOOLEAN_TYPE 2 "Boolean type"
 
 constant CONST_BOOLEAN \
     bool \
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index dfcdd22b8..fd6d20e03 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -34,15 +34,6 @@ public:
     Theory(THEORY_BOOL, c, out, valuation) {
   }
 
-  void preRegisterTerm(TNode n) {
-    Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl;
-    Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
-  }
-  void registerTerm(TNode n) {
-    Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl;
-    Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
-  }
-
   Node getValue(TNode n);
 
   std::string identify() const { return std::string("TheoryBool"); }