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, 54 insertions, 16 deletions

diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index a53da2022..78fc39984 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -35,16 +35,16 @@ me=$(basename "$0")
 
 template=$1; shift
 
-rewriter_includes= 
+rewriter_includes=
 rewrite_init=
 rewrite_shutdown=
 
-pre_rewrite_calls= 
-pre_rewrite_get_cache= 
+pre_rewrite_calls=
+pre_rewrite_get_cache=
 pre_rewrite_set_cache=
 
 post_rewrite_calls=
-post_rewrite_get_cache= 
+post_rewrite_get_cache=
 post_rewrite_set_cache=
 
 seen_theory=false
@@ -55,6 +55,11 @@ function theory {
 
   lineno=${BASH_LINENO[0]}
 
+  if $seen_theory; then
+    echo "$kf:$lineno: theory declaration can only appear once" >&2
+    exit 1;
+  fi
+
   # this script doesn't care about the theory class information, but
   # makes does make sure it's there
   seen_theory=true
@@ -72,8 +77,8 @@ function theory {
   elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
     echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
   fi
-  
-  theory_id="$1"  
+
+  theory_id="$1"
 }
 
 function properties {
@@ -86,32 +91,33 @@ function endtheory {
   # endtheory
   lineno=${BASH_LINENO[0]}
   check_theory_seen
+  seen_endtheory=true
 }
 
 function rewriter {
   # rewriter class header
-  class="$1" 
+  class="$1"
   header="$2"
 
   rewriter_includes="${rewriter_includes}#include \"$header\"
 "
   rewrite_init="${rewrite_init}   ${class}::init();
 "
-  rewrite_shutdown="${rewrite_shutdown}    ${class}::shutdown(); 
+  rewrite_shutdown="${rewrite_shutdown}    ${class}::shutdown();
 "
 
   pre_rewrite_calls="${pre_rewrite_calls}    case ${theory_id}: return ${class}::preRewrite(node);
 "
-  pre_rewrite_get_cache="${pre_rewrite_get_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node); 
+  pre_rewrite_get_cache="${pre_rewrite_get_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node);
 "
-  pre_rewrite_set_cache="${pre_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache); 
+  pre_rewrite_set_cache="${pre_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache);
 "
 
   post_rewrite_calls="${post_rewrite_calls}    case ${theory_id}: return ${class}::postRewrite(node);
 "
-  post_rewrite_get_cache="${post_rewrite_get_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node); 
-" 
-  post_rewrite_set_cache="${post_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache); 
+  post_rewrite_get_cache="${post_rewrite_get_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node);
+"
+  post_rewrite_set_cache="${post_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache);
 "
 
   lineno=${BASH_LINENO[0]}
@@ -119,7 +125,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
 }
@@ -149,6 +161,10 @@ function constant {
 }
 
 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
@@ -164,17 +180,39 @@ 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 rewriter_includes pre_rewrite_calls post_rewrite_calls pre_rewrite_get_cache post_rewrite_get_cache pre_rewrite_set_cache post_rewrite_set_cache rewrite_init rewrite_shutdown; do
+for var in \
+    rewriter_includes \
+    pre_rewrite_calls \
+    post_rewrite_calls \
+    pre_rewrite_get_cache \
+    post_rewrite_get_cache \
+    pre_rewrite_set_cache \
+    post_rewrite_set_cache \
+    rewrite_init rewrite_shutdown \
+    template \
+    ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
 error=`expr "$text" : '.*\${\([^}]*\)}.*'`