14 files changed, 87 insertions, 111 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 915174982..a4bab5a8d 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -141,7 +141,7 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
 AntlrInputStream*
 AntlrInputStream::newFileInputStream(const std::string& name,
                                      bool useMmap)
-  throw (InputStreamException) {
+{
 #ifdef _WIN32
   if(useMmap) {
     useMmap = false;
@@ -164,8 +164,7 @@ AntlrInputStream*
 AntlrInputStream::newStreamInputStream(std::istream& input,
                                        const std::string& name,
                                        bool lineBuffered)
-  throw (InputStreamException) {
-
+{
   pANTLR3_INPUT_STREAM inputStream = NULL;
   pANTLR3_UINT8 inputStringCopy = NULL;
   LineBuffer* line_buffer = NULL;
@@ -223,8 +222,7 @@ AntlrInputStream::newStreamInputStream(std::istream& input,
 AntlrInputStream*
 AntlrInputStream::newStringInputStream(const std::string& input,
                                        const std::string& name)
-  throw (InputStreamException) {
-
+{
   size_t input_size = input.size();
   assert(input_size <= std::numeric_limits<uint32_t>::max());
 
@@ -510,8 +508,7 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons
 }
 
 void AntlrInput::parseError(const std::string& message, bool eofException)
-  throw (ParserException) {
-
+{
   string updatedMessage = parseErrorHelper((const char*)d_antlr3InputStream->getLineBuf(d_antlr3InputStream),
                                            d_lexer->getCharPositionInLine(d_lexer),
                                            message);
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index afede6bbf..d2bb8667d 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -88,14 +88,12 @@ public:
    * input will use the standard ANTLR3 I/O implementation.
    */
   static AntlrInputStream* newFileInputStream(const std::string& name,
-                                              bool useMmap = false)
-    throw (InputStreamException);
+                                              bool useMmap = false);
 
   /** Create an input from an istream. */
   static AntlrInputStream* newStreamInputStream(std::istream& input,
                                                 const std::string& name,
-                                                bool lineBuffered = false)
-    throw (InputStreamException);
+                                                bool lineBuffered = false);
 
   /** Create a string input.
    * NOTE: the new AntlrInputStream will take ownership of input over
@@ -105,8 +103,7 @@ public:
    * @param name the "filename" to use when reporting errors
    */
   static AntlrInputStream* newStringInputStream(const std::string& input,
-                                                const std::string& name)
-    throw (InputStreamException);
+                                                const std::string& name);
 };/* class AntlrInputStream */
 
 class Parser;
@@ -223,13 +220,12 @@ protected:
   /**
    * Issue a non-fatal warning to the user with file, line, and column info.
    */
-  void warning(const std::string& msg);
+  void warning(const std::string& msg) override;
 
   /**
    * Throws a <code>ParserException</code> with the given message.
    */
-  void parseError(const std::string& msg, bool eofException = false)
-    throw (ParserException);
+  void parseError(const std::string& msg, bool eofException = false) override;
 
   /** Set the ANTLR3 lexer for this input. */
   void setAntlr3Lexer(pANTLR3_LEXER pLexer);
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index bc16d646e..c35d8d963 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -40,8 +40,7 @@ class CvcInput : public AntlrInput {
   /** The ANTLR3 CVC parser for the input. */
   pCvcParser d_pCvcParser;
 
-public:
-
+ public:
   /** Create an input.
    *
    * @param inputStream the input to parse
@@ -52,18 +51,18 @@ public:
   virtual ~CvcInput();
 
   /** Get the language that this Input is reading. */
-  InputLanguage getLanguage() const throw() {
+  InputLanguage getLanguage() const override
+  {
     return language::input::LANG_CVC4;
   }
 
-protected:
-
+ protected:
   /** Parse a command from the input. Returns <code>NULL</code> if there is
    * no command there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand();
+  Command* parseCommand() override;
 
   /** Parse an expression from the input. Returns a null <code>Expr</code>
    * if there is no expression there to parse.
@@ -72,8 +71,7 @@ protected:
    */
   Expr parseExpr();
 
-private:
-
+ private:
   /** Initialize the class. Called from the constructors once the input stream
    * is initialized. */
   void init();
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index c8c3c5e6d..b5f86d569 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -57,7 +57,7 @@ InputStream *Input::getInputStream() {
 Input* Input::newFileInput(InputLanguage lang,
                            const std::string& filename,
                            bool useMmap)
-  throw (InputStreamException) {
+{
   AntlrInputStream *inputStream = 
     AntlrInputStream::newFileInputStream(filename, useMmap);
   return AntlrInput::newInput(lang, *inputStream);
@@ -67,7 +67,7 @@ Input* Input::newStreamInput(InputLanguage lang,
                              std::istream& input,
                              const std::string& name,
                              bool lineBuffered)
-  throw (InputStreamException) {
+{
   AntlrInputStream *inputStream =
     AntlrInputStream::newStreamInputStream(input, name, lineBuffered);
   return AntlrInput::newInput(lang, *inputStream);
@@ -76,7 +76,7 @@ Input* Input::newStreamInput(InputLanguage lang,
 Input* Input::newStringInput(InputLanguage lang,
                              const std::string& str,
                              const std::string& name)
-  throw (InputStreamException) {
+{
   AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str, name);
   return AntlrInput::newInput(lang, *inputStream);
 }
diff --git a/src/parser/input.h b/src/parser/input.h
index b41d8a898..76e4ac17e 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -38,10 +38,8 @@ class FunctionType;
 namespace parser {
 
 class CVC4_PUBLIC InputStreamException : public Exception {
-
-public:
+ public:
   InputStreamException(const std::string& msg);
-  virtual ~InputStreamException() throw() { }
 };
 
 /** Wrapper around an input stream. */
@@ -54,16 +52,14 @@ class CVC4_PUBLIC InputStream {
     * delete on exit. */
   bool d_fileIsTemporary;
 
-protected:
-
+ protected:
   /** Initialize the input stream with a name. */
   InputStream(std::string name, bool isTemporary=false) :
     d_name(name),
     d_fileIsTemporary(isTemporary) {
   }
 
-public:
-
+ public:
   /** Destructor. */
   virtual ~InputStream() {
     if( d_fileIsTemporary ) {
@@ -97,8 +93,7 @@ class CVC4_PUBLIC Input {
   Input(const Input& input) CVC4_UNDEFINED;
   Input& operator=(const Input& input) CVC4_UNDEFINED;
 
-public:
-
+ public:
   /** Create an input for the given file.
     *
     * @param lang the input language
@@ -107,8 +102,7 @@ public:
     */
   static Input* newFileInput(InputLanguage lang,
                              const std::string& filename,
-                             bool useMmap = false)
-    throw (InputStreamException);
+                             bool useMmap = false);
 
   /** Create an input for the given stream.
    *
@@ -122,8 +116,7 @@ public:
   static Input* newStreamInput(InputLanguage lang,
                                std::istream& input,
                                const std::string& name,
-                               bool lineBuffered = false)
-    throw (InputStreamException);
+                               bool lineBuffered = false);
 
   /** Create an input for the given string
    *
@@ -133,23 +126,17 @@ public:
    */
   static Input* newStringInput(InputLanguage lang,
                                const std::string& input,
-                               const std::string& name)
-    throw (InputStreamException);
-
+                               const std::string& name);
 
   /** Destructor. Frees the input stream and closes the input. */
   virtual ~Input();
 
   /** Get the language that this Input is reading. */
-  virtual InputLanguage getLanguage() const throw() = 0;
+  virtual InputLanguage getLanguage() const = 0;
 
   /** Retrieve the name of the input stream */
-  const std::string getInputStreamName(){
-    return getInputStream()->getName();
-  }
-
-protected:
-
+  const std::string getInputStreamName() { return getInputStream()->getName(); }
+ protected:
   /** Create an input.
    *
    * @param inputStream the input stream
@@ -175,8 +162,8 @@ protected:
   /**
    * Throws a <code>ParserException</code> with the given message.
    */
-  virtual void parseError(const std::string& msg, bool eofException = false)
-    throw (ParserException) = 0;
+  virtual void parseError(const std::string& msg,
+                          bool eofException = false) = 0;
 
   /** Parse an expression from the input by invoking the
    * implementation-specific parsing method. Returns a null
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 0d8cc1fcb..395f41ba1 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -518,8 +518,10 @@ void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) {
 }
 
 void Parser::checkDeclaration(const std::string& varName,
-                              DeclarationCheck check, SymbolType type,
-                              std::string notes) throw(ParserException) {
+                              DeclarationCheck check,
+                              SymbolType type,
+                              std::string notes)
+{
   if (!d_checksEnabled) {
     return;
   }
@@ -549,7 +551,8 @@ void Parser::checkDeclaration(const std::string& varName,
   }
 }
 
-void Parser::checkFunctionLike(Expr fun) throw(ParserException) {
+void Parser::checkFunctionLike(Expr fun)
+{
   if (d_checksEnabled && !isFunctionLike(fun)) {
     stringstream ss;
     ss << "Expecting function-like symbol, found '";
@@ -559,7 +562,8 @@ void Parser::checkFunctionLike(Expr fun) throw(ParserException) {
   }
 }
 
-void Parser::checkArity(Kind kind, unsigned numArgs) throw(ParserException) {
+void Parser::checkArity(Kind kind, unsigned numArgs)
+{
   if (!d_checksEnabled) {
     return;
   }
@@ -581,7 +585,8 @@ void Parser::checkArity(Kind kind, unsigned numArgs) throw(ParserException) {
   }
 }
 
-void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
+void Parser::checkOperator(Kind kind, unsigned numArgs)
+{
   if (d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end()) {
     parseError("Operator is not defined in the current logic: " +
                kindToString(kind));
@@ -592,9 +597,8 @@ void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
 void Parser::addOperator(Kind kind) { d_logicOperators.insert(kind); }
 
 void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); }
-
-Command* Parser::nextCommand() throw(ParserException,
-                                     UnsafeInterruptException) {
+Command* Parser::nextCommand()
+{
   Debug("parser") << "nextCommand()" << std::endl;
   Command* cmd = NULL;
   if (!d_commandQueue.empty()) {
@@ -627,7 +631,8 @@ Command* Parser::nextCommand() throw(ParserException,
   return cmd;
 }
 
-Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) {
+Expr Parser::nextExpression()
+{
   Debug("parser") << "nextExpression()" << std::endl;
   const Options& options = d_exprManager->getOptions();
   d_resourceManager->spendResource(options.getParseStep());
diff --git a/src/parser/parser.h b/src/parser/parser.h
index f2044c7ef..7f64b9580 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -400,9 +400,10 @@ public:
    * @param notes notes to add to a parse error (if one is generated)
    * @throws ParserException if checks are enabled and the check fails
    */
-  void checkDeclaration(const std::string& name, DeclarationCheck check,
+  void checkDeclaration(const std::string& name,
+                        DeclarationCheck check,
                         SymbolType type = SYM_VARIABLE,
-                        std::string notes = "") throw(ParserException);
+                        std::string notes = "");
 
   /**
    * Reserve a symbol at the assertion level.
@@ -418,7 +419,7 @@ public:
    * @throws ParserException if checks are enabled and fun is not
    * a function
    */
-  void checkFunctionLike(Expr fun) throw(ParserException);
+  void checkFunctionLike(Expr fun);
 
   /**
    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
@@ -428,7 +429,7 @@ public:
    * <code>kind</code> cannot be applied to <code>numArgs</code>
    * arguments.
    */
-  void checkArity(Kind kind, unsigned numArgs) throw(ParserException);
+  void checkArity(Kind kind, unsigned numArgs);
 
   /**
    * Check that <code>kind</code> is a legal operator in the current
@@ -439,7 +440,7 @@ public:
    * @throws ParserException if the parser mode is strict and the
    * operator <code>kind</code> has not been enabled
    */
-  void checkOperator(Kind kind, unsigned numArgs) throw(ParserException);
+  void checkOperator(Kind kind, unsigned numArgs);
 
   /** Create a new CVC4 variable expression of the given type. 
    *
@@ -671,26 +672,21 @@ public:
   bool isPredicate(const std::string& name);
 
   /** Parse and return the next command. */
-  Command* nextCommand() throw(ParserException, UnsafeInterruptException);
+  Command* nextCommand();
 
   /** Parse and return the next expression. */
-  Expr nextExpression() throw(ParserException, UnsafeInterruptException);
+  Expr nextExpression();
 
   /** Issue a warning to the user. */
-  inline void warning(const std::string& msg) {
-    d_input->warning(msg);
-  }
-
+  void warning(const std::string& msg) { d_input->warning(msg); }
   /** Issue a warning to the user, but only once per attribute. */
   void attributeNotSupported(const std::string& attr);
 
   /** Raise a parse error with the given message. */
-  inline void parseError(const std::string& msg) throw(ParserException) {
-    d_input->parseError(msg);
-  }
-
+  inline void parseError(const std::string& msg) { d_input->parseError(msg); }
   /** Unexpectedly encountered an EOF */
-  inline void unexpectedEOF(const std::string& msg) throw(ParserException) {
+  inline void unexpectedEOF(const std::string& msg)
+  {
     d_input->parseError(msg, true);
   }
 
@@ -708,7 +704,8 @@ public:
    * support parsing quantifiers (just not doing anything with them).
    * So this mechanism gives you a way to do it with --parse-only.
    */
-  inline void unimplementedFeature(const std::string& msg) throw(ParserException) {
+  inline void unimplementedFeature(const std::string& msg)
+  {
     if(!d_parseOnly) {
       parseError("Unimplemented feature: " + msg);
     }
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index ec8d4949d..ceda2ba47 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -65,7 +65,7 @@ void ParserBuilder::init(ExprManager* exprManager,
 }
 
 Parser* ParserBuilder::build()
-  throw (InputStreamException) {
+{
   Input* input = NULL;
   switch( d_inputType ) {
   case FILE_INPUT:
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 4b4eb4e4e..fe4a754d1 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -97,7 +97,7 @@ public:
                 const Options& options);
 
   /** Build the parser, using the current settings. */
-  Parser *build() throw (InputStreamException);
+  Parser* build();
 
   /** Should semantic checks be enabled in the parser? (Default: yes) */
   ParserBuilder& withChecks(bool flag = true);
diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h
index c5a3d312e..7577b7bff 100644
--- a/src/parser/smt1/smt1_input.h
+++ b/src/parser/smt1/smt1_input.h
@@ -54,19 +54,19 @@ public:
   virtual ~Smt1Input();
 
   /** Get the language that this Input is reading. */
-  InputLanguage getLanguage() const throw() {
+  InputLanguage getLanguage() const override
+  {
     return language::input::LANG_SMTLIB_V1;
   }
 
-protected:
-
+ protected:
   /**
    * Parse a command from the input. Returns <code>NULL</code> if
    * there is no command there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand();
+  Command* parseCommand() override;
 
   /**
    * Parse an expression from the input. Returns a null
@@ -76,8 +76,7 @@ protected:
    */
   Expr parseExpr();
 
-private:
-
+ private:
   /**
    * Initialize the class. Called from the constructors once the input
    * stream is initialized.
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 4832fc6b5..94bc03235 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -278,9 +278,11 @@ public:
    * Smt2 parser provides its own checkDeclaration, which does the
    * same as the base, but with some more helpful errors.
    */
-  void checkDeclaration(const std::string& name, DeclarationCheck check,
+  void checkDeclaration(const std::string& name,
+                        DeclarationCheck check,
                         SymbolType type = SYM_VARIABLE,
-                        std::string notes = "") throw(ParserException) {
+                        std::string notes = "")
+  {
     // if the symbol is something like "-1", we'll give the user a helpful
     // syntax hint.  (-1 is a valid identifier in SMT-LIB, NOT unary minus.)
     if( check != CHECK_DECLARED ||
@@ -304,7 +306,8 @@ public:
     this->Parser::checkDeclaration(name, check, type, ss.str());
   }
 
-  void checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
+  void checkOperator(Kind kind, unsigned numArgs)
+  {
     Parser::checkOperator(kind, numArgs);
     // strict SMT-LIB mode enables extra checks for some bitvector operators
     // that CVC4 permits as N-ary but the standard requires is binary
@@ -328,7 +331,8 @@ public:
   }
 
   // Throw a ParserException with msg appended with the current logic.
-  inline void parseErrorLogic(const std::string& msg) throw(ParserException) {
+  inline void parseErrorLogic(const std::string& msg)
+  {
     const std::string withLogic = msg + getLogic().getLogicString();
     parseError(withLogic);
   }
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 4d6168643..0acb5462d 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -53,8 +53,7 @@ class Smt2Input : public AntlrInput {
    */
   void init();
 
-public:
-
+ public:
   /**
    * Create an input.
    *
@@ -67,22 +66,18 @@ public:
   virtual ~Smt2Input();
 
   /** Get the language that this Input is reading. */
-  InputLanguage getLanguage() const throw() {
-    return d_lang;
-  }
-
+  InputLanguage getLanguage() const override { return d_lang; }
   /** Set the language that this Input is reading. */
   void setLanguage(InputLanguage);
 
-protected:
-
+ protected:
   /**
    * Parse a command from the input. Returns <code>NULL</code> if
    * there is no command there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand();
+  Command* parseCommand() override;
 
   /**
    * Parse an expression from the input. Returns a null
diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h
index a66730ad6..0dca60a82 100644
--- a/src/parser/smt2/sygus_input.h
+++ b/src/parser/smt2/sygus_input.h
@@ -50,8 +50,7 @@ class SygusInput : public AntlrInput {
    */
   void init();
 
-public:
-
+ public:
   /**
    * Create an input.
    *
@@ -63,19 +62,19 @@ public:
   virtual ~SygusInput();
 
   /** Get the language that this Input is reading. */
-  InputLanguage getLanguage() const throw() {
+  InputLanguage getLanguage() const override
+  {
     return language::input::LANG_SYGUS;
   }
 
-protected:
-
+ protected:
   /**
    * Parse a command from the input. Returns <code>NULL</code> if
    * there is no command there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand();
+  Command* parseCommand() override;
 
   /**
    * Parse an expression from the input. Returns a null
diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h
index a1f70641e..5dd56034d 100644
--- a/src/parser/tptp/tptp_input.h
+++ b/src/parser/tptp/tptp_input.h
@@ -50,8 +50,7 @@ class TptpInput : public AntlrInput {
    */
   void init();
 
-public:
-
+ public:
   /**
    * Create an input.
    *
@@ -63,19 +62,19 @@ public:
   virtual ~TptpInput();
 
   /** Get the language that this Input is reading. */
-  InputLanguage getLanguage() const throw() {
+  InputLanguage getLanguage() const override
+  {
     return language::input::LANG_TPTP;
   }
 
-protected:
-
+ protected:
   /**
    * Parse a command from the input. Returns <code>NULL</code> if
    * there is no command there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand();
+  Command* parseCommand() override;
 
   /**
    * Parse an expression from the input. Returns a null