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

11 files changed, 524 insertions, 43 deletions

diff --git a/src/util/Assert.h b/src/util/Assert.h
index 0ff89bedf..e38a3f9cf 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -221,6 +221,16 @@ public:
     va_end(args);
   }
 
+  InternalErrorException(const char* function, const char* file, unsigned line,
+                         std::string fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Internal error detected", "",
+              function, file, line, fmt.c_str(), args);
+    va_end(args);
+  }
+
 };/* class InternalErrorException */
 
 #ifdef CVC4_DEBUG
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index e76858d80..a6ff0ea40 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -45,8 +45,11 @@ libutil_la_SOURCES = \
 	stats.cpp \
 	dynamic_array.h \
 	language.h \
+	language.cpp \
 	triple.h \
 	subrange_bound.h \
+	cardinality.h \
+	cardinality.cpp \
 	trans_closure.h \
 	trans_closure.cpp \
 	boolean_simplification.h \
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
new file mode 100644
index 000000000..d38be1c92
--- /dev/null
+++ b/src/util/cardinality.cpp
@@ -0,0 +1,126 @@
+/*********************                                                        */
+/*! \file cardinality.cpp
+ ** \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
+ **
+ ** Implementation of a simple class to represent a cardinality.
+ **/
+
+#include "util/cardinality.h"
+
+namespace CVC4 {
+
+const Integer Cardinality::s_intCard(-1);
+const Integer Cardinality::s_realCard(-2);
+
+const Cardinality Cardinality::INTEGERS(Cardinality::Beth(0));
+const Cardinality Cardinality::REALS(Cardinality::Beth(1));
+
+Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
+  if(isFinite() && c.isFinite()) {
+    d_card += c.d_card;
+    return *this;
+  }
+  if(*this >= c) {
+    return *this;
+  } else {
+    return *this = c;
+  }
+}
+
+/** Assigning multiplication of this cardinality with another. */
+Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
+  if(*this == 0 || c == 0) {
+    return *this = 0;
+  } else if(!isFinite() || !c.isFinite()) {
+    if(*this >= c) {
+      return *this;
+    } else {
+      return *this = c;
+    }
+  } else {
+    d_card *= c.d_card;
+    return *this;
+  }
+}
+
+/** Assigning exponentiation of this cardinality with another. */
+Cardinality& Cardinality::operator^=(const Cardinality& c)
+  throw(IllegalArgumentException) {
+  if(c == 0) {
+    // (anything) ^ 0 == 1
+    d_card = 1;
+    return *this;
+  } else if(*this == 0) {
+    // 0 ^ (>= 1) == 0
+    return *this;
+  } else if(*this == 1) {
+    // 1 ^ (>= 1) == 1
+    return *this;
+  } else if(c == 1) {
+    // (anything) ^ 1 == (that thing)
+    return *this;
+  } else if(isFinite() && c.isFinite()) {
+    // finite ^ finite == finite
+    //
+    // Note: can throw an assertion if c is too big for
+    // exponentiation
+    d_card = d_card.pow(c.d_card.getUnsignedLong());
+    return *this;
+  } else if(!isFinite() && c.isFinite()) {
+    // inf ^ finite == inf
+    return *this;
+  } else {
+    Assert(*this >= 2 && !c.isFinite(),
+           "fall-through case not as expected:\n%s\n%s",
+           this->toString().c_str(), c.toString().c_str());
+    // (>= 2) ^ beth_k == beth_(k+1)
+    // unless the base is already > the exponent
+    if(*this > c) {
+      return *this;
+    }
+    d_card = c.d_card - 1;
+    return *this;
+  }
+}
+
+
+std::string Cardinality::toString() const throw() {
+  std::stringstream ss;
+  ss << *this;
+  return ss.str();
+}
+
+
+std::ostream& operator<<(std::ostream& out,
+                                Cardinality::Beth b)
+  throw() {
+  out << "beth[" << b.getNumber() << ']';
+
+  return out;
+}
+
+
+std::ostream& operator<<(std::ostream& out, const Cardinality& c)
+  throw() {
+  if(c.isFinite()) {
+    out << c.getFiniteCardinality();
+  } else {
+    out << Cardinality::Beth(c.getBethNumber());
+  }
+
+  return out;
+}
+
+
+}/* CVC4 namespace */
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 */
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 26e58264a..74bff1843 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -150,6 +150,7 @@ public:
 
       /** Get the name of this constructor argument. */
       std::string getName() const throw();
+
       /**
        * Get the selector for this constructor argument; this call is
        * only permitted after resolution.
@@ -203,12 +204,14 @@ public:
      * to this Datatype constructor.
      */
     void addArg(std::string selectorName, Type selectorType);
+
     /**
      * Add an argument (i.e., a data field) of the given name to this
      * Datatype constructor that refers to an as-yet-unresolved
      * Datatype (which may be mutually-recursive).
      */
     void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
