Minor mixed-bag commit. Expected performance impact negligible.

* Fixed hole in arrays typechecking.
* Fixed "make dist".
* Better ouroborous test, and some printer fixes.
* Continued cleanup in CVC parser, removed some warnings.
* Better output.

11 files changed, 173 insertions, 120 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 51a734757..74bfd3f2b 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -72,10 +72,8 @@ TypeCheckingException::~TypeCheckingException() throw () {
   delete d_expr;
 }
 
-std::string TypeCheckingException::toString() const {
-  std::stringstream ss;
-  ss << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr;
-  return ss.str();
+void TypeCheckingException::toStream(std::ostream& os) const {
+  os << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr;
 }
 
 Expr TypeCheckingException::getExpression() const {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index c45cc9b99..291016044 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -99,8 +99,12 @@ public:
    */
   Expr getExpression() const;
 
-  /** Returns the message corresponding to the type-checking failure */
-  std::string toString() const;
+  /**
+   * Returns the message corresponding to the type-checking failure.
+   * We prefer toStream() to toString() because that keeps the expr-depth
+   * and expr-language settings present in the stream.
+   */
+  void toStream(std::ostream& out) const;
 
   friend class ExprManager;
 };/* class TypeCheckingException */
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 445d91da8..586d0cb13 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: dejan
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** 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
@@ -35,10 +35,8 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
   delete d_node;
 }
 
-string TypeCheckingExceptionPrivate::toString() const {
-  stringstream ss;
-  ss << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
-  return ss.str();
+void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const {
+  os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
 }
 
 Node TypeCheckingExceptionPrivate::getNode() const {
diff --git a/src/expr/node.h b/src/expr/node.h
index 6fe1e7d0e..a40b3fce5 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -80,9 +80,14 @@ public:
    */
   NodeTemplate<true> getNode() const;
 
-  /** Returns the message corresponding to the type-checking failure */
-  std::string toString() const;
-};
+  /**
+   * Returns the message corresponding to the type-checking failure.
+   * We prefer toStream() to toString() because that keeps the expr-depth
+   * and expr-language settings present in the stream.
+   */
+  void toStream(std::ostream& out) const;
+
+};/* class TypeCheckingExceptionPrivate */
 
 /**
  * \typedef NodeTemplate<true> Node;
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 792f53605..794f0a670 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -460,8 +460,8 @@ command returns [CVC4::Command* cmd = 0]
   std::vector<CVC4::Datatype> dts;
   Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f);   }
-  | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f);    }
+  : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); }
+  | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f); }
   | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); }
   | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_CONST(true)); }
   | OPTION_TOK STRING_LITERAL symbolicExpr[sexpr] SEMICOLON
@@ -684,7 +684,16 @@ identifier[std::string& id,
   ;
 
 /**
- * Match the type in a declaration and do the declaration binding.
+ * Match the type in a declaration and do the declaration binding.  If
+ * "check" is CHECK_NONE, then identifiers occurring in the type need
+ * not exist!  They are created as "unresolved" types and linked up in
+ * a type-substitution pass.  Right now, only datatype definitions are
+ * supported in this way (since type names can occur without any
+ * forward-declaration in CVC language datatype definitions, we have
+ * to create types for them on-the-fly).  Before passing CHECK_NONE
+ * you really should have a clear idea of WHY you need to parse that
+ * way; then you should trace through Parser::mkMutualDatatypeType()
+ * to figure out just what you're in for.
  */
 type[CVC4::Type& t,
      CVC4::parser::DeclarationCheck check]
@@ -1059,8 +1068,8 @@ concatBitwiseTerm[CVC4::Expr& f]
   std::vector<unsigned> operators;
   unsigned op;
 }
