Removing throw specifiers from internal Printer hierarchy. (#1393)

12 files changed, 535 insertions, 255 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 35b39914a..be95c947d 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -34,8 +34,9 @@ namespace CVC4 {
 namespace printer {
 namespace ast {
 
-void AstPrinter::toStream(std::ostream& out, TNode n,
-                          int toDepth, bool types, size_t dag) const throw() {
+void AstPrinter::toStream(
+    std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
+{
   if(dag != 0) {
     DagificationVisitor dv(dag);
     NodeVisitor<DagificationVisitor> visitor;
@@ -68,8 +69,11 @@ void AstPrinter::toStream(std::ostream& out, TNode n,
   }
 }
 
-void AstPrinter::toStream(std::ostream& out, TNode n,
-                          int toDepth, bool types) const throw() {
+void AstPrinter::toStream(std::ostream& out,
+                          TNode n,
+                          int toDepth,
+                          bool types) const
+{
   // null
   if(n.getKind() == kind::NULL_EXPR) {
     out << "null";
@@ -126,10 +130,14 @@ void AstPrinter::toStream(std::ostream& out, TNode n,
 }/* AstPrinter::toStream(TNode) */
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) throw();
-
-void AstPrinter::toStream(std::ostream& out, const Command* c,
-                          int toDepth, bool types, size_t dag) const throw() {
+static bool tryToStream(std::ostream& out, const Command* c);
+
+void AstPrinter::toStream(std::ostream& out,
+                          const Command* c,
+                          int toDepth,
+                          bool types,
+                          size_t dag) const
+{
   expr::ExprSetDepth::Scope sdScope(out, toDepth);
   expr::ExprPrintTypes::Scope ptScope(out, types);
   expr::ExprDag::Scope dagScope(out, dag);
@@ -173,10 +181,10 @@ void AstPrinter::toStream(std::ostream& out, const Command* c,
 }/* AstPrinter::toStream(Command*) */
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
-
-void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+static bool tryToStream(std::ostream& out, const CommandStatus* s);
 
+void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const
+{
   if(tryToStream<CommandSuccess>(out, s) ||
      tryToStream<CommandFailure>(out, s) ||
      tryToStream<CommandUnsupported>(out, s) ||
@@ -189,32 +197,38 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* AstPrinter::toStream(CommandStatus*) */
 
-void AstPrinter::toStream(std::ostream& out, const Model& m) const throw() {
+void AstPrinter::toStream(std::ostream& out, const Model& m) const
+{
   out << "Model()";
 }
 
-void AstPrinter::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
+void AstPrinter::toStream(std::ostream& out,
+                          const Model& m,
+                          const Command* c) const
+{
   // shouldn't be called; only the non-Command* version above should be
   Unreachable();
 }
 
-static void toStream(std::ostream& out, const EmptyCommand* c)  throw() {
+static void toStream(std::ostream& out, const EmptyCommand* c)
+{
   out << "EmptyCommand(" << c->getName() << ")";
 }
 
-static void toStream(std::ostream& out, const AssertCommand* c) throw() {
+static void toStream(std::ostream& out, const AssertCommand* c)
+{
   out << "Assert(" << c->getExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const PushCommand* c) throw() {
+static void toStream(std::ostream& out, const PushCommand* c)
+{
   out << "Push()";
 }
 
-static void toStream(std::ostream& out, const PopCommand* c) throw() {
-  out << "Pop()";
-}
+static void toStream(std::ostream& out, const PopCommand* c) { out << "Pop()"; }
 
-static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
+static void toStream(std::ostream& out, const CheckSatCommand* c)
+{
   Expr e = c->getExpr();
   if(e.isNull()) {
     out << "CheckSat()";
@@ -223,23 +237,28 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
   }
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c) throw() {
+static void toStream(std::ostream& out, const QueryCommand* c)
+{
   out << "Query(" << c->getExpr() << ')';
 }
 
-static void toStream(std::ostream& out, const ResetCommand* c) throw() {
+static void toStream(std::ostream& out, const ResetCommand* c)
+{
   out << "Reset()";
 }
 
-static void toStream(std::ostream& out, const ResetAssertionsCommand* c) throw() {
+static void toStream(std::ostream& out, const ResetAssertionsCommand* c)
+{
   out << "ResetAssertions()";
 }
 
-static void toStream(std::ostream& out, const QuitCommand* c) throw() {
+static void toStream(std::ostream& out, const QuitCommand* c)
+{
   out << "Quit()";
 }
 
-static void toStream(std::ostream& out, const DeclarationSequence* c) throw() {
+static void toStream(std::ostream& out, const DeclarationSequence* c)
+{
   out << "DeclarationSequence[" << endl;
   for(CommandSequence::const_iterator i = c->begin();
       i != c->end();
@@ -249,7 +268,8 @@ static void toStream(std::ostream& out, const DeclarationSequence* c) throw() {
   out << "]";
 }
 
-static void toStream(std::ostream& out, const CommandSequence* c) throw() {
+static void toStream(std::ostream& out, const CommandSequence* c)
+{
   out << "CommandSequence[" << endl;
   for(CommandSequence::const_iterator i = c->begin();
       i != c->end();
@@ -259,11 +279,13 @@ static void toStream(std::ostream& out, const CommandSequence* c) throw() {
   out << "]";
 }
 
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() {
+static void toStream(std::ostream& out, const DeclareFunctionCommand* c)
+{
   out << "Declare(" << c->getSymbol() << "," << c->getType() << ")";
 }
 
-static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() {
+static void toStream(std::ostream& out, const DefineFunctionCommand* c)
+{
   Expr func = c->getFunction();
   const std::vector<Expr>& formals = c->getFormals();
   Expr formula = c->getFormula();
@@ -276,12 +298,14 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw()
   out << "], << " << formula << " >> )";
 }
 
-static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
+static void toStream(std::ostream& out, const DeclareTypeCommand* c)
+{
   out << "DeclareType(" << c->getSymbol() << "," << c->getArity() << ","
       << c->getType() << ")";
 }
 
-static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
+static void toStream(std::ostream& out, const DefineTypeCommand* c)
+{
   const vector<Type>& params = c->getParameters();
   out << "DefineType(" << c->getSymbol() << ",[";
   if(params.size() > 0) {
@@ -292,58 +316,72 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
   out << "]," << c->getType() << ")";
 }
 
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() {
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c)
+{
   out << "DefineNamedFunction( ";
   toStream(out, static_cast<const DefineFunctionCommand*>(c));
   out << " )";
 }
 
-static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
+static void toStream(std::ostream& out, const SimplifyCommand* c)
+{
   out << "Simplify( << " << c->getTerm() << " >> )";
 }
 
-static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
+static void toStream(std::ostream& out, const GetValueCommand* c)
+{
   out << "GetValue( << ";
   const vector<Expr>& terms = c->getTerms();
   copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
   out << " >> )";
 }
 
-static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
+static void toStream(std::ostream& out, const GetModelCommand* c)
+{
   out << "GetModel()";
 }
 
-static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
+static void toStream(std::ostream& out, const GetAssignmentCommand* c)
+{
   out << "GetAssignment()";
 }
-static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
+static void toStream(std::ostream& out, const GetAssertionsCommand* c)
+{
   out << "GetAssertions()";
 }
-static void toStream(std::ostream& out, const GetProofCommand* c) throw() {
+static void toStream(std::ostream& out, const GetProofCommand* c)
+{
   out << "GetProof()";
 }
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c)
+{
   out << "SetBenchmarkStatus(" << c->getStatus() << ")";
 }
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() {
+static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c)
+{
   out << "SetBenchmarkLogic(" << c->getLogic() << ")";
 }
-static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
+static void toStream(std::ostream& out, const SetInfoCommand* c)
+{
   out << "SetInfo(" << c->getFlag() << ", " << c->getSExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
+static void toStream(std::ostream& out, const GetInfoCommand* c)
+{
   out << "GetInfo(" << c->getFlag() << ")";
 }
-static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
+static void toStream(std::ostream& out, const SetOptionCommand* c)
+{
   out << "SetOption(" << c->getFlag() << ", " << c->getSExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
+static void toStream(std::ostream& out, const GetOptionCommand* c)
+{
   out << "GetOption(" << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() {
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c)
+{
   const vector<DatatypeType>& datatypes = c->getDatatypes();
   out << "DatatypeDeclarationCommand([";
   for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
@@ -355,12 +393,14 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
   out << "])";
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c) throw() {
+static void toStream(std::ostream& out, const CommentCommand* c)
+{
   out << "CommentCommand([" << c->getComment() << "])";
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) throw() {
+static bool tryToStream(std::ostream& out, const Command* c)
+{
   if(typeid(*c) == typeid(T)) {
     toStream(out, dynamic_cast<const T*>(c));
     return true;
@@ -368,26 +408,31 @@ static bool tryToStream(std::ostream& out, const Command* c) throw() {
   return false;
 }
 
-static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
+static void toStream(std::ostream& out, const CommandSuccess* s)
+{
   if(Command::printsuccess::getPrintSuccess(out)) {
     out << "OK" << endl;
   }
 }
 
-static void toStream(std::ostream& out, const CommandInterrupted* s) throw() {
+static void toStream(std::ostream& out, const CommandInterrupted* s)
+{
   out << "INTERRUPTED" << endl;
 }
 
-static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
+static void toStream(std::ostream& out, const CommandUnsupported* s)
+{
   out << "UNSUPPORTED" << endl;
 }
 
-static void toStream(std::ostream& out, const CommandFailure* s) throw() {
+static void toStream(std::ostream& out, const CommandFailure* s)
+{
   out << s->getMessage() << endl;
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
+static bool tryToStream(std::ostream& out, const CommandStatus* s)
+{
   if(typeid(*s) == typeid(T)) {
     toStream(out, dynamic_cast<const T*>(s));
     return true;
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index 29c3981bf..1d790dd61 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -28,14 +28,26 @@ namespace printer {
 namespace ast {
 
 class AstPrinter : public CVC4::Printer {
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
-  void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
-public:
+ public:
   using CVC4::Printer::toStream;
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
-  void toStream(std::ostream& out, const CommandStatus* s) const throw();
-  void toStream(std::ostream& out, const Model& m) const throw();
+  void toStream(std::ostream& out,
+                TNode n,
+                int toDepth,
+                bool types,
+                size_t dag) const override;
+  void toStream(std::ostream& out,
+                const Command* c,
+                int toDepth,
+                bool types,
+                size_t dag) const override;
+  void toStream(std::ostream& out, const CommandStatus* s) const override;
+  void toStream(std::ostream& out, const Model& m) const override;
+
+ private:
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+  void toStream(std::ostream& out,
+                const Model& m,
+                const Command* c) const override;
 };/* class AstPrinter */
 
 }/* CVC4::printer::ast namespace */
@@ -43,4 +55,3 @@ public:
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PRINTER__AST_PRINTER_H */
-
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index cbfad67b5..f20cb7cce 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -42,7 +42,9 @@ namespace CVC4 {
 namespace printer {
 namespace cvc {
 
-void CvcPrinter::toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw() {
+void CvcPrinter::toStream(
+    std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
+{
   if(dag != 0) {
     DagificationVisitor dv(dag);
     NodeVisitor<DagificationVisitor> visitor;
@@ -72,7 +74,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int toDepth, bool types, s
   }
 }
 
-void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, bool bracket) const throw() {
+void CvcPrinter::toStream(
+    std::ostream& out, TNode n, int depth, bool types, bool bracket) const
+{
   if (depth == 0) {
     out << "(...)";
   } else {
@@ -935,10 +939,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
 }/* CvcPrinter::toStream(TNode) */
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) throw();
-
-void CvcPrinter::toStream(std::ostream& out, const Command* c,
-                           int toDepth, bool types, size_t dag) const throw() {
+static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode);
+
+void CvcPrinter::toStream(std::ostream& out,
+                          const Command* c,
+                          int toDepth,
+                          bool types,
+                          size_t dag) const
+{
   expr::ExprSetDepth::Scope sdScope(out, toDepth);
   expr::ExprPrintTypes::Scope ptScope(out, types);
   expr::ExprDag::Scope dagScope(out, dag);
@@ -984,10 +992,12 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
 }/* CvcPrinter::toStream(Command*) */
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw();
-
-void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+static bool tryToStream(std::ostream& out,
+                        const CommandStatus* s,
+                        bool cvc3Mode);
 
+void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const
+{
   if(tryToStream<CommandSuccess>(out, s, d_cvc3Mode) ||
      tryToStream<CommandFailure>(out, s, d_cvc3Mode) ||
      tryToStream<CommandUnsupported>(out, s, d_cvc3Mode) ||
@@ -1000,7 +1010,10 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* CvcPrinter::toStream(CommandStatus*) */
 
-void CvcPrinter::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
+void CvcPrinter::toStream(std::ostream& out,
+                          const Model& m,
+                          const Command* c) const
+{
   const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
@@ -1115,19 +1128,23 @@ void CvcPrinter::toStream(std::ostream& out, const Model& m, const Command* c) c
   }
 }
 
-static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode)
+{
   out << "ASSERT " << c->getExpr() << ";";
 }
 
-static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode)
+{
   out << "PUSH;";
 }
 
-static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode)
+{
   out << "POP;";
 }
 
-static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode)
+{
   Expr e = c->getExpr();
   if(cvc3Mode) {
     out << "PUSH; ";
@@ -1142,7 +1159,8 @@ static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode)
   }
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode)
+{
   Expr e = c->getExpr();
   if(cvc3Mode) {
     out << "PUSH; ";
@@ -1157,19 +1175,25 @@ static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode) th
   }
 }
 
-static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode)
+{
   out << "RESET;";
 }
 
-static void toStream(std::ostream& out, const ResetAssertionsCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const ResetAssertionsCommand* c,
+                     bool cvc3Mode)
+{
   out << "RESET ASSERTIONS;";
 }
 
-static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode)
+{
   //out << "EXIT;";
 }
 
-static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode)
+{
   for(CommandSequence::const_iterator i = c->begin();
       i != c->end();
       ++i) {
@@ -1177,7 +1201,10 @@ static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode)
   }
 }
 
-static void toStream(std::ostream& out, const DeclarationSequence* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const DeclarationSequence* c,
+                     bool cvc3Mode)
+{
   DeclarationSequence::const_iterator i = c->begin();
   for(;;) {
     DeclarationDefinitionCommand* dd =
@@ -1191,11 +1218,17 @@ static void toStream(std::ostream& out, const DeclarationSequence* c, bool cvc3M
   }
 }
 
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const DeclareFunctionCommand* c,
+                     bool cvc3Mode)
+{
   out << c->getSymbol() << " : " << c->getType() << ";";
 }
 
-static void toStream(std::ostream& out, const DefineFunctionCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const DefineFunctionCommand* c,
+                     bool cvc3Mode)
+{
   Expr func = c->getFunction();
   const vector<Expr>& formals = c->getFormals();
   Expr formula = c->getFormula();
@@ -1214,7 +1247,10 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c, bool cvc
   out << formula << ";";
 }
 
-static void toStream(std::ostream& out, const DeclareTypeCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const DeclareTypeCommand* c,
+                     bool cvc3Mode)
+{
   if(c->getArity() > 0) {
     //TODO?
     out << "ERROR: Don't know how to print parameterized type declaration "
@@ -1224,7 +1260,10 @@ static void toStream(std::ostream& out, const DeclareTypeCommand* c, bool cvc3Mo
   }
 }
 
-static void toStream(std::ostream& out, const DefineTypeCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const DefineTypeCommand* c,
+                     bool cvc3Mode)
+{
   if(c->getParameters().size() > 0) {
     out << "ERROR: Don't know how to print parameterized type definition "
            "in CVC language:" << endl << c->toString() << endl;
@@ -1233,15 +1272,20 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c, bool cvc3Mod
   }
 }
 
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const DefineNamedFunctionCommand* c,
+                     bool cvc3Mode)
+{
   toStream(out, static_cast<const DefineFunctionCommand*>(c), cvc3Mode);
 }
 
-static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode)
+{
   out << "TRANSFORM " << c->getTerm() << ";";
 }
 
-static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode)
+{
   const vector<Expr>& terms = c->getTerms();
   Assert(!terms.empty());
   out << "GET_VALUE ";
@@ -1249,35 +1293,53 @@ static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode)
   out << terms.back() << ";";
 }
 
-static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode)
+{
   out << "COUNTERMODEL;";
 }
 
-static void toStream(std::ostream& out, const GetAssignmentCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const GetAssignmentCommand* c,
+                     bool cvc3Mode)
+{
   out << "% (get-assignment)";
 }
 
-static void toStream(std::ostream& out, const GetAssertionsCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const GetAssertionsCommand* c,
+                     bool cvc3Mode)
+{
   out << "WHERE;";
 }
 
-static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode)
+{
   out << "DUMP_PROOF;";
 }
 
-static void toStream(std::ostream& out, const GetUnsatCoreCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const GetUnsatCoreCommand* c,
+                     bool cvc3Mode)
+{
   out << "DUMP_UNSAT_CORE;";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const SetBenchmarkStatusCommand* c,
+                     bool cvc3Mode)
+{
   out << "% (set-info :status " << c->getStatus() << ")";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const SetBenchmarkLogicCommand* c,
+                     bool cvc3Mode)
+{
   out << "OPTION \"logic\" \"" << c->getLogic() << "\";";
 }
 
-static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode)
+{
   out << "% (set-info " << c->getFlag() << " ";
   OutputLanguage language =
       cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
@@ -1285,21 +1347,31 @@ static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode)
   out << ")";
 }
 
-static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode)
+{
   out << "% (get-info " << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const SetOptionCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const SetOptionCommand* c,
+                     bool cvc3Mode)
+{
   out << "OPTION \"" << c->getFlag() << "\" ";
   SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4);
   out << ";";
 }
 
-static void toStream(std::ostream& out, const GetOptionCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const GetOptionCommand* c,
+                     bool cvc3Mode)
+{
   out << "% (get-option " << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const DatatypeDeclarationCommand* c,
+                     bool cvc3Mode)
+{
   const vector<DatatypeType>& datatypes = c->getDatatypes();
   //do not print tuple/datatype internal declarations
   if( datatypes.size()!=1 || ( !datatypes[0].getDatatype().isTuple() && !datatypes[0].getDatatype().isRecord() ) ){
@@ -1358,19 +1430,21 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, boo
   }
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode)
+{
   out << "% " << c->getComment();
 }
 
-static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) throw() {
-}
+static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) {}
 
-static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode)
+{
   out << "ECHO \"" << c->getOutput() << "\";";
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) throw() {
+static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode)
+{
   if(typeid(*c) == typeid(T)) {
     toStream(out, dynamic_cast<const T*>(c), cvc3Mode);
     return true;
@@ -1378,26 +1452,37 @@ static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) thro
   return false;
 }
 
-static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode)
+{
   if(Command::printsuccess::getPrintSuccess(out)) {
     out << "OK" << endl;
   }
 }
 
-static void toStream(std::ostream& out, const CommandUnsupported* s, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const CommandUnsupported* s,
+                     bool cvc3Mode)
+{
   out << "UNSUPPORTED" << endl;
 }
 
-static void toStream(std::ostream& out, const CommandInterrupted* s, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out,
+                     const CommandInterrupted* s,
+                     bool cvc3Mode)
+{
   out << "INTERRUPTED" << endl;
 }
 
-static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode) throw() {
+static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode)
+{
   out << s->getMessage() << endl;
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw() {
+static bool tryToStream(std::ostream& out,
+                        const CommandStatus* s,
+                        bool cvc3Mode)
+{
   if(typeid(*s) == typeid(T)) {
     toStream(out, dynamic_cast<const T*>(s), cvc3Mode);
     return true;
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 54ff3ea1d..ee25ad1f4 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -28,16 +28,29 @@ namespace printer {
 namespace cvc {
 
 class CvcPrinter : public CVC4::Printer {
-  bool d_cvc3Mode;
-
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw();
-  void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
-public:
+ public:
   using CVC4::Printer::toStream;
   CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) { }
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
-  void toStream(std::ostream& out, const CommandStatus* s) const throw();
+  void toStream(std::ostream& out,
+                TNode n,
+                int toDepth,
+                bool types,
+                size_t dag) const override;
+  void toStream(std::ostream& out,
+                const Command* c,
+                int toDepth,
+                bool types,
+                size_t dag) const override;
+  void toStream(std::ostream& out, const CommandStatus* s) const override;
+
+ private:
+  void toStream(
+      std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const;
+  void toStream(std::ostream& out,
+                const Model& m,
+                const Command* c) const override;
+
+  bool d_cvc3Mode;
 };/* class CvcPrinter */
 
 }/* CVC4::printer::cvc namespace */
@@ -45,4 +58,3 @@ public:
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PRINTER__CVC_PRINTER_H */
-
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index e50b1970f..2ccac5e9f 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -31,7 +31,8 @@ namespace CVC4 {
 
 Printer* Printer::d_printers[language::output::LANG_MAX];
 
-Printer* Printer::makePrinter(OutputLanguage lang) throw() {
+Printer* Printer::makePrinter(OutputLanguage lang)
+{
   using namespace CVC4::language::output;
 
   switch(lang) {
@@ -70,14 +71,15 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   }
 }/* Printer::makePrinter() */
 
-void Printer::toStreamSygus(std::ostream& out, TNode n) const throw()
+void Printer::toStreamSygus(std::ostream& out, TNode n) const
 {
   // no sygus-specific printing associated with this printer,
   // just print the original term
   toStream(out, n, -1, false, 1);
 }
 
-void Printer::toStream(std::ostream& out, const Model& m) const throw() {
+void Printer::toStream(std::ostream& out, const Model& m) const
+{
   for(size_t i = 0; i < m.getNumCommands(); ++i) {
     const Command* cmd = m.getCommand(i);
     const DeclareFunctionCommand* dfc = dynamic_cast<const DeclareFunctionCommand*>(cmd);
@@ -88,7 +90,8 @@ void Printer::toStream(std::ostream& out, const Model& m) const throw() {
   }
 }/* Printer::toStream(Model) */
 
-void Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() {
+void Printer::toStream(std::ostream& out, const UnsatCore& core) const
+{
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
     AssertCommand cmd(*i);
     toStream(out, &cmd, -1, false, -1);
@@ -96,7 +99,8 @@ void Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() {
   }
 }/* Printer::toStream(UnsatCore) */
 
-Printer* Printer::getPrinter(OutputLanguage lang) throw() {
+Printer* Printer::getPrinter(OutputLanguage lang)
+{
   if(lang == language::output::LANG_AUTO) {
   // Infer the language to use for output.
   //
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 9baeeb8b6..f5e05a848 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -35,7 +35,7 @@ class Printer {
   static Printer* d_printers[language::output::LANG_MAX];
 
   /** Make a Printer for a given OutputLanguage */
-  static Printer* makePrinter(OutputLanguage lang) throw();
+  static Printer* makePrinter(OutputLanguage lang);
 
   // disallow copy, assignment
   Printer(const Printer&) CVC4_UNDEFINED;
@@ -43,37 +43,49 @@ class Printer {
 
 protected:
   // derived classes can construct, but no one else.
-  Printer() throw() {}
-  virtual ~Printer() {}
-
-  /** write model response to command */
-  virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0;
-
-  /** write model response to command using another language printer */
-  void toStreamUsing(OutputLanguage lang, std::ostream& out, const Model& m, const Command* c) const throw() {
-    getPrinter(lang)->toStream(out, m, c);
+ Printer() {}
+ virtual ~Printer() {}
+
+ /** write model response to command */
+ virtual void toStream(std::ostream& out,
+                       const Model& m,
+                       const Command* c) const = 0;
+
+ /** write model response to command using another language printer */
+ void toStreamUsing(OutputLanguage lang,
+                    std::ostream& out,
+                    const Model& m,
+                    const Command* c) const
+ {
+   getPrinter(lang)->toStream(out, m, c);
   }
 
-public:
+ public:
   /** Get the Printer for a given OutputLanguage */
-  static Printer* getPrinter(OutputLanguage lang) throw();
+  static Printer* getPrinter(OutputLanguage lang);
 
   /** Write a Node out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, TNode n,
-                        int toDepth, bool types, size_t dag) const throw() = 0;
+  virtual void toStream(std::ostream& out,
+                        TNode n,
+                        int toDepth,
+                        bool types,
+                        size_t dag) const = 0;
 
   /** Write a Command out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, const Command* c,
-                        int toDepth, bool types, size_t dag) const throw() = 0;
+  virtual void toStream(std::ostream& out,
+                        const Command* c,
+                        int toDepth,
+                        bool types,
+                        size_t dag) const = 0;
 
   /** Write a CommandStatus out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
+  virtual void toStream(std::ostream& out, const CommandStatus* s) const = 0;
 
   /** Write a Model out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, const Model& m) const throw();
+  virtual void toStream(std::ostream& out, const Model& m) const;
 
   /** Write an UnsatCore out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, const UnsatCore& core) const throw();
+  virtual void toStream(std::ostream& out, const UnsatCore& core) const;
 
   /**
    * Write the term that sygus datatype term n
@@ -88,7 +100,7 @@ public:
    * This method may make calls to sygus printing callback
    * methods stored in sygus datatype constructors.
    */
-  virtual void toStreamSygus(std::ostream& out, TNode n) const throw();
+  virtual void toStreamSygus(std::ostream& out, TNode n) const;
 
 };/* class Printer */
 
diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
index b67274ce2..ac3c2f970 100644
--- a/src/printer/smt1/smt1_printer.cpp
+++ b/src/printer/smt1/smt1_printer.cpp
@@ -31,26 +31,35 @@ namespace CVC4 {
 namespace printer {
 namespace smt1 {
 
-void Smt1Printer::toStream(std::ostream& out, TNode n,
-                           int toDepth, bool types, size_t dag) const throw() {
+void Smt1Printer::toStream(
+    std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
+{
   n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* Smt1Printer::toStream() */
 
-void Smt1Printer::toStream(std::ostream& out, const Command* c,
-                           int toDepth, bool types, size_t dag) const throw() {
+void Smt1Printer::toStream(std::ostream& out,
+                           const Command* c,
+                           int toDepth,
+                           bool types,
+                           size_t dag) const
+{
   c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* Smt1Printer::toStream() */
 
-void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const
+{
   s->toStream(out, language::output::LANG_SMTLIB_V2_5);
 }/* Smt1Printer::toStream() */
 
-
-void Smt1Printer::toStream(std::ostream& out, const Model& m) const throw() {
+void Smt1Printer::toStream(std::ostream& out, const Model& m) const
+{
   Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, m);
 }
 
-void Smt1Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
+void Smt1Printer::toStream(std::ostream& out,
+                           const Model& m,
+                           const Command* c) const
+{
   // shouldn't be called; only the non-Command* version above should be
   Unreachable();
 }
diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h
index 920bd6494..560393b81 100644
--- a/src/printer/smt1/smt1_printer.h
+++ b/src/printer/smt1/smt1_printer.h
@@ -28,14 +28,26 @@ namespace printer {
 namespace smt1 {
 
 class Smt1Printer : public CVC4::Printer {
-  void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
-public:
+ public:
   using CVC4::Printer::toStream;
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
-  void toStream(std::ostream& out, const CommandStatus* s) const throw();
-  void toStream(std::ostream& out, const SExpr& sexpr) const throw();
-  void toStream(std::ostream& out, const Model& m) const throw();
+  void toStream(std::ostream& out,
+                TNode n,
+                int toDepth,
+                bool types,
+                size_t dag) const override;
+  void toStream(std::ostream& out,
+                const Command* c,
+                int toDepth,
+                bool types,
+                size_t dag) const override;
+  void toStream(std::ostream& out, const CommandStatus* s) const override;
+  void toStream(std::ostream& out, const Model& m) const override;
+
+ private:
+  void toStream(std::ostream& out,
+                const Model& m,
+                const Command* c) const override;
+  void toStream(std::ostream& out, const SExpr& sexpr) const;
 };/* class Smt1Printer */
 
 }/* CVC4::printer::smt1 namespace */
@@ -43,4 +55,3 @@ public:
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PRINTER__SMT1_PRINTER_H */
-
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index c029c0824..19adba6da 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -40,17 +40,20 @@ namespace CVC4 {
 namespace printer {
 namespace smt2 {
 
-static OutputLanguage variantToLanguage(Variant v) throw();
+static OutputLanguage variantToLanguage(Variant v);
 
-static string smtKindString(Kind k) throw();
+static string smtKindString(Kind k);
 
-static void printBvParameterizedOp(std::ostream& out, TNode n) throw();
-static void printFpParameterizedOp(std::ostream& out, TNode n) throw();
+static void printBvParameterizedOp(std::ostream& out, TNode n);
+static void printFpParameterizedOp(std::ostream& out, TNode n);
 
-static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) throw();
+static void toStreamRational(std::ostream& out,
+                             const Rational& r,
+                             bool decimal);
 
-void Smt2Printer::toStream(std::ostream& out, TNode n,
-                           int toDepth, bool types, size_t dag) const throw() {
+void Smt2Printer::toStream(
+    std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
+{
   if(dag != 0) {
     DagificationVisitor dv(dag);
     NodeVisitor<DagificationVisitor> visitor;
@@ -108,8 +111,12 @@ static bool stringifyRegexp(Node n, stringstream& ss) {
 }
 
 // force_nt is the type that n must have
-void Smt2Printer::toStream(std::ostream& out, TNode n,
-                           int toDepth, bool types, TypeNode force_nt) const throw() {
+void Smt2Printer::toStream(std::ostream& out,
+                           TNode n,
+                           int toDepth,
+                           bool types,
+                           TypeNode force_nt) const
+{
   // null
   if(n.getKind() == kind::NULL_EXPR) {
     out << "null";
@@ -803,7 +810,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   }
 }/* Smt2Printer::toStream(TNode) */
 
-static string smtKindString(Kind k) throw() {
+static string smtKindString(Kind k)
+{
   switch(k) {
     // builtin theory
   case kind::APPLY: break;
@@ -991,7 +999,8 @@ static string smtKindString(Kind k) throw() {
   return kind::kindToString(k);
 }
 
-static void printBvParameterizedOp(std::ostream& out, TNode n) throw() {
+static void printBvParameterizedOp(std::ostream& out, TNode n)
+{
   out << "(_ ";
   switch(n.getKind()) {
   case kind::BITVECTOR_EXTRACT: {
@@ -1029,7 +1038,8 @@ static void printBvParameterizedOp(std::ostream& out, TNode n) throw() {
   out << ")";
 }
 
-static void printFpParameterizedOp(std::ostream& out, TNode n) throw() {
+static void printFpParameterizedOp(std::ostream& out, TNode n)
+{
   out << "(_ ";
   switch(n.getKind()) {
   case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
@@ -1088,14 +1098,17 @@ static void printFpParameterizedOp(std::ostream& out, TNode n) throw() {
   out << ")";
 }
 
-
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) throw();
+static bool tryToStream(std::ostream& out, const Command* c);
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c, Variant v) throw();
+static bool tryToStream(std::ostream& out, const Command* c, Variant v);
 
-void Smt2Printer::toStream(std::ostream& out, const Command* c,
-                           int toDepth, bool types, size_t dag) const throw() {
+void Smt2Printer::toStream(std::ostream& out,
+                           const Command* c,
+                           int toDepth,
+                           bool types,
+                           size_t dag) const
+{
   expr::ExprSetDepth::Scope sdScope(out, toDepth);
   expr::ExprPrintTypes::Scope ptScope(out, types);
   expr::ExprDag::Scope dagScope(out, dag);
@@ -1148,11 +1161,11 @@ static std::string quoteSymbol(TNode n) {
   return CVC4::quoteSymbol(ss.str());
 }
 
-
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw();
+static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v);
 
-void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const
+{
   if (tryToStream<CommandSuccess>(out, s, d_variant) ||
       tryToStream<CommandFailure>(out, s, d_variant) ||
       tryToStream<CommandRecoverableFailure>(out, s, d_variant) ||
@@ -1166,8 +1179,8 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
 
 }/* Smt2Printer::toStream(CommandStatus*) */
 
-
-void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() {
+void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const
+{
   out << "(" << std::endl;
   SmtEngine * smt = core.getSmtEngine();
   Assert( smt!=NULL );
@@ -1184,8 +1197,8 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const throw
   out << ")" << endl;
 }/* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
 
-
-void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
+void Smt2Printer::toStream(std::ostream& out, const Model& m) const
+{
   //print the model comments
   std::stringstream c;
   m.getComments( c );
@@ -1208,8 +1221,10 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
   }
 }
 
-
-void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
+void Smt2Printer::toStream(std::ostream& out,
+                           const Model& m,
+                           const Command* c) const
+{
   const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
@@ -1314,7 +1329,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
   }
 }
 
-void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const throw()
+void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
 {
   if (n.getKind() == kind::APPLY_CONSTRUCTOR)
   {
@@ -1364,19 +1379,23 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const throw()
   }
 }
 
-static void toStream(std::ostream& out, const AssertCommand* c) throw() {
+static void toStream(std::ostream& out, const AssertCommand* c)
+{
   out << "(assert " << c->getExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const PushCommand* c) throw() {
+static void toStream(std::ostream& out, const PushCommand* c)
+{
   out << "(push 1)";
 }
 
-static void toStream(std::ostream& out, const PopCommand* c) throw() {
+static void toStream(std::ostream& out, const PopCommand* c)
+{
   out << "(pop 1)";
 }
 
-static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
+static void toStream(std::ostream& out, const CheckSatCommand* c)
+{
   Expr e = c->getExpr();
   if(!e.isNull() && !(e.getKind() == kind::CONST_BOOLEAN && e.getConst<bool>())) {
     out << PushCommand() << endl
@@ -1388,7 +1407,8 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
   }
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c) throw() {
+static void toStream(std::ostream& out, const QueryCommand* c)
+{
   Expr e = c->getExpr();
   if(!e.isNull()) {
     out << PushCommand() << endl
@@ -1400,19 +1420,23 @@ static void toStream(std::ostream& out, const QueryCommand* c) throw() {
   }
 }
 
-static void toStream(std::ostream& out, const ResetCommand* c) throw() {
+static void toStream(std::ostream& out, const ResetCommand* c)
+{
   out << "(reset)";
 }
 
-static void toStream(std::ostream& out, const ResetAssertionsCommand* c) throw() {
+static void toStream(std::ostream& out, const ResetAssertionsCommand* c)
+{
   out << "(reset-assertions)";
 }
 
-static void toStream(std::ostream& out, const QuitCommand* c) throw() {
+static void toStream(std::ostream& out, const QuitCommand* c)
+{
   out << "(exit)";
 }
 
-static void toStream(std::ostream& out, const CommandSequence* c) throw() {
+static void toStream(std::ostream& out, const CommandSequence* c)
+{
   CommandSequence::const_iterator i = c->begin();
   if(i != c->end()) {
     for(;;) {
@@ -1426,7 +1450,8 @@ static void toStream(std::ostream& out, const CommandSequence* c) throw() {
   }
 }
 
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() {
+static void toStream(std::ostream& out, const DeclareFunctionCommand* c)
+{
   Type type = c->getType();
   out << "(declare-fun " << CVC4::quoteSymbol(c->getSymbol()) << " (";
   if(type.isFunction()) {
@@ -1443,7 +1468,8 @@ static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw()
   out << ") " << type << ")";
 }
 
-static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() {
+static void toStream(std::ostream& out, const DefineFunctionCommand* c)
+{
   Expr func = c->getFunction();
   const vector<Expr>* formals = &c->getFormals();
   out << "(define-fun " << func << " (";
@@ -1475,7 +1501,8 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw()
   out << ") " << type << " " << formula << ")";
 }
 
-static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) throw() {
+static void toStreamRational(std::ostream& out, const Rational& r, bool decimal)
+{
   bool neg = r.sgn() < 0;
 
   // TODO:
@@ -1529,12 +1556,13 @@ static void toStreamRational(std::ostream& out, const Rational& r, bool decimal)
   //     }
 }
 
-
-static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
+static void toStream(std::ostream& out, const DeclareTypeCommand* c)
+{
   out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")";
 }
 
-static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
+static void toStream(std::ostream& out, const DefineTypeCommand* c)
+{
   const vector<Type>& params = c->getParameters();
   out << "(define-sort " << c->getSymbol() << " (";
   if(params.size() > 0) {
@@ -1545,7 +1573,8 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
   out << ") " << c->getType() << ")";
 }
 
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() {
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c)
+{
   out << "DefineNamedFunction( ";
   toStream(out, static_cast<const DefineFunctionCommand*>(c));
   out << " )";
@@ -1553,38 +1582,48 @@ static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) thr
   out << "ERROR: don't know how to output define-named-function command" << endl;
 }
 
-static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
+static void toStream(std::ostream& out, const SimplifyCommand* c)
+{
   out << "(simplify " << c->getTerm() << ")";
 }
 
-static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
+static void toStream(std::ostream& out, const GetValueCommand* c)
+{
   out << "(get-value ( ";
   const vector<Expr>& terms = c->getTerms();
   copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
   out << "))";
 }
 
-static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
+static void toStream(std::ostream& out, const GetModelCommand* c)
+{
   out << "(get-model)";
 }
 
-static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
+static void toStream(std::ostream& out, const GetAssignmentCommand* c)
+{
   out << "(get-assignment)";
 }
 
-static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
+static void toStream(std::ostream& out, const GetAssertionsCommand* c)
+{
   out << "(get-assertions)";
 }
 
-static void toStream(std::ostream& out, const GetProofCommand* c) throw() {
+static void toStream(std::ostream& out, const GetProofCommand* c)
+{
   out << "(get-proof)";
 }
 
-static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) throw() {
+static void toStream(std::ostream& out, const GetUnsatCoreCommand* c)
+{
   out << "(get-unsat-core)";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, Variant v) throw() {
+static void toStream(std::ostream& out,
+                     const SetBenchmarkStatusCommand* c,
+                     Variant v)
+{
   if(v == z3str_variant || v == smt2_0_variant) {
     out << "(set-info :status " << c->getStatus() << ")";
   } else {
@@ -1592,7 +1631,10 @@ static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, Vari
   }
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Variant v) throw() {
+static void toStream(std::ostream& out,
+                     const SetBenchmarkLogicCommand* c,
+                     Variant v)
+{
   // Z3-str doesn't have string-specific logic strings(?), so comment it
   if(v == z3str_variant) {
     out << "; (set-logic " << c->getLogic() << ")";
@@ -1601,7 +1643,8 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Varia
   }
 }
 
-static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v) throw() {
+static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v)
+{
   if(v == z3str_variant || v == smt2_0_variant) {
     out << "(set-info :" << c->getFlag() << " ";
   } else {
@@ -1612,17 +1655,20 @@ static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v) thro
   out << ")";
 }
 
-static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
+static void toStream(std::ostream& out, const GetInfoCommand* c)
+{
   out << "(get-info :" << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
+static void toStream(std::ostream& out, const SetOptionCommand* c)
+{
   out << "(set-option :" << c->getFlag() << " ";
   SExpr::toStream(out, c->getSExpr(), language::output::LANG_SMTLIB_V2_5);
   out << ")";
 }
 
-static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
+static void toStream(std::ostream& out, const GetOptionCommand* c)
+{
   out << "(get-option :" << c->getFlag() << ")";
 }
 
@@ -1641,7 +1687,10 @@ static void toStream(std::ostream& out, const Datatype & d) {
   }
 }
 
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, Variant v) throw() {
+static void toStream(std::ostream& out,
+                     const DatatypeDeclarationCommand* c,
+                     Variant v)
+{
   const vector<DatatypeType>& datatypes = c->getDatatypes();
   out << "(declare-";
   Assert( !datatypes.empty() );
@@ -1683,7 +1732,8 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, Var
   out << ")";
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c, Variant v) throw() {
+static void toStream(std::ostream& out, const CommentCommand* c, Variant v)
+{
   string s = c->getComment();
   size_t pos = 0;
   while((pos = s.find_first_of('"', pos)) != string::npos) {
@@ -1693,10 +1743,10 @@ static void toStream(std::ostream& out, const CommentCommand* c, Variant v) thro
   out << "(set-info :notes \"" << s << "\")";
 }
 
-static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
-}
+static void toStream(std::ostream& out, const EmptyCommand* c) {}
 
-static void toStream(std::ostream& out, const EchoCommand* c, Variant v) throw() {
+static void toStream(std::ostream& out, const EchoCommand* c, Variant v)
+{
   std::string s = c->getOutput();
   // escape all double-quotes
   size_t pos = 0;
@@ -1708,7 +1758,8 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v) throw()
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) throw() {
+static bool tryToStream(std::ostream& out, const Command* c)
+{
   if(typeid(*c) == typeid(T)) {
     toStream(out, dynamic_cast<const T*>(c));
     return true;
@@ -1717,7 +1768,8 @@ static bool tryToStream(std::ostream& out, const Command* c) throw() {
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c, Variant v) throw() {
+static bool tryToStream(std::ostream& out, const Command* c, Variant v)
+{
   if(typeid(*c) == typeid(T)) {
     toStream(out, dynamic_cast<const T*>(c), v);
     return true;
@@ -1725,17 +1777,20 @@ static bool tryToStream(std::ostream& out, const Command* c, Variant v) throw()
   return false;
 }
 
-static void toStream(std::ostream& out, const CommandSuccess* s, Variant v) throw() {
+static void toStream(std::ostream& out, const CommandSuccess* s, Variant v)
+{
   if(Command::printsuccess::getPrintSuccess(out)) {
     out << "success" << endl;
   }
 }
 
-static void toStream(std::ostream& out, const CommandInterrupted* s, Variant v) throw() {
+static void toStream(std::ostream& out, const CommandInterrupted* s, Variant v)
+{
   out << "interrupted" << endl;
 }
 
-static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) throw() {
+static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v)
+{
 #ifdef CVC4_COMPETITION_MODE
   // if in competition mode, lie and say we're ok
   // (we have nothing to lose by saying success, and everything to lose
@@ -1766,7 +1821,8 @@ static void toStream(std::ostream& out, const CommandRecoverableFailure* s,
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw() {
+static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v)
+{
   if(typeid(*s) == typeid(T)) {
     toStream(out, dynamic_cast<const T*>(s), v);
     return true;
@@ -1774,7 +1830,8 @@ static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) th
   return false;
 }
 
-static OutputLanguage variantToLanguage(Variant variant) throw() {
+static OutputLanguage variantToLanguage(Variant variant)
+{
   switch(variant) {
   case smt2_0_variant:
     return language::output::LANG_SMTLIB_V2_0;
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 96f55d7a2..922b69a9e 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -36,29 +36,42 @@ enum Variant {
 };/* enum Variant */
 
 class Smt2Printer : public CVC4::Printer {
-  Variant d_variant;
-
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types, TypeNode nt) const throw();
-  void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
-public:
+ public:
   Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }
   using CVC4::Printer::toStream;
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
-  void toStream(std::ostream& out, const CommandStatus* s) const throw();
-  void toStream(std::ostream& out, const SExpr& sexpr) const throw();
-  void toStream(std::ostream& out, const Model& m) const throw();
+  void toStream(std::ostream& out,
+                TNode n,
+                int toDepth,
+                bool types,
+                size_t dag) const override;
+  void toStream(std::ostream& out,
+                const Command* c,
+                int toDepth,
+                bool types,
+                size_t dag) const override;
+  void toStream(std::ostream& out, const CommandStatus* s) const override;
+  void toStream(std::ostream& out, const Model& m) const override;
   /**
    * Writes the unsat core to the stream out.
    * We use the expression names that are stored in the SMT engine associated
    * with the core (UnsatCore::getSmtEngine) for printing named assertions.
    */
-  void toStream(std::ostream& out, const UnsatCore& core) const throw();
+  void toStream(std::ostream& out, const UnsatCore& core) const override;
   /**
    * Write the term that sygus datatype term node n
    * encodes to a stream with this Printer.
    */
-  virtual void toStreamSygus(std::ostream& out, TNode n) const throw() override;
+  void toStreamSygus(std::ostream& out, TNode n) const override;
+
+ private:
+  void toStream(
+      std::ostream& out, TNode n, int toDepth, bool types, TypeNode nt) const;
+  void toStream(std::ostream& out,
+                const Model& m,
+                const Command* c) const override;
+  void toStream(std::ostream& out, const SExpr& sexpr) const;
+
+  Variant d_variant;
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */
@@ -66,4 +79,3 @@ public:
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PRINTER__SMT2_PRINTER_H */
-
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 102419ec4..ceee07bf1 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -33,22 +33,28 @@ namespace CVC4 {
 namespace printer {
 namespace tptp {
 
-void TptpPrinter::toStream(std::ostream& out, TNode n,
-                           int toDepth, bool types, size_t dag) const throw() {
+void TptpPrinter::toStream(
+    std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
+{
   n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
-void TptpPrinter::toStream(std::ostream& out, const Command* c,
-                           int toDepth, bool types, size_t dag) const throw() {
+void TptpPrinter::toStream(std::ostream& out,
+                           const Command* c,
+                           int toDepth,
+                           bool types,
+                           size_t dag) const
+{
   c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
-void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const
+{
   s->toStream(out, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
-
-void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() {
+void TptpPrinter::toStream(std::ostream& out, const Model& m) const
+{
   out << "% SZS output start FiniteModel for " << m.getInputName() << endl;
   for(size_t i = 0; i < m.getNumCommands(); ++i) {
     this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m, m.getCommand(i));
@@ -56,11 +62,15 @@ void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() {
   out << "% SZS output end FiniteModel for " << m.getInputName() << endl;
 }
 
-void TptpPrinter::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
+void TptpPrinter::toStream(std::ostream& out,
+                           const Model& m,
+                           const Command* c) const
+{
   // shouldn't be called; only the non-Command* version above should be
   Unreachable();
 }
-void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const throw() {
+void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const
+{
   out << "% SZS output start UnsatCore " << std::endl;
   SmtEngine * smt = core.getSmtEngine();
   Assert( smt!=NULL );
diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h
index 731885068..7e4cc0f83 100644
--- a/src/printer/tptp/tptp_printer.h
+++ b/src/printer/tptp/tptp_printer.h
@@ -28,18 +28,30 @@ namespace printer {
 namespace tptp {
 
 class TptpPrinter : public CVC4::Printer {
-  void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
-public:
+ public:
   using CVC4::Printer::toStream;
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
-  void toStream(std::ostream& out, const CommandStatus* s) const throw();
-  void toStream(std::ostream& out, const Model& m) const throw();
+  void toStream(std::ostream& out,
+                TNode n,
+                int toDepth,
+                bool types,
+                size_t dag) const override;
+  void toStream(std::ostream& out,
+                const Command* c,
+                int toDepth,
+                bool types,
+                size_t dag) const override;
+  void toStream(std::ostream& out, const CommandStatus* s) const override;
+  void toStream(std::ostream& out, const Model& m) const override;
   /** print unsat core to stream
   * We use the expression names stored in the SMT engine associated with the unsat core
   * with UnsatCore::getSmtEngine.
   */
-  void toStream(std::ostream& out, const UnsatCore& core) const throw();
+  void toStream(std::ostream& out, const UnsatCore& core) const override;
+
+ private:
+  void toStream(std::ostream& out,
+                const Model& m,
+                const Command* c) const override;
 };/* class TptpPrinter */
 
 }/* CVC4::printer::tptp namespace */