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, 234 insertions, 0 deletions

diff --git a/src/util/cardinality.h b/src/util/cardinality.h
new file mode 100644
index 000000000..c520c2735
--- /dev/null
+++ b/src/util/cardinality.h
@@ -0,0 +1,234 @@
+/*********************                                                        */
+/*! \file cardinality.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 Representation of cardinality
+ **
+ ** Simple class to represent a cardinality; used by the CVC4 type system
+ ** give the cardinality of sorts.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CARDINALITY_H
+#define __CVC4__CARDINALITY_H
+
+#include <iostream>
+#include <utility>
+
+#include "util/integer.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+/**
+ * A simple representation of a cardinality.  We store an
+ * arbitrary-precision integer for finite cardinalities, and we
+ * distinguish infinite cardinalities represented as Beth numbers.
+ */
+class CVC4_PUBLIC Cardinality {
+  /** Cardinality of the integers */
+  static const Integer s_intCard;
+
+  /** Cardinality of the reals */
+  static const Integer s_realCard;
+
+  /**
+   * In the case of finite cardinality, this is >= 0, and is equal to
+   * the cardinality.  If infinite, it is < 0, and is Beth[|card|-1].
+   * That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc.
+   */
+  Integer d_card;
+
+public:
+
+  /** The cardinality of the set of integers. */
+  static const Cardinality INTEGERS;
+
+  /** The cardinality of the set of real numbers. */
+  static const Cardinality REALS;
+
+  /**
+   * Representation for a Beth number, used only to construct
+   * Cardinality objects.
+   */
+  class Beth {
+    Integer d_index;
+
+  public:
+    Beth(const Integer& beth) : d_index(beth) {
+      CheckArgument(beth >= 0, beth,
+                    "Beth index must be a nonnegative integer, not %s.",
+                    beth.toString().c_str());
+    }
+
+    const Integer& getNumber() const throw() {
+      return d_index;
+    }
+  };/* class Cardinality::Beth */
+
+  /**
+   * Construct a finite cardinality equal to the integer argument.
+   * The argument must be nonnegative.  If we change this to an
+   * "unsigned" argument to enforce the restriction, we mask some
+   * errors that automatically convert, like "Cardinality(-1)".
+   */
+  Cardinality(long card) : d_card(card) {
+    CheckArgument(card >= 0, card,
+                  "Cardinality must be a nonnegative integer, not %ld.", card);
+    Assert(isFinite());
+  }
+
+  /**
+   * Construct a finite cardinality equal to the integer argument.
+   * The argument must be nonnegative.
+   */
+  Cardinality(const Integer& card) : d_card(card) {
+    CheckArgument(card >= 0, card,
+                  "Cardinality must be a nonnegative integer, not %s.",
+                  card.toString().c_str());
+    Assert(isFinite());
+  }
+
+  /**
+   * Construct an infinite cardinality equal to the given Beth number.
+   */
+  Cardinality(Beth beth) : d_card(-beth.getNumber() - 1) {
+    Assert(!isFinite());
+  }
+
+  /** Returns true iff this cardinality is finite. */
+  bool isFinite() const throw() {
+    return d_card >= 0;
+  }
+
+  /**
+   * Returns true iff this cardinality is finite or countably
+   * infinite.
+   */
+  bool isCountable() const throw() {
+    return d_card >= s_intCard;
+  }
+
+  /**
+   * In the case that this cardinality is finite, return its
+   * cardinality.  (If this cardinality is infinite, this function
+   * throws an IllegalArgumentException.)
+   */
+  const Integer& getFiniteCardinality() const throw(IllegalArgumentException) {
+    CheckArgument(isFinite(), *this, "This cardinality is not finite.");
+    return d_card;
+  }
+
+  /**
+   * In the case that this cardinality is infinite, return its Beth
+   * number.  (If this cardinality is finite, this function throws an
+   * IllegalArgumentException.)
+   */
+  Integer getBethNumber() const throw(IllegalArgumentException) {
+    CheckArgument(!isFinite(), *this, "This cardinality is not infinite.");
+    return -d_card - 1;
+  }
+
+  /** Assigning addition of this cardinality with another. */
+  Cardinality& operator+=(const Cardinality& c) throw();
+
+  /** Assigning multiplication of this cardinality with another. */
+  Cardinality& operator*=(const Cardinality& c) throw();
+
+  /** Assigning exponentiation of this cardinality with another. */
+  Cardinality& operator^=(const Cardinality& c) throw(IllegalArgumentException);
+
+  /** Add two cardinalities. */
+  Cardinality operator+(const Cardinality& c) const throw() {
+    Cardinality card(*this);
+    card += c;
+    return card;
+  }
+
+  /** Multiply two cardinalities. */
+  Cardinality operator*(const Cardinality& c) const throw() {
+    Cardinality card(*this);
+    card *= c;
+    return card;
+  }
+
+  /**
+   * Exponentiation of two cardinalities.  Throws an exception if both
+   * are finite and the exponent is too large.
+   */
+  Cardinality operator^(const Cardinality& c) const throw(IllegalArgumentException) {
+    Cardinality card(*this);
+    card ^= c;
+    return card;
+  }
+
+  /** Test for equality between cardinalities. */
+  bool operator==(const Cardinality& c) const throw() {
+    return d_card == c.d_card;
+  }
+
+  /** Test for disequality between cardinalities. */
+  bool operator!=(const Cardinality& c) const throw() {
+    return !(*this == c);
+  }
+
+  /** Test whether this cardinality is less than another. */
+  bool operator<(const Cardinality& c) const throw() {
+    return
+      ( isFinite() && !c.isFinite() ) ||
+      ( isFinite() && c.isFinite() && d_card < c.d_card ) ||
+      ( !isFinite() && !c.isFinite() && d_card > c.d_card );
+  }
+
+  /**
+   * Test whether this cardinality is less than or equal to
+   * another.
+   */
+  bool operator<=(const Cardinality& c) const throw() {
+    return *this < c || *this == c;
+  }
+
+  /** Test whether this cardinality is greater than another. */
+  bool operator>(const Cardinality& c) const throw() {
+    return !(*this <= c);
+  }
+
+  /**
+   * Test whether this cardinality is greater than or equal to
+   * another.
+   */
+  bool operator>=(const Cardinality& c) const throw() {
+    return !(*this < c);
+  }
+
+  /**
+   * Return a string representation of this cardinality.
+   */
+  std::string toString() const throw();
+
+};/* class Cardinality */
+
+
+/** Print an element of the InfiniteCardinality enumeration. */
+std::ostream& operator<<(std::ostream& out, Cardinality::Beth b)
+  throw() CVC4_PUBLIC;
+
+
+/** Print a cardinality in a human-readable fashion. */
+std::ostream& operator<<(std::ostream& out, const Cardinality& c)
+  throw() CVC4_PUBLIC;
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CARDINALITY_H */