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

2 files changed, 150 insertions, 81 deletions

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