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, 41 insertions, 4 deletions

diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 13bed50b3..c1d46ca65 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -25,6 +25,7 @@
 #include <string>
 #include <iostream>
 
+#include "util/Assert.h"
 #include "util/gmp_util.h"
 
 namespace CVC4 {
@@ -84,7 +85,7 @@ public:
     return d_value == y.d_value;
   }
 
-  Integer operator-() const{
+  Integer operator-() const {
     return Integer(-(d_value));
   }
 
@@ -110,23 +111,45 @@ public:
   }
 
 
-  Integer operator+(const Integer& y) const{
+  Integer operator+(const Integer& y) const {
     return Integer( d_value + y.d_value );
   }
+  Integer& operator+=(const Integer& y) {
+    d_value += y.d_value;
+    return *this;
+  }
 
   Integer operator-(const Integer& y) const {
     return Integer( d_value - y.d_value );
   }
+  Integer& operator-=(const Integer& y) {
+    d_value -= y.d_value;
+    return *this;
+  }
 
   Integer operator*(const Integer& y) const {
     return Integer( d_value * y.d_value );
   }
+  Integer& operator*=(const Integer& y) {
+    d_value *= y.d_value;
+    return *this;
+  }
+
   Integer operator/(const Integer& y) const {
     return Integer( d_value / y.d_value );
   }
+  Integer& operator/=(const Integer& y) {
+    d_value /= y.d_value;
+    return *this;
+  }
+
   Integer operator%(const Integer& y) const {
     return Integer( d_value % y.d_value );
   }
+  Integer& operator%=(const Integer& y) {
+    d_value %= y.d_value;
+    return *this;
+  }
 
   /** Raise this Integer to the power <code>exp</code>.
    *
@@ -144,8 +167,22 @@ public:
 
   //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
 
-  long getLong() const { return d_value.get_si(); }
-  unsigned long getUnsignedLong() const {return d_value.get_ui(); }
+  long getLong() const {
+    long si = d_value.get_si();
+#ifdef CVC4_ASSERTIONS
+    // ensure there wasn't overflow
+    Assert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0);
+#endif /* CVC4_ASSERTIONS */
+    return si;
+  }
+  unsigned long getUnsignedLong() const {
+    unsigned long ui = d_value.get_ui();
+#ifdef CVC4_ASSERTIONS
+    // ensure there wasn't overflow
+    Assert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0);
+#endif /* CVC4_ASSERTIONS */
+    return ui;
+  }
 
   /**
    * Computes the hash of the node from the first word of the