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

12 files changed, 267 insertions, 19 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 1d7af717b..4ed5a3ac7 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -31,6 +31,7 @@ libexpr_la_SOURCES = \
 nodist_libexpr_la_SOURCES = \
 	kind.h \
 	metakind.h \
+	type_properties.h \
 	expr.h \
 	expr.cpp \
 	expr_manager.h \
@@ -39,6 +40,7 @@ nodist_libexpr_la_SOURCES = \
 EXTRA_DIST = \
 	kind_template.h \
 	metakind_template.h \
+	type_properties_template.h \
 	expr_manager_template.h \
 	expr_manager_template.cpp \
 	expr_template.h \
@@ -50,6 +52,7 @@ EXTRA_DIST = \
 BUILT_SOURCES = \
 	kind.h \
 	metakind.h \
+	type_properties.h \
 	expr.h \
 	expr.cpp \
 	expr_manager.h \
@@ -83,6 +86,14 @@ metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @t
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
+type_properties.h: type_properties_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+	$(AM_V_at)chmod +x @srcdir@/mkkind
+	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
+	$(AM_V_GEN)(@srcdir@/mkkind \
+		$< \
+		`cat @top_builddir@/src/theory/.subdirs` \
+	> $@) || (rm -f $@ && exit 1)
+
 expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkexpr
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index b7f376811..f395d781c 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -278,7 +278,6 @@ public:
    */
   Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
 
-
   /** Make a function type from domain to range. */
   FunctionType mkFunctionType(Type domain, Type range);
 
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 24cb6dc5d..43d40105e 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -758,7 +758,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 758 "${template}"
+#line 762 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 6b9787f6c..724f7413f 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Template for the Node kind header.
+ ** \brief Template for the Node kind header
  **
  ** Template for the Node kind header.
  **/
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index da2847d84..a7302da26 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -104,10 +104,17 @@ function endtheory {
   # endtheory
   lineno=${BASH_LINENO[0]}
   check_theory_seen
+  seen_endtheory=true
 }
 
 function sort {
-  # sort TYPE ["comment"]
+  # sort TYPE cardinality ["comment"]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function cardinality {
+  # cardinality TYPE cardinality-computer [header]
   lineno=${BASH_LINENO[0]}
   check_theory_seen
 }
