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

3 files changed, 269 insertions, 2 deletions

diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h
new file mode 100644
index 000000000..5927e1bfa
--- /dev/null
+++ b/test/unit/util/cardinality_public.h
@@ -0,0 +1,255 @@
+/*********************                                                        */
+/*! \file cardinality_public.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 Public-box testing of CVC4::Cardinality
+ **
+ ** Public-box testing of CVC4::Cardinality.
+ **/
+
+#include "util/cardinality.h"
+#include "util/integer.h"
+
+#include <string>
+#include <sstream>
+
+using namespace CVC4;
+using namespace std;
+
+class CardinalityPublic : public CxxTest::TestSuite {
+  stringstream ss;
+
+public:
+
+  void testCardinalities() {
+    Cardinality zero(0);
+    Cardinality one(1);
+    Cardinality two(2);
+
+    Cardinality invalid(0);
+    TS_ASSERT_THROWS( invalid = Cardinality(-1), IllegalArgumentException);
+    TS_ASSERT_THROWS( invalid = Cardinality(-2), IllegalArgumentException);
+    TS_ASSERT_THROWS( invalid = Cardinality(Integer("-3983982192391747295721957")), IllegalArgumentException);
+    invalid = one; // test assignment
+    invalid = Cardinality(5); // test assignment to temporary
+
+    Cardinality copy(one); // test copy
+    Cardinality big(Integer("3983982192391747295721957"));
+    Cardinality r(Cardinality::REALS);
+    Cardinality i(Cardinality::INTEGERS);
+
+    TS_ASSERT( zero < one );
+    TS_ASSERT( one < two );
+    TS_ASSERT( two < invalid );
+    TS_ASSERT( invalid < big );
+    TS_ASSERT( big < i );
+    TS_ASSERT( i < r );
+
+    TS_ASSERT( zero <= one );
+    TS_ASSERT( zero <= zero );
+    TS_ASSERT( one <= two );
+    TS_ASSERT( one <= one );
+    TS_ASSERT( two <= invalid );
+    TS_ASSERT( two <= two );
+    TS_ASSERT( invalid <= big );
+    TS_ASSERT( invalid <= invalid );
+    TS_ASSERT( big <= i );
+    TS_ASSERT( big <= big );
+    TS_ASSERT( i <= r );
+    TS_ASSERT( i <= i );
+    TS_ASSERT( r <= r );
+
+    TS_ASSERT( zero == zero );
+    TS_ASSERT( one == one );
+    TS_ASSERT( two == two );
+    TS_ASSERT( invalid == invalid );
+    TS_ASSERT( copy == copy );
+    TS_ASSERT( copy == one );
+    TS_ASSERT( one == copy );
+    TS_ASSERT( big == big );
+    TS_ASSERT( i == i );
+    TS_ASSERT( r == r );
+
+    TS_ASSERT( zero != one );
+    TS_ASSERT( one != two );
+    TS_ASSERT( two != invalid );
+    TS_ASSERT( copy != r );
+    TS_ASSERT( copy != i );
+    TS_ASSERT( big != i );
+    TS_ASSERT( i != big );
+    TS_ASSERT( big != zero );
+    TS_ASSERT( r != i );
+    TS_ASSERT( i != r );
+
+    TS_ASSERT( r > zero );
+    TS_ASSERT( r > one );
+    TS_ASSERT( r > two );
+    TS_ASSERT( r > copy );
+    TS_ASSERT( r > invalid );
+    TS_ASSERT( r > big );
+    TS_ASSERT( r > i );
+    TS_ASSERT( !( r > r ) );
+    TS_ASSERT( r >= r );
+
+    TS_ASSERT( zero.isFinite() );
+    TS_ASSERT( one.isFinite() );
+    TS_ASSERT( two.isFinite() );
+    TS_ASSERT( copy.isFinite() );
+    TS_ASSERT( invalid.isFinite() );
+    TS_ASSERT( big.isFinite() );
+    TS_ASSERT( !i.isFinite() );
+    TS_ASSERT( !r.isFinite() );
+
+    TS_ASSERT( zero.getFiniteCardinality() == 0 );
+    TS_ASSERT( one.getFiniteCardinality() == 1 );
+    TS_ASSERT( two.getFiniteCardinality() == 2 );
+    TS_ASSERT( copy.getFiniteCardinality() == 1 );
+    TS_ASSERT( invalid.getFiniteCardinality() == 5 );
+    TS_ASSERT( big.getFiniteCardinality() == Integer("3983982192391747295721957") );
+    TS_ASSERT_THROWS( i.getFiniteCardinality(), IllegalArgumentException );
+    TS_ASSERT_THROWS( r.getFiniteCardinality(), IllegalArgumentException );
+
+    TS_ASSERT_THROWS( zero.getBethNumber(), IllegalArgumentException );
+    TS_ASSERT_THROWS( one.getBethNumber(), IllegalArgumentException );
+    TS_ASSERT_THROWS( two.getBethNumber(), IllegalArgumentException );
+    TS_ASSERT_THROWS( copy.getBethNumber(), IllegalArgumentException );
+    TS_ASSERT_THROWS( invalid.getBethNumber(), IllegalArgumentException );
+    TS_ASSERT_THROWS( big.getBethNumber(), IllegalArgumentException );
+    TS_ASSERT( i.getBethNumber() == 0 );
+    TS_ASSERT( r.getBethNumber() == 1 );
+
+    TS_ASSERT( zero != Cardinality::INTEGERS );
+    TS_ASSERT( one != Cardinality::INTEGERS );
+    TS_ASSERT( two != Cardinality::INTEGERS );
+    TS_ASSERT( copy != Cardinality::INTEGERS );
+    TS_ASSERT( invalid != Cardinality::INTEGERS );
+    TS_ASSERT( big != Cardinality::INTEGERS );
+    TS_ASSERT( r != Cardinality::INTEGERS );
+    TS_ASSERT( i == Cardinality::INTEGERS );
+
+    TS_ASSERT( zero != Cardinality::REALS );
+    TS_ASSERT( one != Cardinality::REALS );
+    TS_ASSERT( two != Cardinality::REALS );
+    TS_ASSERT( copy != Cardinality::REALS );
+    TS_ASSERT( invalid != Cardinality::REALS );
+    TS_ASSERT( big != Cardinality::REALS );
+    TS_ASSERT( i != Cardinality::REALS );
+    TS_ASSERT( r == Cardinality::REALS );
+
+    // should work the other way too
+
+    TS_ASSERT( Cardinality::INTEGERS != zero );
+    TS_ASSERT( Cardinality::INTEGERS != one );
+    TS_ASSERT( Cardinality::INTEGERS != two );
+    TS_ASSERT( Cardinality::INTEGERS != copy );
+    TS_ASSERT( Cardinality::INTEGERS != invalid );
+    TS_ASSERT( Cardinality::INTEGERS != big );
+    TS_ASSERT( Cardinality::INTEGERS != r );
+    TS_ASSERT( Cardinality::INTEGERS == i );
+
+    TS_ASSERT( Cardinality::REALS != zero );
+    TS_ASSERT( Cardinality::REALS != one );
+    TS_ASSERT( Cardinality::REALS != two );
+    TS_ASSERT( Cardinality::REALS != copy );
+    TS_ASSERT( Cardinality::REALS != invalid );
+    TS_ASSERT( Cardinality::REALS != big );
+    TS_ASSERT( Cardinality::REALS != i );
+    TS_ASSERT( Cardinality::REALS == r );
+
+    // finite cardinal arithmetic
+
+    TS_ASSERT( zero + zero == zero );
+    TS_ASSERT( zero * zero == zero );
+    TS_ASSERT( (zero ^ zero) == one );
+    TS_ASSERT( zero + one == one );
+    TS_ASSERT( zero * one == zero );
+    TS_ASSERT( (zero ^ one) == zero );
+    TS_ASSERT( one + zero == one );
+    TS_ASSERT( one * zero == zero );
+    TS_ASSERT( (one ^ zero) == one );
+    TS_ASSERT( two + two == 4 );
+    TS_ASSERT( (two ^ two) == 4 );
+    TS_ASSERT( two * two == 4 );
+    TS_ASSERT( (two += two) == 4 );
+    TS_ASSERT( two == 4 );
+    TS_ASSERT( (two = 2) == 2 );
+    TS_ASSERT( two == 2 );
+    TS_ASSERT( (two *= 2) == 4 );
+    TS_ASSERT( two == 4 );
+    TS_ASSERT( ((two = 2) ^= 2) == 4 );
+    TS_ASSERT( two == 4 );
+    TS_ASSERT( (two = 2) == 2 );
+
+    // infinite cardinal arithmetic
+
+    Cardinality x = i, y = Cardinality(2)^x, z = Cardinality(2)^y;
+
+    TS_ASSERT( x == i && y == r );
+    TS_ASSERT( x != r && y != i );
+    TS_ASSERT( x != z && y != z );
+    TS_ASSERT( x.isCountable() && !x.isFinite() );
+    TS_ASSERT( !y.isCountable() && !y.isFinite() );
+    TS_ASSERT( !z.isCountable() && !z.isFinite() );
+
+    TS_ASSERT( big < x );
+    TS_ASSERT( x < y );
+    TS_ASSERT( y < z );
+
+    TS_ASSERT_THROWS( big.getBethNumber(), IllegalArgumentException );
+    TS_ASSERT( x.getBethNumber() == 0 );
+    TS_ASSERT( y.getBethNumber() == 1 );
+    TS_ASSERT( z.getBethNumber() == 2 );
+
+    TS_ASSERT( (zero ^ x) == zero );
+    TS_ASSERT( (one ^ x) == one );
+    TS_ASSERT( (two ^ x) == y && (two ^ x) != x );
+    TS_ASSERT( (big ^ x) == y && (big ^ x) != x );
+    TS_ASSERT( (two ^ x) == (big ^ x) );
+
+    TS_ASSERT( (x ^ zero) == one );
+    TS_ASSERT( (x ^ one) == x );
+    TS_ASSERT( (x ^ two) == x );
+    TS_ASSERT( (x ^ big) == x );
+    TS_ASSERT( (x ^ big) == (x ^ two) );
+
+    TS_ASSERT( (zero ^ y) == zero );
+    TS_ASSERT( (one ^ y) == one );
+    TS_ASSERT( (two ^ y) != x && (two ^ y) != y );
+    TS_ASSERT( (big ^ y) != y && (big ^ y) != y );
+    TS_ASSERT( (big ^ y).getBethNumber() == 2 );
+    TS_ASSERT( (two ^ y) == (big ^ y) );
+
+    TS_ASSERT( (y ^ zero) == one );
+    TS_ASSERT( (y ^ one) == y );
+    TS_ASSERT( (y ^ two) == y );
+    TS_ASSERT( (y ^ big) == y );
+    TS_ASSERT( (y ^ big) == (y ^ two) );
+
+    TS_ASSERT( (x ^ x) == y );
+    TS_ASSERT( (y ^ x) == y );
+    TS_ASSERT( (x ^ y) == z );
+    TS_ASSERT( (y ^ y) == z );
+    TS_ASSERT( (z ^ x) == z );
+    TS_ASSERT( (z ^ y) == z );
+    TS_ASSERT( (zero ^ z) == 0 );
+    TS_ASSERT( (z ^ zero) == 1 );
+    TS_ASSERT( (z ^ 0) == 1 );
+    TS_ASSERT( (two ^ z) > z );
+    TS_ASSERT( (big ^ z) == (two ^ z) );
+    TS_ASSERT( (x ^ z) == (two ^ z) );
+    TS_ASSERT( (y ^ z) == (x ^ z) );
+    TS_ASSERT( (z ^ z) == (x ^ z) );
+    TS_ASSERT( (z ^ z).getBethNumber() == 3 );
+
+  }/* testCardinalities() */
+
+};/* class CardinalityPublic */
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index f4bd1f8b8..66e29a01b 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -18,6 +18,7 @@
 
 #include <cxxtest/TestSuite.h>
 #include <sstream>
