More language bindings work:

* with a patched SWIG, the ocaml bindings build correctly.
** I will provide my patch to the SWIG dev team.
* fixed some class interfaces to play more nicely with SWIG.
* php, perl, tcl now work; examples added.
* improved binding module building and installation.

Also:

Stop #defining NULL ((void*) 0).  This has been in cvc4_public.h for
a long, long time, I forget why I added it in the first place, and
it's a very, very bad idea.  In C++, certain things are permitted
for NULL that aren't permitted for ((void*) 0), like for instance
implicit conversion to any pointer type.  We didn't see an issue
here (until now, when interfacing with SWIG), because GCC is usually
pretty smart at working around such a broken #definition of NULL.
But that's fragile.

New exception-free Command architecture.  Previously, some command
invocations were wrapped in a try {} catch() {} and printed out an
error.  This is much more consistent now.  Each Command invocation
results in a CommandStatus.  The status can be "unsupported",
"error", or "success" (these are each derived classes, though, not
strings, so that they can be easily printed in a language-specific
way... e.g., in SMT-LIBv2, they are printed in a manner consistent
with the spec, and "success" is not printed if the print-success
option is off.)  All Command functionality are now no-throw
functions, which @cconway reports is a Good Thing for Google
(where all C++ exceptions are suspect), and also I think is much
cleaner than the old way in this instance.

Added an --smtlib2 option that enables an "SMT-LIBv2 compliance
mode"---really it just sets a few other options like strictParsing,
inputLanguage, and printSuccess.  In the future we might put other
options into a compliance mode, or we might choose to make it the
default.

8 files changed, 600 insertions, 332 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 345d7f956..47c6d1eb5 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -21,6 +21,7 @@
 #include <utility>
 #include <iterator>
 #include <sstream>
+#include <exception>
 
 #include "expr/command.h"
 #include "smt/smt_engine.h"