-  : bitwiseXorTerm[f] { expressions.push_back(f); }
-    ( concatBitwiseBinop[op] bitwiseXorTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
+  : bvNegTerm[f] { expressions.push_back(f); }
+    ( concatBitwiseBinop[op] bvNegTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
     { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
   ;
 concatBitwiseBinop[unsigned& op]
@@ -1072,7 +1081,56 @@ concatBitwiseBinop[unsigned& op]
   | BVAND_TOK
   ;
 
-bitwiseXorTerm[CVC4::Expr& f]
+bvNegTerm[CVC4::Expr& f]
+    /* BV neg */
+  : BVNEG_TOK bvNegTerm[f]
+    { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
+  | selectExtractShift[f]
+  ;
+
+/**
+ * Parses an array select / bitvector extract / bitvector shift.
+ * These are all parsed the same way because they are all effectively
+ * post-fix operators and can continue piling onto an expression.
+ * Array selects and bitvector extracts even share similar syntax with
+ * their use of [ square brackets ], so we left-factor as much out as
+ * possible to make ANTLR happy.
+ */
+selectExtractShift[CVC4::Expr& f]
+@init {
+  Expr f2;
+  bool extract, left;
+}
+  : bvTerm[f]
+    ( /* array select / bitvector extract */
+      LBRACKET
+        ( formula[f2] { extract = false; }
+        | k1=numeral COLON k2=numeral { extract = true; } )
+      RBRACKET
+      { if(extract) {
+          /* bitvector extract */
+          f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f);
+        } else {
+          /* array select */
+          f = MK_EXPR(CVC4::kind::SELECT, f, f2);
+        }
+      }
+    | ( LEFTSHIFT_TOK { left = true; }
+      | RIGHTSHIFT_TOK { left = false; } ) k=numeral
+      { // Defined in:
+        // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
+        if(left) {
+          f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k)));
+        } else {
+          unsigned n = BitVectorType(f.getType()).getSize();
+          f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)),
+                      MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f));
+        }
+      }
+    )*
+  ;
+
+bvTerm[CVC4::Expr& f]
 @init {
   Expr f2;
 }
@@ -1087,27 +1145,15 @@ bitwiseXorTerm[CVC4::Expr& f]
     { f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); }
   | BVXNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
     { f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); }
-  | bvNegTerm[f]
-  ;
-bvNegTerm[CVC4::Expr& f]
-    /* BV neg */
-  : BVNEG_TOK bvNegTerm[f]
-    { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
-  | bvUminusTerm[f]
-  ;
-bvUminusTerm[CVC4::Expr& f]
-@init {
-  Expr f2;
-}
+
     /* BV unary minus */
-  : BVUMINUS_TOK LPAREN formula[f] RPAREN
+  | BVUMINUS_TOK LPAREN formula[f] RPAREN
     { f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); }
     /* BV addition */
   | BVPLUS_TOK LPAREN k=numeral COMMA formula[f]
     ( COMMA formula[f2] { f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, f, f2); } )+ RPAREN
     { unsigned size = BitVectorType(f.getType()).getSize();
       if(k == 0) {
-#       warning cannot do BVPLUS(...)[i:j]
         PARSER_STATE->parseError("BVPLUS(k,_,_,...) must have k > 0");
       }
       if(k > size) {
@@ -1191,35 +1237,9 @@ bvUminusTerm[CVC4::Expr& f]
     /* BV rotate left */
   | BVROTL_TOK LPAREN formula[f] COMMA k=numeral RPAREN
     { f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); }
-    /* left and right shifting with << and >>, or something else */
-  | bvShiftTerm[f]
-  ;
 
-bvShiftTerm[CVC4::Expr& f]
-@init {
-  bool left = false;
-}
-  : bvComparison[f]
-    ( (LEFTSHIFT_TOK { left = true; } | RIGHTSHIFT_TOK) k=numeral
-      { // Defined in:
-        // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
-        if(left) {
-          f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k)));
-        } else {
-          unsigned n = BitVectorType(f.getType()).getSize();
-          f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)),
-                      MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f));
-        }
-      }
-    )?
-  ;
-
-bvComparison[CVC4::Expr& f]
-@init {
-  Expr f2;
-}
     /* BV comparisons */
-  : BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+  | BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_EXPR(CVC4::kind::BITVECTOR_ULT, f, f2); }
   | BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_EXPR(CVC4::kind::BITVECTOR_ULE, f, f2); }
@@ -1235,35 +1255,13 @@ bvComparison[CVC4::Expr& f]
     { f = MK_EXPR(CVC4::kind::BITVECTOR_SGT, f, f2); }
   | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_EXPR(CVC4::kind::BITVECTOR_SGE, f, f2); }
+
   /*
   | IS_INTEGER_TOK LPAREN formula[f] RPAREN
     { f = MK_EXPR(CVC4::kind::BITVECTOR_IS_INTEGER, f); }
   */