+#include <limits>
 
 #include "util/integer.h"
 
@@ -295,6 +296,17 @@ public:
     TS_ASSERT_EQUALS( Integer(-1000), Integer(-10).pow(3) );
   }
 
+  void testOverlyLong() {
+    unsigned long ul = numeric_limits<unsigned long>::max();
+    Integer i(ul);
+    TS_ASSERT(i.getUnsignedLong() == ul);
+    TS_ASSERT_THROWS_ANYTHING(i.getLong());
+    unsigned long ulplus1 = ul + 1;
+    TS_ASSERT(ulplus1 == 0);
+    i = i + 1;
+    TS_ASSERT_THROWS_ANYTHING(i.getUnsignedLong());
+  }
+
   void testTestBit() {
     TS_ASSERT( ! Integer(0).testBit(6) );
     TS_ASSERT( ! Integer(0).testBit(5) );
diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h
index a41f75af9..d7587d679 100644
--- a/test/unit/util/subrange_bound_white.h
+++ b/test/unit/util/subrange_bound_white.h
@@ -11,9 +11,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief White box testing of CVC4::SubrangeBound
+ ** \brief White-box testing of CVC4::SubrangeBound
  **
- ** White box testing of CVC4::SubrangeBound.
+ ** White-box testing of CVC4::SubrangeBound.
  **/
 
 #include "util/subrange_bound.h"