From: Morgan Deters Date: Tue, 6 Jul 2010 15:52:10 +0000 (+0000) Subject: merge from CC work: pieces of the parser need to be declared to throw AssertionExcept... X-Git-Tag: cvc5-1.0.0~8941 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d6b40829e8d92a7a298d0c0023d944131a8285cf;p=cvc5.git merge from CC work: pieces of the parser need to be declared to throw AssertionException, and language enum should have stream insertion op --- 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 ParserException 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 Expr * 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 ParserException 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 + 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 */