-  | selectExtractTerm[f]
-  ;
-
-/** Parses an array select. */
-selectExtractTerm[CVC4::Expr& f]
-@init {
-  Expr f2;
-  bool extract;
-}
-    /* array select / bitvector extract */
-  : simpleTerm[f]
-    ( { extract = false; }
-      LBRACKET formula[f2] ( COLON k2=numeral { extract = true; } )? RBRACKET
-      { if(extract) {
-          if(f2.getKind() != kind::CONST_INTEGER) {
-            PARSER_STATE->parseError("bitvector extraction requires [numeral:numeral] range");
-          }
-          unsigned k1 = f2.getConst<Integer>().getLong();
-          f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f);
-        } else {
-          f = MK_EXPR(CVC4::kind::SELECT, f, f2);
-        }
-      }
-    )*
 
+  | simpleTerm[f]
   ;
 
 /** Parses a simple term. */
@@ -1447,13 +1445,7 @@ selector[CVC4::Datatype::Constructor& ctor]
   Type t;
 }
   : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON type[t,CHECK_NONE]
-    { if(t.isNull()) {
-#       warning FIXME datatypes
-        //std::pair<Type, std::string> unresolved = PARSER_STATE->newUnresolvedType();
-        //ctor.addArg(id, Datatype::UnresolvedType(unresolved.second);
-      } else {
-        ctor.addArg(id, t);
-      }
+    { ctor.addArg(id, t);
       Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
     }
   ;
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 9a5b654a8..d32914d8e 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -5,7 +5,7 @@
  ** Major contributors: cconway
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** 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
@@ -64,14 +64,12 @@ public:
   // Destructor
   virtual ~ParserException() throw() {}
 
-  virtual std::string toString() const {
+  virtual void toStream(std::ostream& os) const {
     if( d_line > 0 ) {
-      std::stringstream ss;
-      ss <<  "Parse Error: " << d_filename << ":" << d_line << "."
+      os <<  "Parse Error: " << d_filename << ":" << d_line << "."
          << d_column << ": " << d_msg;
-      return ss.str();
     } else {
-      return "Parse Error: " + d_msg;
+      os << "Parse Error: " << d_msg;
     }
   }
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 409518fcf..e23d7c88b 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -182,7 +182,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
       out << "BVROTR(" << n[0] << "," << n.getOperator() << ')';
       break;
 
-
     default:
       out << n.getOperator();
       if(n.getNumChildren() > 0) {
@@ -233,15 +232,20 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
       out << "IF " << n[0] << " THEN " << n[1] << " ELSE " << n[2];
       break;
 
-    // these are prefix
+    // these are prefix and have an extra size 'k' as first argument
     case kind::BITVECTOR_PLUS:
     case kind::BITVECTOR_SUB:
+    case kind::BITVECTOR_MULT:
+      out << n.getOperator() << '(' << n.getType().getBitVectorSize() << ','
+          << n[0] << ',' << n[1] << ')';
+      break;
+
+    // these are prefix
     case kind::BITVECTOR_XOR:
     case kind::BITVECTOR_NAND:
     case kind::BITVECTOR_NOR:
     case kind::BITVECTOR_XNOR:
     case kind::BITVECTOR_COMP:
-    case kind::BITVECTOR_MULT:
     case kind::BITVECTOR_UDIV:
     case kind::BITVECTOR_UREM:
     case kind::BITVECTOR_SDIV:
@@ -267,7 +271,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
         out << n[0][0] << " /= " << n[0][1];
       } else if(n.getNumChildren() == 2) {
         // infix operator
-        out << n[0] << ' ' << n.getOperator() << ' ' << n[1];
+        out << '(' << n[0] << ' ' << n.getOperator() << ' ' << n[1] << ')';
+      } else if(k == kind::BITVECTOR_NOT) {
+        // precedence on ~ is a little unexpected; add parens
+        out << "(~(" << n[0] << "))";
       } else {
         // prefix operator
         out << n.getOperator() << ' ';
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2467db3bb..376a8a531 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): taking, cconway
+ ** Minor contributors (to current version): cconway
  ** 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
@@ -346,7 +346,8 @@ void SmtEngine::defineFunction(Expr func,
     FunctionType(funcType).getRangeType() : funcType;
   if(formulaType != rangeType) {
     stringstream ss;
-    ss << "Defined function's declared type does not match that of body\n"
+    ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
+       << "Defined function's declared type does not match that of body\n"
        << "The function  : " << func << "\n"
        << "Its range type: " << rangeType << "\n"
        << "The body      : " << formula << "\n"
@@ -474,9 +475,11 @@ Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in)
     // theory could still create a new expression that isn't
     // well-typed, and we don't want the C++ runtime to abort our
     // process without any error notice.
-    InternalError("A bad expression was produced.  "
-                  "Original exception follows:\n%s",
-                  tcep.toString().c_str());
+    stringstream ss;
+    ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
+       << "A bad expression was produced.  Original exception follows:\n"
+       << tcep;
+    InternalError(ss.str().c_str());
   }
 }
 
@@ -503,9 +506,11 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
     // theory could still create a new expression that isn't
     // well-typed, and we don't want the C++ runtime to abort our
     // process without any error notice.
-    InternalError("A bad expression was produced.  "
-                  "Original exception follows:\n%s",
-                  tcep.toString().c_str());
+    stringstream ss;
+    ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
+       << "A bad expression was produced.  Original exception follows:\n"
+       << tcep;
+    InternalError(ss.str().c_str());
   }
 }
 
