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, 30 insertions, 3 deletions

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index d13c946de..8c3fc14e5 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -142,25 +142,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( cln::floor1(d_value, y.d_value) );
   }
+  Integer& operator/=(const Integer& y) {
+    d_value = cln::floor1(d_value, y.d_value);
+    return *this;
+  }
 
   Integer operator%(const Integer& y) const {
     return Integer( cln::floor2(d_value, y.d_value).remainder );
   }
+  Integer& operator%=(const Integer& y) {
+    d_value = cln::floor2(d_value, y.d_value).remainder;
+    return *this;
+  }
 
   /** Raise this Integer to the power <code>exp</code>.
    *
@@ -208,8 +228,15 @@ public:
 
   //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
 
-  long getLong() const { return cln::cl_I_to_long(d_value); }
-  unsigned long getUnsignedLong() const {return cln::cl_I_to_ulong(d_value); }
+  long getLong() const {
+    // supposed to throw if not representable in type "long"
+    return cln::cl_I_to_long(d_value);
+  }
+
+  unsigned long getUnsignedLong() const {
+    // supposed to throw if not representable in type "unsigned long"
+    return cln::cl_I_to_ulong(d_value);
+  }
 
   /**
    * Computes the hash of the node from the first word of the