@@ -164,6 +171,10 @@ template <> $2 const & Expr::getConst() const {
 }
 
 function check_theory_seen {
+  if $seen_endtheory; then
+    echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
+    exit 1
+  fi
   if ! $seen_theory; then
     echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
     exit 1
@@ -179,15 +190,27 @@ function check_builtin_theory_seen {
 while [ $# -gt 0 ]; do
   kf=$1
   seen_theory=false
+  seen_endtheory=false
   b=$(basename $(dirname "$kf"))
   source "$kf"
-  check_theory_seen
+  if ! $seen_theory; then
+    echo "$kf: error: no theory content found in file!" >&2
+    exit 1
+  fi
+  if ! $seen_endtheory; then
+    echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
+    exit 1
+  fi
   shift
 done
 check_builtin_theory_seen
 
 ## output
 
+# generate warnings about incorrect #line annotations in templates
+nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
+  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
+
 text=$(cat "$template")
 for var in \
     includes \
@@ -195,7 +218,8 @@ for var in \
     getConst_instantiations \
     getConst_implementations \
     mkConst_instantiations \
-    mkConst_implementations; do
+    mkConst_implementations \
+    ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
 error=`expr "$text" : '.*\${\([^}]*\)}.*'`
diff --git a/src/expr/mkkind b/src/expr/mkkind
index fa80894b2..08d874c79 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -4,8 +4,8 @@
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
 # Copyright (c) 2010-2011  The CVC4 Project
 #
-# The purpose of this script is to create kind.h from a template and a
-# list of theory kinds.
+# The purpose of this script is to create kind.h (and also
+# type_properties.h) from a template and a list of theory kinds.
 #
 # Invocation:
 #
@@ -16,9 +16,11 @@
 
 copyright=2010-2011
 
+filename=`basename "$1" | sed 's,_template,,'`
+
 cat <<EOF
 /*********************                                                        */
-/** kind.h
+/** $filename
  **
  ** Copyright $copyright  The AcSys Group, New York University, and as below.
  **
@@ -29,6 +31,23 @@ cat <<EOF
  ** for the CVC4 project.
  **/
 
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* Edit the template file instead:                     */
+/* $1 */
+
 EOF
 
 me=$(basename "$0")
@@ -42,6 +61,9 @@ kind_to_theory_id=
 type_constant_descriptions=
 type_constant_list=
 type_constant_to_theory_id=
+type_cardinalities=
+type_constant_cardinalities=
+type_cardinalities_includes=
 
 seen_theory=false
 seen_theory_builtin=false
@@ -89,6 +111,7 @@ function endtheory {
   # endtheory
   lineno=${BASH_LINENO[0]}
   check_theory_seen
+  seen_endtheory=true
 }
 
 function rewriter {
@@ -98,10 +121,17 @@ function rewriter {
 }
 
 function sort {
-  # sort TYPE ["comment"]
+  # sort TYPE cardinality ["comment"]
   lineno=${BASH_LINENO[0]}
   check_theory_seen
-  register_sort "$1" "$2"
+  register_sort "$1" "$2" "$3"
+}
+
+function cardinality {
+  # cardinality TYPE cardinality-computer [header]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  register_cardinality "$1" "$2" "$3"
 }
 
 function variable {
@@ -142,14 +172,33 @@ function constant {
 
 function register_sort {
   id=$1
-  comment=$2
+  cardinality=$2
+  comment=$3
 
   type_constant_list="${type_constant_list}  ${id}, /**< ${comment} */
 "
   type_constant_descriptions="${type_constant_descriptions}  case $id:  out << \"${comment}\"; break;
 "
-  type_constant_to_theory_id="${type_constant_to_theory_id}  case $id: return $theory_id; break;
+  type_constant_to_theory_id="${type_constant_to_theory_id}  case $id: return $theory_id;
+"
+  type_constant_cardinalities="${type_constant_cardinalities}#line $lineno \"$kf\"
+  case $id: return Cardinality($cardinality);
+"
+}
+
+function register_cardinality {
+  id=$1
+  cardinality_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$2")
+  header=$3
+
+  type_cardinalities="${type_cardinalities}#line $lineno \"$kf\"
+  case $id: return $cardinality_computer;
+"
+  if [ -n "$header" ]; then
+    type_cardinalities_includes="${type_cardinalities_includes}#line $lineno \"$kf\"
+#include \"$header\"
 "
+  fi
 }
 
 function register_kind {
@@ -161,11 +210,15 @@ function register_kind {
 "
   kind_printers="${kind_printers}  case $r: out << \"$r\"; break;
 "
-  kind_to_theory_id="${kind_to_theory_id}  case kind::$r: return $theory_id; break;
+  kind_to_theory_id="${kind_to_theory_id}  case kind::$r: return $theory_id;
 "
 }
 
 function check_theory_seen {
+  if $seen_endtheory; then
+    echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
+    exit 1
+  fi
   if ! $seen_theory; then
     echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
     exit 1
@@ -181,6 +234,7 @@ function check_builtin_theory_seen {
 while [ $# -gt 0 ]; do
   kf=$1
   seen_theory=false
+  seen_endtheory=false
   b=$(basename $(dirname "$kf"))
   kind_decls="${kind_decls}
   /* from $b */
@@ -189,15 +243,39 @@ while [ $# -gt 0 ]; do
   /* from $b */
 "
   source "$kf"
-  check_theory_seen
+  if ! $seen_theory; then
+    echo "$kf: error: no theory content found in file!" >&2
+    exit 1
+  fi
+  if ! $seen_endtheory; then
+    echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
+    exit 1
+  fi
   shift
 done
 check_builtin_theory_seen
 
 ## output
 
+# generate warnings about incorrect #line annotations in templates
+nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
+  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
+
 text=$(cat "$template")
-for var in kind_decls kind_printers kind_to_theory_id theory_enum type_constant_list type_constant_descriptions type_constant_to_theory_id theory_descriptions; do
+for var in \
+    kind_decls \
+    kind_printers \
+    kind_to_theory_id \
+    theory_enum \
+    type_constant_list \
+    type_constant_descriptions \
+    type_constant_to_theory_id \
+    type_cardinalities \
+    type_constant_cardinalities \
+    type_cardinalities_includes \
+    theory_descriptions \
+    template \
+    ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
 error=`expr "$text" : '.*\${\([^}]*\)}.*'`
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 7f9037c1c..00599c5a0 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -90,6 +90,7 @@ function endtheory {
   # endtheory
   lineno=${BASH_LINENO[0]}
   check_theory_seen
+  seen_endtheory=true
 }
 
 function rewriter {
@@ -99,7 +100,13 @@ function rewriter {
 }
 
 function sort {
-  # sort TYPE ["comment"]
+  # sort TYPE cardinality ["comment"]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
+function cardinality {
+  # cardinality TYPE cardinality-computer [header]
   lineno=${BASH_LINENO[0]}
   check_theory_seen
 }
@@ -287,6 +294,10 @@ function primitive_type {
 }
 
 function check_theory_seen {
+  if $seen_endtheory; then
+    echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
+    exit 1
+  fi
   if ! $seen_theory; then
     echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
     exit 1
@@ -302,6 +313,7 @@ function check_builtin_theory_seen {
 while [ $# -gt 0 ]; do
   kf=$1
   seen_theory=false
+  seen_endtheory=false
   b=$(basename $(dirname "$kf"))
   metakind_kinds="${metakind_kinds}
     /* from $b */
@@ -310,13 +322,24 @@ while [ $# -gt 0 ]; do
     /* from $b */
 "
   source "$kf"
-  check_theory_seen
+  if ! $seen_theory; then
+    echo "$kf: error: no theory content found in file!" >&2
+    exit 1
+  fi
+  if ! $seen_endtheory; then
+    echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
+    exit 1
+  fi
   shift
 done
 check_builtin_theory_seen
 
 ## output
 
+# generate warnings about incorrect #line annotations in templates
+nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
+  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
+
 text=$(cat "$template")
 for var in \
     metakind_includes \
@@ -328,7 +351,9 @@ for var in \
     metakind_constDeleters \
     metakind_ubchildren \
     metakind_lbchildren \
-    metakind_operatorKinds; do
+    metakind_operatorKinds \
+    template \
+    ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
 error=`expr "$text" : '.*\${\([^}]*\)}.*'`
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 4ea425aa7..27a3f9da7 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -68,6 +68,11 @@ bool Type::isNull() const {
   return d_typeNode->isNull();
 }
 
+Cardinality Type::getCardinality() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getCardinality();
+}
+
 Type& Type::operator=(const Type& t) {
   Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!");
   Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!");
diff --git a/src/expr/type.h b/src/expr/type.h
index 290bb360a..89cb994e7 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -27,6 +27,7 @@
 #include <stdint.h>
 
 #include "util/Assert.h"
+#include "util/cardinality.h"
 
 namespace CVC4 {
 
@@ -137,6 +138,11 @@ public:
   bool isNull() const;
 
   /**
+   * Return the cardinality of this type.
+   */
+  Cardinality getCardinality() const;
+
+  /**
    * Substitution of Types.
    */
   Type substitute(const Type& type, const Type& replacement) const;
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 0b22fdf0f..e48a92321 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -19,6 +19,7 @@
 #include <vector>
 
 #include "expr/type_node.h"
+#include "expr/type_properties.h"
 
 using namespace std;
 
@@ -46,6 +47,10 @@ TypeNode TypeNode::substitute(const TypeNode& type,
   return nb.constructTypeNode();
 }
 
+Cardinality TypeNode::getCardinality() const {
+  return kind::getCardinality(*this);
+}
+
 bool TypeNode::isBoolean() const {
   return getKind() == kind::TYPE_CONSTANT &&
     getConst<TypeConstant>() == BOOLEAN_TYPE;
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index c04bef0c7..f51d7a9ba 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -32,6 +32,7 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "util/Assert.h"
+#include "util/cardinality.h"
 
 namespace CVC4 {
 
@@ -342,6 +343,13 @@ public:
     return d_nv == &expr::NodeValue::s_null;
   }
 
+  /**
+   * Returns the cardinality of this type.
+   *
+   * @return a finite or infinite cardinality
+   */
+  Cardinality getCardinality() const;
+
   /** Is this the Boolean type? */
   bool isBoolean() const;
 
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
new file mode 100644
index 000000000..b6fd644c8
--- /dev/null
+++ b/src/expr/type_properties_template.h
@@ -0,0 +1,87 @@
+/*********************                                                        */
+/*! \file type_properties_template.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, 2010, 2011  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 Template for the Type properties header
+ **
+ ** Template for the Type properties header.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__TYPE_PROPERTIES_H
+#define __CVC4__TYPE_PROPERTIES_H
+
+#line 25 "${template}"
+
+#include "expr/type_node.h"
+#include "util/Assert.h"
+#include "expr/kind.h"
+#include "expr/expr.h"
+#include "util/language.h"
+
+#include <sstream>
+
+${type_cardinalities_includes}
+
+#line 37 "${template}"
+
+namespace CVC4 {
+namespace kind {
+
+/**
+ * Return the cardinality of the type constant represented by the
+ * TypeConstant argument.  This function is auto-generated from Theory
+ * "kinds" files, so includes contributions from each theory regarding
+ * that theory's types.
+ */
+inline Cardinality getCardinality(TypeConstant tc) {
+  switch(tc) {
+${type_constant_cardinalities}
+#line 51 "${template}"
+  default: {
+    std::stringstream ss;
+    ss << "No cardinality known for type constant " << tc;
+    InternalError(ss.str());
+  }
+  }
+}/* getCardinality(TypeConstant) */
+
+/**
+ * Return the cardinality of the type represented by the TypeNode
+ * argument.  This function is auto-generated from Theory "kinds"
+ * files, so includes contributions from each theory regarding that
+ * theory's types.
+ */
+inline Cardinality getCardinality(TypeNode typeNode) {
+  AssertArgument(!typeNode.isNull(), typeNode);
+  switch(Kind k = typeNode.getKind()) {
+  case TYPE_CONSTANT:
+    return getCardinality(typeNode.getConst<TypeConstant>());
+${type_cardinalities}
+#line 72 "${template}"
+  default: {
+    std::stringstream ss;
+    ss << Expr::setlanguage(language::toOutputLanguage
+                            ( Options::current()->inputLanguage ));
+    ss << "A theory kinds file did not provide a cardinality "
+       << "or cardinality computer for type:\n" << typeNode
+       << "\nof kind " << k;
+    InternalError(ss.str());
+  }
+  }
+}/* getCardinality(TypeNode) */
+
+}/* CVC4::kind namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__TYPE_PROPERTIES_H */