merge from CC work: pieces of the parser need to be declared to throw AssertionException, and language enum should have stream insertion op

11 files changed, 63 insertions, 29 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 740d7fae5..b919c3bd5 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -63,7 +63,7 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
 AntlrInputStream* 
 AntlrInputStream::newFileInputStream(const std::string& name, 
                                      bool useMmap)
-  throw (InputStreamException) {
+  throw (InputStreamException, AssertionException) {
   pANTLR3_INPUT_STREAM input = NULL;
   if( useMmap ) {
     input = MemoryMappedInputBufferNew(name);
@@ -79,7 +79,7 @@ AntlrInputStream::newFileInputStream(const std::string& name,
 AntlrInputStream* 
 AntlrInputStream::newStreamInputStream(std::istream& input, 
                                        const std::string& name)
-  throw (InputStreamException) {
+  throw (InputStreamException, AssertionException) {
 
   // Since these are all NULL on entry, realloc will be called
   char *basep = NULL, *boundp = NULL, *cp = NULL;
@@ -126,7 +126,7 @@ AntlrInputStream::newStreamInputStream(std::istream& input,
 AntlrInputStream* 
 AntlrInputStream::newStringInputStream(const std::string& input, 
                                        const std::string& name)
-  throw (InputStreamException) {
+  throw (InputStreamException, AssertionException) {
   char* inputStr = strdup(input.c_str());
   char* nameStr = strdup(name.c_str());
   AlwaysAssert( inputStr!=NULL && nameStr!=NULL );
@@ -159,6 +159,7 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
   default:
     Unhandled(lang);
   }
+
   return input;
 }
 
@@ -225,7 +226,7 @@ void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
 }
 
 void AntlrInput::parseError(const std::string& message)
-    throw (ParserException) {
+  throw (ParserException, AssertionException) {
   Debug("parser") << "Throwing exception: "
       << getInputStream()->getName() << ":"
       << d_lexer->getLine(d_lexer) << "."
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 0d5fda89a..940835a7e 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -74,12 +74,12 @@ public:
    */
   static AntlrInputStream* newFileInputStream(const std::string& name, 
                                               bool useMmap = false)
-    throw (InputStreamException);
+    throw (InputStreamException, AssertionException);
 
   /** Create an input from an istream. */
   static AntlrInputStream* newStreamInputStream(std::istream& input, 
                                                 const std::string& name)
-    throw (InputStreamException);
+    throw (InputStreamException, AssertionException);
 
   /** Create a string input.
    *
@@ -88,7 +88,7 @@ public:
    */
   static AntlrInputStream* newStringInputStream(const std::string& input, 
                                                 const std::string& name)
-    throw (InputStreamException);
+    throw (InputStreamException, AssertionException);
 };
 
 class Parser;
@@ -192,7 +192,8 @@ protected:
   /**
    * Throws a <code>ParserException</code> with the given message.
    */
-  void parseError(const std::string& msg) throw (ParserException);
+  void parseError(const std::string& msg)
+    throw (ParserException, AssertionException);
 
   /** Set the ANTLR3 lexer for this input. */
   void setAntlr3Lexer(pANTLR3_LEXER pLexer);
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 2b99f9a87..6b38abaab 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -58,11 +58,13 @@ CvcInput::~CvcInput() {
   d_pCvcParser->free(d_pCvcParser);
 }
 
-Command* CvcInput::parseCommand() throw (ParserException) {
+Command* CvcInput::parseCommand()
+  throw (ParserException, AssertionException) {
   return d_pCvcParser->parseCommand(d_pCvcParser);
 }
 
-Expr CvcInput::parseExpr() throw (ParserException) {
+Expr CvcInput::parseExpr()
+  throw (ParserException, AssertionException) {
   return d_pCvcParser->parseExpr(d_pCvcParser);
 }
 
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 64c6beea7..6a37680e8 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -71,14 +71,14 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand() throw(ParserException);
+  Command* parseCommand() throw(ParserException, AssertionException);
 
   /** Parse an expression from the input. Returns a null <code>Expr</code>
    * if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() throw(ParserException);
+  Expr parseExpr() throw(ParserException, AssertionException);
 
 private:
 
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 2c4671b93..36e96516f 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) {
+  throw (InputStreamException, AssertionException) {
   AntlrInputStream *inputStream = 
     AntlrInputStream::newFileInputStream(filename,useMmap);
   return AntlrInput::newInput(lang,*inputStream);
@@ -66,7 +66,7 @@ Input* Input::newFileInput(InputLanguage lang,
 Input* Input::newStreamInput(InputLanguage lang, 
                              std::istream& input, 
                              const std::string& name) 
-  throw (InputStreamException) {
+  throw (InputStreamException, AssertionException) {
   AntlrInputStream *inputStream = 
     AntlrInputStream::newStreamInputStream(input,name);
   return AntlrInput::newInput(lang,*inputStream);
@@ -75,7 +75,7 @@ Input* Input::newStreamInput(InputLanguage lang,
 Input* Input::newStringInput(InputLanguage lang,
                              const std::string& str,
                              const std::string& name)
-  throw (InputStreamException) {
+  throw (InputStreamException, AssertionException) {
   AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name);
   return AntlrInput::newInput(lang,*inputStream);
 }
diff --git a/src/parser/input.h b/src/parser/input.h
index ceec1c8bd..62015ba51 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -108,7 +108,7 @@ class CVC4_PUBLIC Input {
   static Input* newFileInput(InputLanguage lang, 
                              const std::string& filename, 
                              bool useMmap=false)
-      throw (InputStreamException);
+    throw (InputStreamException, AssertionException);
 
   /** Create an input for the given stream.
    *
@@ -119,7 +119,7 @@ class CVC4_PUBLIC Input {
   static Input* newStreamInput(InputLanguage lang, 
                                std::istream& input, 
                                const std::string& name) 
-    throw (InputStreamException);
+    throw (InputStreamException, AssertionException);
 
   /** Create an input for the given string
    *
@@ -130,7 +130,7 @@ class CVC4_PUBLIC Input {
   static Input* newStringInput(InputLanguage lang, 
                                const std::string& input, 
                                const std::string& name)
-    throw (InputStreamException);
+    throw (InputStreamException, AssertionException);
 
 public:
 
@@ -154,12 +154,14 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  virtual Command* parseCommand() throw(ParserException) = 0;
+  virtual Command* parseCommand()
+    throw (ParserException, AssertionException) = 0;
 
   /**
    * Throws a <code>ParserException</code> with the given message.
    */
-  virtual void parseError(const std::string& msg) throw (ParserException) = 0;
+  virtual void parseError(const std::string& msg)
+    throw (ParserException, AssertionException) = 0;
 
   /** Parse an
    * expression from the input by invoking the implementation-specific
@@ -168,7 +170,8 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  virtual Expr parseExpr() throw(ParserException) = 0;
+  virtual Expr parseExpr()
+    throw (ParserException, AssertionException) = 0;
 
   /** Set the Parser object for this input. */
   virtual void setParser(Parser& parser) = 0;
diff --git a/src/parser/parser_options.h b/src/parser/parser_options.h
index 85994c52c..b3fd203e2 100644
--- a/src/parser/parser_options.h
+++ b/src/parser/parser_options.h
@@ -21,6 +21,8 @@
 #ifndef __CVC4__PARSER__PARSER_OPTIONS_H
 #define __CVC4__PARSER__PARSER_OPTIONS_H
 
+#include <iostream>
+
 namespace CVC4 {
 namespace parser {
 
@@ -36,6 +38,27 @@ enum InputLanguage {
   LANG_AUTO
 };/* enum InputLanguage */
 
+inline std::ostream& operator<<(std::ostream& out, InputLanguage lang) {
+  switch(lang) {
+  case LANG_SMTLIB:
+    out << "LANG_SMTLIB";
+    break;
+  case LANG_SMTLIB_V2:
+    out << "LANG_SMTLIB_V2";
+    break;
+  case LANG_CVC4:
+    out << "LANG_CVC4";
+    break;
+  case LANG_AUTO:
+    out << "LANG_AUTO";
+    break;
+  default:
+    out << "undefined_language";
+  }
+
+  return out;
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp
index c19eca080..42843bac2 100644
--- a/src/parser/smt/smt_input.cpp
+++ b/src/parser/smt/smt_input.cpp
@@ -59,11 +59,13 @@ SmtInput::~SmtInput() {
   d_pSmtParser->free(d_pSmtParser);
 }
 
-Command* SmtInput::parseCommand() throw (ParserException) {
+Command* SmtInput::parseCommand()
+  throw (ParserException, AssertionException) {
   return d_pSmtParser->parseCommand(d_pSmtParser);
 }
 
-Expr SmtInput::parseExpr() throw (ParserException) {
+Expr SmtInput::parseExpr()
+  throw (ParserException, AssertionException) {
   return d_pSmtParser->parseExpr(d_pSmtParser);
 }
 
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
index 42581ec1c..f3f461915 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt/smt_input.h
@@ -72,7 +72,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand() throw(ParserException);
+  Command* parseCommand() throw(ParserException, AssertionException);
 
   /**
    * Parse an expression from the input. Returns a null
@@ -80,7 +80,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() throw(ParserException);
+  Expr parseExpr() throw(ParserException, AssertionException);
 
 private:
 
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 5156ea2e5..e0bcadd61 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -60,11 +60,13 @@ Smt2Input::~Smt2Input() {
   d_pSmt2Parser->free(d_pSmt2Parser);
 }
 
-Command* Smt2Input::parseCommand() throw (ParserException) {
+Command* Smt2Input::parseCommand()
+  throw (ParserException, AssertionException) {
   return d_pSmt2Parser->parseCommand(d_pSmt2Parser);
 }
 
-Expr Smt2Input::parseExpr() throw (ParserException) {
+Expr Smt2Input::parseExpr()
+  throw (ParserException, AssertionException) {
   return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
 }
 
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index c9d0d5ec5..45986948a 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -81,7 +81,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand() throw(ParserException);
+  Command* parseCommand() throw(ParserException, AssertionException);
 
   /**
    * Parse an expression from the input. Returns a null
@@ -89,7 +89,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() throw(ParserException);
+  Expr parseExpr() throw(ParserException, AssertionException);
 
 };/* class Smt2Input */