@@ -34,7 +35,10 @@ using namespace std;
 
 namespace CVC4 {
 
-std::ostream& operator<<(std::ostream& out, const Command& c) {
+const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
+const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
+
+std::ostream& operator<<(std::ostream& out, const Command& c) throw() {
   c.toStream(out,
              Node::setdepth::getDepth(out),
              Node::printtypes::getPrintTypes(out),
@@ -42,7 +46,7 @@ std::ostream& operator<<(std::ostream& out, const Command& c) {
   return out;
 }
 
-ostream& operator<<(ostream& out, const Command* c) {
+ostream& operator<<(ostream& out, const Command* c) throw() {
   if(c == NULL) {
     out << "null";
   } else {
@@ -51,180 +55,259 @@ ostream& operator<<(ostream& out, const Command* c) {
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() {
+  s.toStream(out, Node::setlanguage::getLanguage(out));
+  return out;
+}
+
+ostream& operator<<(ostream& out, const CommandStatus* s) throw() {
+  if(s == NULL) {
+    out << "null";
+  } else {
+    out << *s;
+  }
+  return out;
+}
+
 /* class Command */
 
-void Command::invoke(SmtEngine* smtEngine, std::ostream& out) {
+Command::Command() throw() : d_commandStatus(NULL) {
+}
+
+Command::~Command() throw() {
+  if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) {
+    delete d_commandStatus;
+  }
+}
+
+bool Command::ok() const throw() {
+  // either we haven't run the command yet, or it ran successfully
+  return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL;
+}
+
+void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
   invoke(smtEngine);
   printResult(out);
 }
 
-std::string Command::toString() const {
+std::string Command::toString() const throw() {
   std::stringstream ss;
   toStream(ss);
   return ss.str();
 }
 
 void Command::toStream(std::ostream& out, int toDepth, bool types,
-                       OutputLanguage language) const {
+                       OutputLanguage language) const throw() {
   Printer::getPrinter(language)->toStream(out, this, toDepth, types);
 }
 
-void Command::printResult(std::ostream& out) const {
+void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() {
+  Printer::getPrinter(language)->toStream(out, this);
+}
+
+void Command::printResult(std::ostream& out) const throw() {
+  if(d_commandStatus != NULL) {
+    out << *d_commandStatus;
+  }
 }
 
 /* class EmptyCommand */
 
-EmptyCommand::EmptyCommand(std::string name) :
+EmptyCommand::EmptyCommand(std::string name) throw() :
   d_name(name) {
 }
 
-std::string EmptyCommand::getName() const {
+std::string EmptyCommand::getName() const throw() {
   return d_name;
 }
 
-void EmptyCommand::invoke(SmtEngine* smtEngine) {
+void EmptyCommand::invoke(SmtEngine* smtEngine) throw() {
   /* empty commands have no implementation */
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class AssertCommand */
 
-AssertCommand::AssertCommand(const BoolExpr& e) :
+AssertCommand::AssertCommand(const BoolExpr& e) throw() :
   d_expr(e) {
 }
 
-BoolExpr AssertCommand::getExpr() const {
+BoolExpr AssertCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void AssertCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->assertFormula(d_expr);
+void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    smtEngine->assertFormula(d_expr);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
 /* class PushCommand */
 
-void PushCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->push();
+void PushCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    smtEngine->push();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
 /* class PopCommand */
 
-void PopCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->pop();
+void PopCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    smtEngine->pop();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
 /* class CheckSatCommand */
 
-CheckSatCommand::CheckSatCommand() :
+CheckSatCommand::CheckSatCommand() throw() :
   d_expr() {
 }
 
-CheckSatCommand::CheckSatCommand(const BoolExpr& expr) :
+CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() :
   d_expr(expr) {
 }
 
-BoolExpr CheckSatCommand::getExpr() const {
+BoolExpr CheckSatCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void CheckSatCommand::invoke(SmtEngine* smtEngine) {
-  d_result = smtEngine->checkSat(d_expr);
+void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->checkSat(d_expr);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
-Result CheckSatCommand::getResult() const {
+Result CheckSatCommand::getResult() const throw() {
   return d_result;
 }
 
-void CheckSatCommand::printResult(std::ostream& out) const {
-  out << d_result << endl;
+void CheckSatCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
 }
 
 /* class QueryCommand */
 
-QueryCommand::QueryCommand(const BoolExpr& e) :
+QueryCommand::QueryCommand(const BoolExpr& e) throw() :
   d_expr(e) {
 }
 
-BoolExpr QueryCommand::getExpr() const {
+BoolExpr QueryCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void QueryCommand::invoke(SmtEngine* smtEngine) {
-  d_result = smtEngine->query(d_expr);
+void QueryCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->query(d_expr);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
-Result QueryCommand::getResult() const {
+Result QueryCommand::getResult() const throw() {
   return d_result;
 }
 
-void QueryCommand::printResult(std::ostream& out) const {
-  out << d_result << endl;
+void QueryCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
 }
 
 /* class QuitCommand */
 
-QuitCommand::QuitCommand() {
+QuitCommand::QuitCommand() throw() {
 }
 
-void QuitCommand::invoke(SmtEngine* smtEngine) {
+void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("benchmark") << *this;
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class CommentCommand */
 
-CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {
+CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
 }
 
-std::string CommentCommand::getComment() const {
+std::string CommentCommand::getComment() const throw() {
   return d_comment;
 }
 
-void CommentCommand::invoke(SmtEngine* smtEngine) {
+void CommentCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("benchmark") << *this;
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class CommandSequence */
 
-CommandSequence::CommandSequence() :
+CommandSequence::CommandSequence() throw() :
   d_index(0) {
 }
 
-CommandSequence::~CommandSequence() {
+CommandSequence::~CommandSequence() throw() {
   for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
     delete d_commandSequence[i];
   }
 }
 
-void CommandSequence::addCommand(Command* cmd) {
+void CommandSequence::addCommand(Command* cmd) throw() {
   d_commandSequence.push_back(cmd);
 }
 
-void CommandSequence::invoke(SmtEngine* smtEngine) {
+void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
   for(; d_index < d_commandSequence.size(); ++d_index) {
     d_commandSequence[d_index]->invoke(smtEngine);
+    if(! d_commandSequence[d_index]->ok()) {
+      // abort execution
+      d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
+      return;
+    }
     delete d_commandSequence[d_index];
   }
+
+  AlwaysAssert(d_commandStatus == NULL);
+  d_commandStatus = CommandSuccess::instance();
 }
 
-void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
+void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
   for(; d_index < d_commandSequence.size(); ++d_index) {
     d_commandSequence[d_index]->invoke(smtEngine, out);
     delete d_commandSequence[d_index];
   }
 }
 
-CommandSequence::const_iterator CommandSequence::begin() const {
+CommandSequence::const_iterator CommandSequence::begin() const throw() {
   return d_commandSequence.begin();
 }
 
-CommandSequence::const_iterator CommandSequence::end() const {
+CommandSequence::const_iterator CommandSequence::end() const throw() {
   return d_commandSequence.end();
 }
 
-CommandSequence::iterator CommandSequence::begin() {
+CommandSequence::iterator CommandSequence::begin() throw() {
   return d_commandSequence.begin();
 }
 
-CommandSequence::iterator CommandSequence::end() {
+CommandSequence::iterator CommandSequence::end() throw() {
   return d_commandSequence.end();
 }
 
@@ -232,53 +315,53 @@ CommandSequence::iterator CommandSequence::end() {
 
 /* class DeclarationDefinitionCommand */
 
-DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) :
+DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() :
   d_symbol(id) {
 }
 
-std::string DeclarationDefinitionCommand::getSymbol() const {
+std::string DeclarationDefinitionCommand::getSymbol() const throw() {
   return d_symbol;
 }
 
 /* class DeclareFunctionCommand */
 
-DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) :
+DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) throw() :
   DeclarationDefinitionCommand(id),
   d_type(t) {
 }
 
-Type DeclareFunctionCommand::getType() const {
+Type DeclareFunctionCommand::getType() const throw() {
   return d_type;
 }
 
-void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) {
+void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
 }
 
 /* class DeclareTypeCommand */
 
-DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) :
+DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() :
   DeclarationDefinitionCommand(id),
   d_arity(arity),
   d_type(t) {
 }
 
-size_t DeclareTypeCommand::getArity() const {
+size_t DeclareTypeCommand::getArity() const throw() {
   return d_arity;
 }
 
-Type DeclareTypeCommand::getType() const {
+Type DeclareTypeCommand::getType() const throw() {
   return d_type;
 }
 
-void DeclareTypeCommand::invoke(SmtEngine* smtEngine) {
+void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
 }
 
 /* class DefineTypeCommand */
 
 DefineTypeCommand::DefineTypeCommand(const std::string& id,
-                                     Type t) :
+                                     Type t) throw() :
   DeclarationDefinitionCommand(id),
   d_params(),
   d_type(t) {
@@ -286,29 +369,30 @@ DefineTypeCommand::DefineTypeCommand(const std::string& id,
 
 DefineTypeCommand::DefineTypeCommand(const std::string& id,
                                      const std::vector<Type>& params,
-                                     Type t) :
+                                     Type t) throw() :
   DeclarationDefinitionCommand(id),
   d_params(params),
   d_type(t) {
 }
 
-const std::vector<Type>& DefineTypeCommand::getParameters() const {
+const std::vector<Type>& DefineTypeCommand::getParameters() const throw() {
   return d_params;
 }
 
-Type DefineTypeCommand::getType() const {
+Type DefineTypeCommand::getType() const throw() {
   return d_type;
 }
 
-void DefineTypeCommand::invoke(SmtEngine* smtEngine) {
+void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class DefineFunctionCommand */
 
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
                                              Expr func,
-                                             Expr formula) :
+                                             Expr formula) throw() :
   DeclarationDefinitionCommand(id),
   d_func(func),
   d_formals(),
@@ -318,30 +402,31 @@ DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
                                              Expr func,
                                              const std::vector<Expr>& formals,
-                                             Expr formula) :
+                                             Expr formula) throw() :
   DeclarationDefinitionCommand(id),
   d_func(func),
   d_formals(formals),
   d_formula(formula) {
 }
 
-Expr DefineFunctionCommand::getFunction() const {
+Expr DefineFunctionCommand::getFunction() const throw() {
   return d_func;
 }
 
-const std::vector<Expr>& DefineFunctionCommand::getFormals() const {
+const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() {
   return d_formals;
 }
 
-Expr DefineFunctionCommand::getFormula() const {
+Expr DefineFunctionCommand::getFormula() const throw() {
   return d_formula;
 }
 
-void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
+void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   //Dump("declarations") << *this << endl; -- done by SmtEngine
   if(!d_func.isNull()) {
     smtEngine->defineFunction(d_func, d_formals, d_formula);
   }
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class DefineNamedFunctionCommand */
@@ -349,314 +434,339 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
 DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
                                                        Expr func,
                                                        const std::vector<Expr>& formals,
-                                                       Expr formula) :
+                                                       Expr formula) throw() :
   DefineFunctionCommand(id, func, formals, formula) {
 }
 
-void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) {
+void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   this->DefineFunctionCommand::invoke(smtEngine);
   if(!d_func.isNull() && d_func.getType().isBoolean()) {
-    smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY,
-                                                               d_func));
+    smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func));
   }
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class Simplify */
 
-SimplifyCommand::SimplifyCommand(Expr term) :
+SimplifyCommand::SimplifyCommand(Expr term) throw() :
   d_term(term) {
 }
 
-Expr SimplifyCommand::getTerm() const {
+Expr SimplifyCommand::getTerm() const throw() {
   return d_term;
 }
 
-void SimplifyCommand::invoke(SmtEngine* smtEngine) {
+void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
   d_result = smtEngine->simplify(d_term);
+  d_commandStatus = CommandSuccess::instance();
 }
 
-Expr SimplifyCommand::getResult() const {
+Expr SimplifyCommand::getResult() const throw() {
   return d_result;
 }
 
-void SimplifyCommand::printResult(std::ostream& out) const {
-  out << d_result << endl;
+void SimplifyCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
 }
 
 /* class GetValueCommand */
 
-GetValueCommand::GetValueCommand(Expr term) :
+GetValueCommand::GetValueCommand(Expr term) throw() :
   d_term(term) {
 }
 
-Expr GetValueCommand::getTerm() const {
+Expr GetValueCommand::getTerm() const throw() {
   return d_term;
 }
 
-void GetValueCommand::invoke(SmtEngine* smtEngine) {
+void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
   d_result = d_term.getExprManager()->mkExpr(kind::TUPLE, d_term,
                                              smtEngine->getValue(d_term));
+  d_commandStatus = CommandSuccess::instance();
 }
 
-Expr GetValueCommand::getResult() const {
+Expr GetValueCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetValueCommand::printResult(std::ostream& out) const {
-  out << d_result << endl;
+void GetValueCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
 }
 
 /* class GetAssignmentCommand */
 
-GetAssignmentCommand::GetAssignmentCommand() {
+GetAssignmentCommand::GetAssignmentCommand() throw() {
 }
 
-void GetAssignmentCommand::invoke(SmtEngine* smtEngine) {
-  d_result = smtEngine->getAssignment();
+void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->getAssignment();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
-SExpr GetAssignmentCommand::getResult() const {
+SExpr GetAssignmentCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetAssignmentCommand::printResult(std::ostream& out) const {
-  out << d_result << endl;
+void GetAssignmentCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
 }
 
 /* class GetProofCommand */
 
-GetProofCommand::GetProofCommand() {
+GetProofCommand::GetProofCommand() throw() {
 }
 
-void GetProofCommand::invoke(SmtEngine* smtEngine) {
-  d_result = smtEngine->getProof();
+void GetProofCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->getProof();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
-Proof* GetProofCommand::getResult() const {
+Proof* GetProofCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetProofCommand::printResult(std::ostream& out) const {
-  d_result->toStream(out);
+void GetProofCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    d_result->toStream(out);
+  }
 }
 
 /* class GetAssertionsCommand */
 
-GetAssertionsCommand::GetAssertionsCommand() {
+GetAssertionsCommand::GetAssertionsCommand() throw() {
 }
 
-void GetAssertionsCommand::invoke(SmtEngine* smtEngine) {
-  stringstream ss;
-  const vector<Expr> v = smtEngine->getAssertions();
-  copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
-  d_result = ss.str();
+void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    stringstream ss;
+    const vector<Expr> v = smtEngine->getAssertions();
+    copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
+    d_result = ss.str();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
-std::string GetAssertionsCommand::getResult() const {
+std::string GetAssertionsCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetAssertionsCommand::printResult(std::ostream& out) const {
-  out << d_result;
+void GetAssertionsCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result;
+  }
 }
 
 /* class SetBenchmarkStatusCommand */
 
-SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
+SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
   d_status(status) {
 }
 
-BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const {
+BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
   return d_status;
 }
 
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
-  stringstream ss;
-  ss << d_status;
-  SExpr status = ss.str();
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
+    stringstream ss;
+    ss << d_status;
+    SExpr status = ss.str();
     smtEngine->setInfo(":status", status);
-    //d_result = "success";
-  } catch(ModalException&) {
-    d_result = "error";
-  } catch(BadOptionException&) {
-    // should not happen
-    d_result = "error";
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
 /* class SetBenchmarkLogicCommand */
 
-SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) :
+SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
   d_logic(logic) {
 }
 
-std::string SetBenchmarkLogicCommand::getLogic() const {
+std::string SetBenchmarkLogicCommand::getLogic() const throw() {
   return d_logic;
 }
 
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->setLogic(d_logic);
-    //d_result = "success";
-  } catch(ModalException&) {
-    d_result = "error";
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
 /* class SetInfoCommand */
 
-SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) :
+SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
   d_flag(flag),
   d_sexpr(sexpr) {
 }
 
-std::string SetInfoCommand::getFlag() const {
+std::string SetInfoCommand::getFlag() const throw() {
   return d_flag;
 }
 
-SExpr SetInfoCommand::getSExpr() const {
+SExpr SetInfoCommand::getSExpr() const throw() {
   return d_sexpr;
 }
 
-void SetInfoCommand::invoke(SmtEngine* smtEngine) {
+void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->setInfo(d_flag, d_sexpr);
-    //d_result = "success";
-  } catch(ModalException&) {
-    d_result = "error";
+    d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {
-    d_result = "unsupported";
-  }
-}
-
-std::string SetInfoCommand::getResult() const {
-  return d_result;
-}
-
-void SetInfoCommand::printResult(std::ostream& out) const {
-  if(d_result != "") {
-    out << d_result << endl;
+    d_commandStatus = new CommandUnsupported();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
 /* class GetInfoCommand */
 
-GetInfoCommand::GetInfoCommand(std::string flag) :
+GetInfoCommand::GetInfoCommand(std::string flag) throw() :
   d_flag(flag) {
 }
 
-std::string GetInfoCommand::getFlag() const {
+std::string GetInfoCommand::getFlag() const throw() {
   return d_flag;
 }
 
-void GetInfoCommand::invoke(SmtEngine* smtEngine) {
+void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     stringstream ss;
     ss << smtEngine->getInfo(d_flag);
     d_result = ss.str();
+    d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {
-    d_result = "unsupported";
+    d_commandStatus = new CommandUnsupported();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
-std::string GetInfoCommand::getResult() const {
+std::string GetInfoCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetInfoCommand::printResult(std::ostream& out) const {
-  if(d_result != "") {
+void GetInfoCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else if(d_result != "") {
     out << d_result << endl;
   }
 }
 
 /* class SetOptionCommand */
 
-SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) :
+SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
   d_flag(flag),
   d_sexpr(sexpr) {
 }
 
-std::string SetOptionCommand::getFlag() const {
+std::string SetOptionCommand::getFlag() const throw() {
   return d_flag;
 }
 
-SExpr SetOptionCommand::getSExpr() const {
+SExpr SetOptionCommand::getSExpr() const throw() {
   return d_sexpr;
 }
 
-void SetOptionCommand::invoke(SmtEngine* smtEngine) {
+void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->setOption(d_flag, d_sexpr);
-    //d_result = "success";
-  } catch(ModalException&) {
-    d_result = "error";
+    d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {
-    d_result = "unsupported";
-  }
-}
-
-std::string SetOptionCommand::getResult() const {
-  return d_result;
-}
-
-void SetOptionCommand::printResult(std::ostream& out) const {
-  if(d_result != "") {
-    out << d_result << endl;
+    d_commandStatus = new CommandUnsupported();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
 /* class GetOptionCommand */
 
-GetOptionCommand::GetOptionCommand(std::string flag) :
+GetOptionCommand::GetOptionCommand(std::string flag) throw() :
   d_flag(flag) {
 }
 
-std::string GetOptionCommand::getFlag() const {
+std::string GetOptionCommand::getFlag() const throw() {
   return d_flag;
 }
 
-void GetOptionCommand::invoke(SmtEngine* smtEngine) {
+void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     d_result = smtEngine->getOption(d_flag).getValue();
+    d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {
-    d_result = "unsupported";
+    d_commandStatus = new CommandUnsupported();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
-std::string GetOptionCommand::getResult() const {
+std::string GetOptionCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetOptionCommand::printResult(std::ostream& out) const {
-  if(d_result != "") {
+void GetOptionCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else if(d_result != "") {
     out << d_result << endl;
   }
 }
 
 /* class DatatypeDeclarationCommand */
 
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) :
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
   d_datatypes() {
   d_datatypes.push_back(datatype);
 }
 
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) :
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() :
   d_datatypes(datatypes) {
 }
 
 const std::vector<DatatypeType>&
-DatatypeDeclarationCommand::getDatatypes() const {
+DatatypeDeclarationCommand::getDatatypes() const throw() {
   return d_datatypes;
 }
 
-void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
+void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out,
-                         BenchmarkStatus status) {
+                         BenchmarkStatus status) throw() {
   switch(status) {
 
   case SMT_SATISFIABLE:
diff --git a/src/expr/command.h b/src/expr/command.h
index b686025fe..cf8c1b615 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -41,9 +41,12 @@ namespace CVC4 {
 
 class SmtEngine;
 class Command;
+class CommandStatus;
 
-std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
 
 /** The status an SMT benchmark can have */
 enum BenchmarkStatus {
@@ -56,21 +59,156 @@ enum BenchmarkStatus {
 };
 
 std::ostream& operator<<(std::ostream& out,
-                         BenchmarkStatus status) CVC4_PUBLIC;
+                         BenchmarkStatus status) throw() CVC4_PUBLIC;
+
+/**
+ * IOStream manipulator to print success messages or not.
+ *
+ *   out << Command::printsuccess(false) << CommandSuccess();
+ *
+ * prints nothing, but
+ *
+ *   out << Command::printsuccess(true) << CommandSuccess();
+ *
+ * prints a success message (in a manner appropriate for the current
+ * output language).
+ */
+class CVC4_PUBLIC CommandPrintSuccess {
+  /**
+   * The allocated index in ios_base for our depth setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default setting, for ostreams that haven't yet had a
+   * setdepth() applied to them.
+   */
+  static const int s_defaultPrintSuccess = false;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  bool d_printSuccess;
+
+public:
+  /**
+   * Construct a CommandPrintSuccess with the given setting.
+   */
+  CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {}
+
+  inline void applyPrintSuccess(std::ostream& out) throw() {
+    out.iword(s_iosIndex) = d_printSuccess;
+  }
+
+  static inline bool getPrintSuccess(std::ostream& out) throw() {
+    return out.iword(s_iosIndex);
+  }
+
+  static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() {
+    out.iword(s_iosIndex) = printSuccess;
+  }
+
+  /**
+   * Set the print-success state on the output stream for the current
+   * stack scope.  This makes sure the old state is reset on the
+   * stream after normal OR exceptional exit from the scope, using the
+   * RAII C++ idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    bool d_oldPrintSuccess;
+
+  public:
+
+    inline Scope(std::ostream& out, bool printSuccess) throw() :
+      d_out(out),
+      d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) {
+      CommandPrintSuccess::setPrintSuccess(out, printSuccess);
+    }
+
+    inline ~Scope() throw() {
+      CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess);
+    }
+
+  };/* class CommandPrintSuccess::Scope */
+
+};/* class CommandPrintSuccess */
+
+/**
+ * Sets the default print-success setting when pretty-printing an Expr
+ * to an ostream.  Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::setdepth(n) << e << endl;
+ *
+ * The depth stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() {
+  cps.applyPrintSuccess(out);
+  return out;
+}
+
+class CVC4_PUBLIC CommandStatus {
+protected:
+  // shouldn't construct a CommandStatus (use a derived class)
+  CommandStatus() throw() {}
+public:
+  virtual ~CommandStatus() throw() {}
+  void toStream(std::ostream& out,
+                OutputLanguage language = language::output::LANG_AST) const throw();
+};/* class CommandStatus */
+
+class CVC4_PUBLIC CommandSuccess : public CommandStatus {
+  static const CommandSuccess* s_instance;
+public:
+  static const CommandSuccess* instance() throw() { return s_instance; }
+};/* class CommandSuccess */
+
+class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
+};/* class CommandSuccess */
+
+class CVC4_PUBLIC CommandFailure : public CommandStatus {
+  std::string d_message;
+public:
+  CommandFailure(std::string message) throw() : d_message(message) {}
+  ~CommandFailure() throw() {}
+  std::string getMessage() const throw() { return d_message; }
+};/* class CommandFailure */
 
 class CVC4_PUBLIC Command {
+protected:
+  /**
+   * This field contains a command status if the command has been
+   * invoked, or NULL if it has not.  This field is either a
+   * dynamically-allocated pointer, or it's a pointer to the singleton
+   * CommandSuccess instance.  Doing so is somewhat asymmetric, but
+   * it avoids the need to dynamically allocate memory in the common
+   * case of a successful command.
+   */
+  const CommandStatus* d_commandStatus;
+
 public:
-  virtual ~Command() {}
+  typedef CommandPrintSuccess printsuccess;
+
+  Command() throw();
+  virtual ~Command() throw();
 
-  virtual void invoke(SmtEngine* smtEngine) = 0;
-  virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
+  virtual void invoke(SmtEngine* smtEngine) throw() = 0;
+  virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
 
   virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false,
-                        OutputLanguage language = language::output::LANG_AST) const;
+                        OutputLanguage language = language::output::LANG_AST) const throw();
+
+  std::string toString() const throw();
+
+  /** Either the command hasn't run yet, or it completed successfully. */
+  bool ok() const throw();
 
-  std::string toString() const;
+  /** Get the command status (it's NULL if we haven't run yet). */
+  const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
 
-  virtual void printResult(std::ostream& out) const;
+  virtual void printResult(std::ostream& out) const throw();
 
 };/* class Command */
 
@@ -82,45 +220,51 @@ class CVC4_PUBLIC EmptyCommand : public Command {
 protected:
   std::string d_name;
 public:
-  EmptyCommand(std::string name = "");
-  std::string getName() const;
-  void invoke(SmtEngine* smtEngine);
+  EmptyCommand(std::string name = "") throw();
+  ~EmptyCommand() throw() {}
+  std::string getName() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class EmptyCommand */
 
 class CVC4_PUBLIC AssertCommand : public Command {
 protected:
   BoolExpr d_expr;
 public:
-  AssertCommand(const BoolExpr& e);
-  BoolExpr getExpr() const;
-  void invoke(SmtEngine* smtEngine);
+  AssertCommand(const BoolExpr& e) throw();
+  ~AssertCommand() throw() {}
+  BoolExpr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command {
 public:
-  void invoke(SmtEngine* smtEngine);
+  ~PushCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class PushCommand */
 
 class CVC4_PUBLIC PopCommand : public Command {
 public:
-  void invoke(SmtEngine* smtEngine);
+  ~PopCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class PopCommand */
 
 class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
 protected:
   std::string d_symbol;
 public:
-  DeclarationDefinitionCommand(const std::string& id);
-  std::string getSymbol() const;
+  DeclarationDefinitionCommand(const std::string& id) throw();
+  ~DeclarationDefinitionCommand() throw() {}
+  std::string getSymbol() const throw();
 };/* class DeclarationDefinitionCommand */
 
 class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand {
 protected:
   Type d_type;
 public:
-  DeclareFunctionCommand(const std::string& id, Type type);
-  Type getType() const;
-  void invoke(SmtEngine* smtEngine);
+  DeclareFunctionCommand(const std::string& id, Type type) throw();
+  ~DeclareFunctionCommand() throw() {}
+  Type getType() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DeclareFunctionCommand */
 
 class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
@@ -128,10 +272,11 @@ protected:
   size_t d_arity;
   Type d_type;
 public:
-  DeclareTypeCommand(const std::string& id, size_t arity, Type t);
-  size_t getArity() const;
-  Type getType() const;
-  void invoke(SmtEngine* smtEngine);
+  DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw();
+  ~DeclareTypeCommand() throw() {}
+  size_t getArity() const throw();
+  Type getType() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DeclareTypeCommand */
 
 class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
@@ -139,11 +284,12 @@ protected:
   std::vector<Type> d_params;
   Type d_type;
 public:
-  DefineTypeCommand(const std::string& id, Type t);
-  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t);
-  const std::vector<Type>& getParameters() const;
-  Type getType() const;
-  void invoke(SmtEngine* smtEngine);
+  DefineTypeCommand(const std::string& id, Type t) throw();
+  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw();
+  ~DefineTypeCommand() throw() {}
+  const std::vector<Type>& getParameters() const throw();
+  Type getType() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DefineTypeCommand */
 
 class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
@@ -152,13 +298,14 @@ protected:
   std::vector<Expr> d_formals;
   Expr d_formula;
 public:
-  DefineFunctionCommand(const std::string& id, Expr func, Expr formula);
+  DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw();
   DefineFunctionCommand(const std::string& id, Expr func,
-                        const std::vector<Expr>& formals, Expr formula);
-  Expr getFunction() const;
-  const std::vector<Expr>& getFormals() const;
-  Expr getFormula() const;
-  void invoke(SmtEngine* smtEngine);
+                        const std::vector<Expr>& formals, Expr formula) throw();
+  ~DefineFunctionCommand() throw() {}
+  Expr getFunction() const throw();
+  const std::vector<Expr>& getFormals() const throw();
+  Expr getFormula() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DefineFunctionCommand */
 
 /**
@@ -169,8 +316,8 @@ public:
 class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
 public:
   DefineNamedFunctionCommand(const std::string& id, Expr func,
-                             const std::vector<Expr>& formals, Expr formula);
-  void invoke(SmtEngine* smtEngine);
+                             const std::vector<Expr>& formals, Expr formula) throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DefineNamedFunctionCommand */
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -178,12 +325,13 @@ protected:
   BoolExpr d_expr;
   Result d_result;
 public:
-  CheckSatCommand();
-  CheckSatCommand(const BoolExpr& expr);
-  BoolExpr getExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  Result getResult() const;
-  void printResult(std::ostream& out) const;
+  CheckSatCommand() throw();
+  CheckSatCommand(const BoolExpr& expr) throw();
+  ~CheckSatCommand() throw() {}
+  BoolExpr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Result getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class CheckSatCommand */
 
 class CVC4_PUBLIC QueryCommand : public Command {
@@ -191,11 +339,12 @@ protected:
   BoolExpr d_expr;
   Result d_result;
 public:
-  QueryCommand(const BoolExpr& e);
-  BoolExpr getExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  Result getResult() const;
-  void printResult(std::ostream& out) const;
+  QueryCommand(const BoolExpr& e) throw();
+  ~QueryCommand() throw() {}
+  BoolExpr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Result getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class QueryCommand */
 
 // this is TRANSFORM in the CVC presentation language
@@ -204,11 +353,12 @@ protected:
   Expr d_term;
   Expr d_result;
 public:
-  SimplifyCommand(Expr term);
-  Expr getTerm() const;
-  void invoke(SmtEngine* smtEngine);
-  Expr getResult() const;
-  void printResult(std::ostream& out) const;
+  SimplifyCommand(Expr term) throw();
+  ~SimplifyCommand() throw() {}
+  Expr getTerm() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Expr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class SimplifyCommand */
 
 class CVC4_PUBLIC GetValueCommand : public Command {
@@ -216,75 +366,77 @@ protected:
   Expr d_term;
   Expr d_result;
 public:
-  GetValueCommand(Expr term);
-  Expr getTerm() const;
-  void invoke(SmtEngine* smtEngine);
-  Expr getResult() const;
-  void printResult(std::ostream& out) const;
+  GetValueCommand(Expr term) throw();
+  ~GetValueCommand() throw() {}
+  Expr getTerm() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Expr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetValueCommand */
 
 class CVC4_PUBLIC GetAssignmentCommand : public Command {
 protected:
   SExpr d_result;
 public:
-  GetAssignmentCommand();
-  void invoke(SmtEngine* smtEngine);
-  SExpr getResult() const;
-  void printResult(std::ostream& out) const;
+  GetAssignmentCommand() throw();
+  ~GetAssignmentCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  SExpr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetAssignmentCommand */
 
 class CVC4_PUBLIC GetProofCommand : public Command {
 protected:
   Proof* d_result;
 public:
-  GetProofCommand();
-  void invoke(SmtEngine* smtEngine);
-  Proof* getResult() const;
-  void printResult(std::ostream& out) const;
+  GetProofCommand() throw();
+  ~GetProofCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  Proof* getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetProofCommand */
 
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
 protected:
   std::string d_result;
 public:
-  GetAssertionsCommand();
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  GetAssertionsCommand() throw();
+  ~GetAssertionsCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  std::string getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetAssertionsCommand */
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
 protected:
-  std::string d_result;
   BenchmarkStatus d_status;
 public:
-  SetBenchmarkStatusCommand(BenchmarkStatus status);
-  BenchmarkStatus getStatus() const;
-  void invoke(SmtEngine* smtEngine);
+  SetBenchmarkStatusCommand(BenchmarkStatus status) throw();
+  ~SetBenchmarkStatusCommand() throw() {}
+  BenchmarkStatus getStatus() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetBenchmarkStatusCommand */
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
 protected:
-  std::string d_result;
   std::string d_logic;
 public:
-  SetBenchmarkLogicCommand(std::string logic);
-  std::string getLogic() const;
-  void invoke(SmtEngine* smtEngine);
+  SetBenchmarkLogicCommand(std::string logic) throw();
+  ~SetBenchmarkLogicCommand() throw() {}
+  std::string getLogic() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command {
 protected:
   std::string d_flag;
   SExpr d_sexpr;
-  std::string d_result;
 public:
-  SetInfoCommand(std::string flag, const SExpr& sexpr);
-  std::string getFlag() const;
-  SExpr getSExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  SetInfoCommand(std::string flag, const SExpr& sexpr) throw();
+  ~SetInfoCommand() throw() {}
+  std::string getFlag() const throw();
+  SExpr getSExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetInfoCommand */
 
 class CVC4_PUBLIC GetInfoCommand : public Command {
@@ -292,25 +444,24 @@ protected:
   std::string d_flag;
   std::string d_result;
 public:
-  GetInfoCommand(std::string flag);
-  std::string getFlag() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  GetInfoCommand(std::string flag) throw();
+  ~GetInfoCommand() throw() {}
+  std::string getFlag() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  std::string getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetInfoCommand */
 
 class CVC4_PUBLIC SetOptionCommand : public Command {
 protected:
   std::string d_flag;
   SExpr d_sexpr;
-  std::string d_result;
 public:
-  SetOptionCommand(std::string flag, const SExpr& sexpr);
-  std::string getFlag() const;
-  SExpr getSExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  SetOptionCommand(std::string flag, const SExpr& sexpr) throw();
+  ~SetOptionCommand() throw() {}
+  std::string getFlag() const throw();
+  SExpr getSExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetOptionCommand */
 
 class CVC4_PUBLIC GetOptionCommand : public Command {
@@ -318,35 +469,39 @@ protected:
   std::string d_flag;
   std::string d_result;
 public:
-  GetOptionCommand(std::string flag);
-  std::string getFlag() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  GetOptionCommand(std::string flag) throw();
+  ~GetOptionCommand() throw() {}
+  std::string getFlag() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  std::string getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetOptionCommand */
 
 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
 private:
   std::vector<DatatypeType> d_datatypes;
 public:
-  DatatypeDeclarationCommand(const DatatypeType& datatype);
-  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
-  const std::vector<DatatypeType>& getDatatypes() const;
-  void invoke(SmtEngine* smtEngine);
+  DatatypeDeclarationCommand(const DatatypeType& datatype) throw();
+  ~DatatypeDeclarationCommand() throw() {}
+  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
+  const std::vector<DatatypeType>& getDatatypes() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DatatypeDeclarationCommand */
 
 class CVC4_PUBLIC QuitCommand : public Command {
 public:
-  QuitCommand();
-  void invoke(SmtEngine* smtEngine);
+  QuitCommand() throw();
+  ~QuitCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class QuitCommand */
 
 class CVC4_PUBLIC CommentCommand : public Command {
   std::string d_comment;
 public:
-  CommentCommand(std::string comment);
-  std::string getComment() const;
-  void invoke(SmtEngine* smtEngine);
+  CommentCommand(std::string comment) throw();
+  ~CommentCommand() throw() {}
+  std::string getComment() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class CommentCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command {
@@ -356,27 +511,28 @@ private:
   /** Next command to be executed */
   unsigned int d_index;
 public:
-  CommandSequence();
-  ~CommandSequence();
+  CommandSequence() throw();
+  ~CommandSequence() throw();
 
-  void addCommand(Command* cmd);
+  void addCommand(Command* cmd) throw();
 
-  void invoke(SmtEngine* smtEngine);
-  void invoke(SmtEngine* smtEngine, std::ostream& out);
+  void invoke(SmtEngine* smtEngine) throw();
+  void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
 
   typedef std::vector<Command*>::iterator iterator;
   typedef std::vector<Command*>::const_iterator const_iterator;
 
-  const_iterator begin() const;
-  const_iterator end() const;
+  const_iterator begin() const throw();
+  const_iterator end() const throw();
 
-  iterator begin();
-  iterator end();
+  iterator begin() throw();
+  iterator end() throw();
 
 };/* class CommandSequence */
 
 class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
 public:
+  ~DeclarationSequence() throw() {}
 };/* class DeclarationSequence */
 
 }/* CVC4 namespace */
diff --git a/src/expr/command.i b/src/expr/command.i
index 3a029b785..a4bf5473e 100644
--- a/src/expr/command.i
+++ b/src/expr/command.i
@@ -2,11 +2,11 @@
 #include "expr/command.h"
 %}
 
-%ignore CVC4::operator<<(std::ostream&, const Command&);
-%ignore CVC4::operator<<(std::ostream&, const Command*);
-%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status);
+%ignore CVC4::operator<<(std::ostream&, const Command&) throw();
+%ignore CVC4::operator<<(std::ostream&, const Command*) throw();
+%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw();
 
-%rename(beginConst) CVC4::CommandSequence::begin() const;
-%rename(endConst) CVC4::CommandSequence::end() const;
+%rename(beginConst) CVC4::CommandSequence::begin() const throw();
+%rename(endConst) CVC4::CommandSequence::end() const throw();
 
 %include "expr/command.h"
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 619fd5280..29aa1a737 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -56,31 +56,28 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) {
   return out << e.getNode();
 }
 
-TypeCheckingException::TypeCheckingException(const TypeCheckingException& t)
-: Exception(t.d_msg), d_expr(new Expr(t.getExpression()))
-  {}
-
+TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) throw() :
+  Exception(t.d_msg), d_expr(new Expr(t.getExpression())) {
+}
 
-TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message)
-: Exception(message), d_expr(new Expr(expr))
-{
+TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) throw() :
+  Exception(message), d_expr(new Expr(expr)) {
 }
 
 TypeCheckingException::TypeCheckingException(ExprManager* em,
-                                             const TypeCheckingExceptionPrivate* exc)
-: Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode())))
-{
+                                             const TypeCheckingExceptionPrivate* exc) throw() :
+  Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode()))) {
 }
 
-TypeCheckingException::~TypeCheckingException() throw () {
+TypeCheckingException::~TypeCheckingException() throw() {
   delete d_expr;
 }
 
-void TypeCheckingException::toStream(std::ostream& os) const {
+void TypeCheckingException::toStream(std::ostream& os) const throw() {
   os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr;
 }
 
-Expr TypeCheckingException::getExpression() const {
+Expr TypeCheckingException::getExpression() const throw() {
   return *d_expr;
 }
 
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 616a7c8ff..b54ec20d4 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -81,32 +81,32 @@ private:
 
 protected:
 
-  TypeCheckingException() : Exception() {}
-  TypeCheckingException(const Expr& expr, std::string message);
+  TypeCheckingException() throw() : Exception() {}
+  TypeCheckingException(const Expr& expr, std::string message) throw();
   TypeCheckingException(ExprManager* em,
-                        const TypeCheckingExceptionPrivate* exc);
+                        const TypeCheckingExceptionPrivate* exc) throw();
 
 public:
 
   /** Copy constructor */
-  TypeCheckingException(const TypeCheckingException& t);
+  TypeCheckingException(const TypeCheckingException& t) throw();
 
   /** Destructor */
-  ~TypeCheckingException() throw ();
+  ~TypeCheckingException() throw();
 
   /**
    * Get the Expr that caused the type-checking to fail.
    *
    * @return the expr
    */
-  Expr getExpression() const;
+  Expr getExpression() const throw();
 
   /**
    * 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;
+  void toStream(std::ostream& out) const throw();
 
   friend class ExprManager;
 };/* class TypeCheckingException */
@@ -457,9 +457,13 @@ public:
    *
    *   // let a, b, c, and d be variables of sort U
    *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
-   *   out << e;
+   *   out << printtypes(true) << e;
    *
    * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
+   *
+   *   out << printtypes(false) << [same expr as above]
+   *
+   * gives "(OR a b (AND c (NOT d)))"
    */
   typedef expr::ExprPrintTypes printtypes;
 
@@ -824,7 +828,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 828 "${template}"
+#line 832 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 586d0cb13..695e572ab 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -26,7 +26,7 @@ using namespace std;
 namespace CVC4 {
 
 TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
-                                                           std::string message) :
+                                                           std::string message) throw() :
   Exception(message),
   d_node(new Node(node)) {
 }
@@ -35,11 +35,11 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
   delete d_node;
 }
 
-void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const {
+void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() {
   os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
 }
 
-Node TypeCheckingExceptionPrivate::getNode() const {
+NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const throw() {
   return *d_node;
 }
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 2751c96a8..57b02b05b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -65,7 +65,7 @@ private:
 
 protected:
 
-  TypeCheckingExceptionPrivate() : Exception() {}
+  TypeCheckingExceptionPrivate() throw() : Exception() {}
 
 public:
 
@@ -74,7 +74,7 @@ public:
    * @param node the problematic node
    * @param message the message explaining the failure
    */
-  TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message);
+  TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message) throw();
 
   /** Destructor */
   ~TypeCheckingExceptionPrivate() throw ();
@@ -83,14 +83,14 @@ public:
    * Get the Node that caused the type-checking to fail.
    * @return the node
    */
-  NodeTemplate<true> getNode() const;
+  NodeTemplate<true> getNode() const throw();
 
   /**
    * 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;
+  void toStream(std::ostream& out) const throw();
 
 };/* class TypeCheckingExceptionPrivate */
 
diff --git a/src/expr/type.i b/src/expr/type.i
index 314903342..acde96955 100644
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -18,6 +18,7 @@
 %rename(toIntegerType) CVC4::Type::operator IntegerType() const;
 %rename(toRealType) CVC4::Type::operator RealType() const;
 %rename(toPseudobooleanType) CVC4::Type::operator PseudobooleanType() const;
+%rename(toStringType) CVC4::Type::operator StringType() const;
 %rename(toBitVectorType) CVC4::Type::operator BitVectorType() const;
 %rename(toFunctionType) CVC4::Type::operator FunctionType() const;
 %rename(toTupleType) CVC4::Type::operator TupleType() const;