@@ -514,7 +519,8 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) {
   Type boolType = d_exprManager->booleanType();
   if(type != boolType) {
     stringstream ss;
-    ss << "Expected " << boolType << "\n"
+    ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
+       << "Expected " << boolType << "\n"
        << "The assertion : " << e << "\n"
        << "Its type      : " << type;
     throw TypeCheckingException(e, ss.str());
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 9f24e9873..11e8a8443 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -5,7 +5,7 @@
  ** Major contributors: cconway
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** 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
@@ -31,6 +31,9 @@ struct ArraySelectTypeRule {
     Assert(n.getKind() == kind::SELECT);
     TypeNode arrayType = n[0].getType(check);
     if( check ) {
+      if(!arrayType.isArray()) {
+        throw TypeCheckingExceptionPrivate(n, "array select operating on non-array");
+      }
       TypeNode indexType = n[1].getType(check);
       if(arrayType.getArrayIndexType() != indexType) {
         throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
@@ -46,6 +49,9 @@ struct ArrayStoreTypeRule {
     Assert(n.getKind() == kind::STORE);
     TypeNode arrayType = n[0].getType(check);
     if( check ) {
+      if(!arrayType.isArray()) {
+        throw TypeCheckingExceptionPrivate(n, "array store operating on non-array");
+      }
       TypeNode indexType = n[1].getType(check);
       TypeNode valueType = n[2].getType(check);
       if(arrayType.getArrayIndexType() != indexType) {
diff --git a/src/util/exception.h b/src/util/exception.h
index 4893bd3c2..1b1eb224e 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** 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
@@ -21,7 +21,9 @@
 #ifndef __CVC4__EXCEPTION_H
 #define __CVC4__EXCEPTION_H
 
+#include <iostream>
 #include <string>
+#include <sstream>
 
 namespace CVC4 {
 
@@ -38,16 +40,36 @@ public:
   // NON-VIRTUAL METHOD for setting and printing the error message
   void setMessage(const std::string& msg) { d_msg = msg; }
   std::string getMessage() const { return d_msg; }
-    // Printing: feel free to redefine toString().  When inherited,
-  // it's recommended that this method print the type of exception
-  // before the actual message.
-  virtual std::string toString() const { return d_msg; }
+  /**
+   * Get this exception as a string.  Note that
+   *   cout << ex.toString();
+   * is subtly different from
+   *   cout << ex;
+   * which is equivalent to
+   *   ex.toStream(cout);
+   * That is because with the latter two, the output language (and
+   * other preferences) for exprs on the stream is respected.  In
+   * toString(), there is no stream, so the parameters are default
+   * and you'll get exprs and types printed using the AST language.
+   */
+  std::string toString() const {
+    std::stringstream ss;
+    toStream(ss);
+    return ss.str();
+  }
+  /**
+   * Printing: feel free to redefine toStream().  When overridden in
+   * a derived class, it's recommended that this method print the
+   * type of exception before the actual message.
+   */
+  virtual void toStream(std::ostream& os) const { os << d_msg; }
   // No need to overload operator<< for the inherited classes
   friend std::ostream& operator<<(std::ostream& os, const Exception& e);
 };/* class Exception */
 
 inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
-  return os << e.toString();
+  e.toStream(os);
+  return os;
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/language.h b/src/util/language.h
index fdd2a382d..814f8dcd1 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** 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
@@ -138,12 +138,29 @@ 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 correspond
+    // these entries directly correspond (by design)
     return OutputLanguage(int(language));
 
   default: {