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, 6 insertions, 35 deletions

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 */