+
     /**
      * Add a self-referential (i.e., a data field) of the given name
      * to this Datatype constructor that refers to the enclosing
diff --git a/src/util/debug.h b/src/util/debug.h
index 4fc5d5caa..402c5bed4 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -20,6 +20,8 @@
  ** util/Assert.h.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__DEBUG_H
 #define __CVC4__DEBUG_H
 
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
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
diff --git a/src/util/language.cpp b/src/util/language.cpp
new file mode 100644
index 000000000..da54a4783
--- /dev/null
+++ b/src/util/language.cpp
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file language.cpp
+ ** \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 Definition of input and output languages
+ **
+ ** Definition of input and output languages.
+ **/
+
+#include "util/language.h"
+
+namespace CVC4 {
+namespace language {
+
+InputLanguage toInputLanguage(OutputLanguage language) {
+  switch(language) {
+  case output::LANG_SMTLIB:
+  case output::LANG_SMTLIB_V2:
+  case output::LANG_CVC4:
+    // these entries directly correspond (by design)
+    return InputLanguage(int(language));
+
+  default: {
+    std::stringstream ss;
+    ss << "Cannot map output language `" << language
+       << "' to an input language.";
+    throw CVC4::Exception(ss.str());
+  }
+  }/* switch(language) */
+}/* toInputLanguage() */
+
+OutputLanguage toOutputLanguage(InputLanguage language) {
+  switch(language) {
+  case input::LANG_SMTLIB:
+  case input::LANG_SMTLIB_V2:
+  case input::LANG_CVC4:
+    // these entries directly correspond (by design)
+    return OutputLanguage(int(language));
+
+  default:
+    // Revert to the default (AST) language.
+    //
+    // We used to throw an exception here, but that's not quite right.
+    // We often call this while constructing exceptions, for one, and
+    // it's better to output SOMETHING related to the original
+    // exception rather than mask it with another exception.  Also,
+    // the input language isn't always defined---e.g. during the
+    // initial phase of the main CVC4 driver while it determines which
+    // language is appropriate, and during unit tests.  Also, when
+    // users are writing their own code against the library.
+    return output::LANG_AST;
+  }/* switch(language) */
+}/* toOutputLanguage() */
+
+}/* CVC4::language namespace */
+}/* CVC4 namespace */
diff --git a/src/util/language.h b/src/util/language.h
index 814f8dcd1..dbda6a315 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -31,7 +31,7 @@ namespace language {
 
 namespace input {
 
-enum Language {
+enum CVC4_PUBLIC Language {
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
   /** Auto-detect the language */
@@ -58,6 +58,7 @@ enum Language {
   LANG_MAX
 };/* enum Language */
 
+inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
   switch(lang) {
   case LANG_AUTO:
@@ -82,7 +83,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
 
 namespace output {
 
-enum Language {
+enum CVC4_PUBLIC Language {
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
   // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
@@ -109,6 +110,7 @@ enum Language {
   LANG_MAX
 };/* enum Language */
 
+inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
   switch(lang) {
   case LANG_SMTLIB:
@@ -138,39 +140,8 @@ typedef language::output::Language OutputLanguage;
 
 namespace language {
 
-inline InputLanguage toInputLanguage(OutputLanguage language) {
-  switch(language) {
-  case output::LANG_SMTLIB:
-  case output::LANG_SMTLIB_V2:
-  case output::LANG_CVC4:
-    // these entries directly correspond (by design)
-    return InputLanguage(int(language));
-
-  default: {
-    std::stringstream ss;
-    ss << "Cannot map output language `" << language
-       << "' to an input language.";
-    throw CVC4::Exception(ss.str());
-  }
-  }/* switch(language) */
-}/* toInputLanguage() */
-
-inline OutputLanguage toOutputLanguage(InputLanguage language) {
-  switch(language) {
-  case input::LANG_SMTLIB:
-  case input::LANG_SMTLIB_V2:
-  case input::LANG_CVC4:
-    // these entries directly correspond (by design)
-    return OutputLanguage(int(language));
-
-  default: {
-    std::stringstream ss;
-    ss << "Cannot map input language `" << language
-       << "' to an output language.";
-    throw CVC4::Exception(ss.str());
-  }
-  }/* switch(language) */
-}/* toOutputLanguage() */
+InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC;
+OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC;
 
 }/* CVC4::language namespace */
 }/* CVC4 namespace */
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
index fc6a259b4..0c84b214e 100644
--- a/src/util/subrange_bound.h
+++ b/src/util/subrange_bound.h
@@ -33,7 +33,7 @@ namespace CVC4 {
  * an infinite bound).  For example, the CVC language subrange [-5.._]
  * has a lower bound of -5 and an infinite upper bound.
  */
-class SubrangeBound {
+class CVC4_PUBLIC SubrangeBound {
   bool d_nobound;
   Integer d_bound;
 
@@ -79,6 +79,9 @@ public:
 };/* class SubrangeBound */
 
 inline std::ostream&
+operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC;
+
+inline std::ostream&
 operator<<(std::ostream& out, const SubrangeBound& bound) throw() {
   if(bound.hasBound()) {
     out << bound.getBound();