From 67a3ba16218ca0a936a6f2430dce721a076885f3 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 4 May 2010 19:31:24 +0000 Subject: Adding general support for SMT2 set-info command --- src/parser/antlr_input.cpp | 41 ++++++------ src/parser/antlr_input.h | 10 +-- src/parser/antlr_input_imports.cpp | 4 ++ src/parser/cvc/cvc_input.cpp | 4 +- src/parser/cvc/cvc_input.h | 2 +- src/parser/input.cpp | 20 ++++-- src/parser/input.h | 15 ++++- src/parser/smt/smt_input.cpp | 4 +- src/parser/smt/smt_input.h | 2 +- src/parser/smt2/Smt2.g | 128 +++++++++++++++++++++---------------- src/parser/smt2/smt2_input.cpp | 4 +- src/parser/smt2/smt2_input.h | 18 +++--- 12 files changed, 147 insertions(+), 105 deletions(-) (limited to 'src/parser') diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 5a34354e8..11e3ed604 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -43,6 +43,7 @@ namespace parser { AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) : InputStream(name), d_input(input) { + AlwaysAssert( input != NULL ); } AntlrInputStream::~AntlrInputStream() { @@ -53,34 +54,36 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { return d_input; } -AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) { +AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) + throw (InputStreamException) { + pANTLR3_INPUT_STREAM input = NULL; if( useMmap ) { - return new AntlrInputStream( name, MemoryMappedInputBufferNew(name) ); + input = MemoryMappedInputBufferNew(name); } else { - return new AntlrInputStream( name, antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str()) ); + input = antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str()); } -/* - if( d_inputStream == NULL ) { - throw ParserException("Couldn't open file: " + filename); - } -*/ + if( input == NULL ) { + throw InputStreamException("Couldn't open file: " + name); + } + return new AntlrInputStream( name, input ); } -AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) /*throw (InputStreamException) */{ +AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) + throw (InputStreamException) { char* inputStr = strdup(input.c_str()); char* nameStr = strdup(name.c_str()); -/* - if( inputStr==NULL || nameStr==NULL ) { + AlwaysAssert( inputStr!=NULL && nameStr!=NULL ); + pANTLR3_INPUT_STREAM inputStream = + antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) inputStr, + input.size(), + (pANTLR3_UINT8) nameStr); + if( inputStream==NULL ) { throw InputStreamException("Couldn't initialize string input: '" + input + "'"); } -*/ - return new AntlrInputStream( name, - antlr3NewAsciiStringInPlaceStream( - (pANTLR3_UINT8)inputStr,input.size(), - (pANTLR3_UINT8)nameStr) ); + return new AntlrInputStream( name, inputStream ); } -AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream *inputStream) { +AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStream) { AntlrInput* input; switch(lang) { @@ -102,12 +105,12 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream *inputStre return input; } -AntlrInput::AntlrInput(AntlrInputStream *inputStream, unsigned int lookahead) : +AntlrInput::AntlrInput(AntlrInputStream& inputStream, unsigned int lookahead) : Input(inputStream), d_lookahead(lookahead), d_lexer(NULL), d_parser(NULL), - d_antlr3InputStream( inputStream->getAntlr3InputStream() ), + d_antlr3InputStream( inputStream.getAntlr3InputStream() ), d_tokenStream(NULL) { } diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index d6d01b3cd..18317e4d8 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -62,7 +62,8 @@ public: * @param useMmap true if the input should use memory-mapped I/O; otherwise, the * input will use the standard ANTLR3 I/O implementation. */ - static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false); + static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false) + throw (InputStreamException); /** Create an input from an istream. */ // AntlrInputStream newInputStream(std::istream& input, const std::string& name); @@ -72,7 +73,8 @@ public: * @param input the string to read * @param name the "filename" to use when reporting errors */ - static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name); + static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name) + throw (InputStreamException); }; class Parser; @@ -134,7 +136,7 @@ public: * @param inputStream the input stream * * */ - static AntlrInput* newInput(InputLanguage lang, AntlrInputStream *inputStream); + static AntlrInput* newInput(InputLanguage lang, AntlrInputStream& inputStream); /** Retrieve the text associated with a token. */ static std::string tokenText(pANTLR3_COMMON_TOKEN token); @@ -153,7 +155,7 @@ protected: * @param lookahead the lookahead needed to parse the input (i.e., k for * an LL(k) grammar) */ - AntlrInput(AntlrInputStream *inputStream, unsigned int lookahead); + AntlrInput(AntlrInputStream& inputStream, unsigned int lookahead); /** Retrieve the token stream for this parser. Must not be called before * setLexer(). */ diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index 7c879f5bc..d25d7b66b 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -114,6 +114,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { } else { if(ex->expecting == ANTLR3_TOKEN_EOF) { ss << "Missing end of file marker."; + } else if( ex->expecting == 0 ) { + ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; } else { ss << "Missing " << tokenNames[ex->expecting] << "."; } @@ -147,6 +149,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { } else { if(ex->expecting == ANTLR3_TOKEN_EOF) { ss << "Expected end of file."; + } else if( ex->expecting == 0 ) { + ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; } else { ss << "Expected " << tokenNames[ex->expecting] << "."; } diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 48936a4c9..4a8551a7a 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -26,9 +26,9 @@ namespace CVC4 { namespace parser { /* Use lookahead=2 */ -CvcInput::CvcInput(AntlrInputStream *inputStream) : +CvcInput::CvcInput(AntlrInputStream& inputStream) : AntlrInput(inputStream,2) { - pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); + pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); AlwaysAssert( input != NULL ); d_pCvcLexer = CvcLexerNew(input); diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index ad7110bed..82c31813b 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -45,7 +45,7 @@ public: * * @param inputStream the input to parse */ - CvcInput(AntlrInputStream *inputStream); + CvcInput(AntlrInputStream& inputStream); /** Create a string input. * diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 3c1747759..9ee167897 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -31,12 +31,16 @@ using namespace CVC4::kind; namespace CVC4 { namespace parser { +InputStreamException::InputStreamException(const std::string& msg) : + Exception(msg) { +} + const std::string InputStream::getName() const { return d_name; } -Input::Input(InputStream *inputStream) : - d_inputStream( inputStream ) { +Input::Input(InputStream& inputStream) : + d_inputStream( &inputStream ) { } Input::~Input() { @@ -48,15 +52,19 @@ InputStream *Input::getInputStream() { } Input* Input::newFileInput(InputLanguage lang, - const std::string& filename, bool useMmap) { + const std::string& filename, + bool useMmap) + throw (InputStreamException) { AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap); - return AntlrInput::newInput(lang,inputStream); + return AntlrInput::newInput(lang,*inputStream); } Input* Input::newStringInput(InputLanguage lang, - const std::string& str, const std::string& name) { + const std::string& str, + const std::string& name) + throw (InputStreamException) { AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name); - return AntlrInput::newInput(lang,inputStream); + return AntlrInput::newInput(lang,*inputStream); } }/* CVC4::parser namespace */ diff --git a/src/parser/input.h b/src/parser/input.h index 80849c034..b277f6428 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -36,6 +36,13 @@ class FunctionType; namespace parser { +class CVC4_PUBLIC InputStreamException : public Exception { + +public: + InputStreamException(const std::string& msg); + virtual ~InputStreamException() throw() { } +}; + /** Wrapper around an ANTLR3 input stream. */ class InputStream { @@ -89,7 +96,8 @@ public: * @param filename the input filename * @param useMmap true if the parser should use memory-mapped I/O (default: false) */ - static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false); + static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false) + throw (InputStreamException); /** Create an input for the given stream. * @@ -105,7 +113,8 @@ public: * @param input the input string * @param name the name of the stream, for use in error messages */ - static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name); + static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name) + throw (InputStreamException); protected: @@ -113,7 +122,7 @@ protected: * * @param inputStream the input stream */ - Input(InputStream* inputStream); + Input(InputStream& inputStream); /** Retrieve the input stream for this parser. */ InputStream *getInputStream(); diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp index 520e6a6d6..7c8bf19dd 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -27,9 +27,9 @@ namespace CVC4 { namespace parser { /* Use lookahead=2 */ -SmtInput::SmtInput(AntlrInputStream *inputStream) : +SmtInput::SmtInput(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { - pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); + pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); AlwaysAssert( input != NULL ); d_pSmtLexer = SmtLexerNew(input); diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index 429f4dad5..1d3f87668 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -47,7 +47,7 @@ public: * * @param inputStream the input stream to use */ - SmtInput(AntlrInputStream *inputStream); + SmtInput(AntlrInputStream& inputStream); /** * Create a string input. diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b062e6b33..76ce91fd0 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -100,8 +100,12 @@ setLogic(Parser *parser, const std::string& name) { } } +static void +setInfo(Parser *parser, const std::string& flag, const SExpr& sexpr) { + // TODO: ??? } +} /** * Parses an expression. @@ -130,16 +134,19 @@ command returns [CVC4::Command* cmd] Expr expr; Type t; std::vector sorts; + SExpr sexpr; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] { Debug("parser") << "set logic: '" << name << "' " << std::endl; setLogic(PARSER_STATE,name); - $cmd = new SetBenchmarkLogicCommand(name); } - | SET_INFO_TOK c=setInfo - { cmd = c; } + $cmd = new SetBenchmarkLogicCommand(name); } + | SET_INFO_TOK KEYWORD symbolicExpr[sexpr] + { name = AntlrInput::tokenText($KEYWORD); + setInfo(PARSER_STATE,name,sexpr); + cmd = new SetInfoCommand(name,sexpr); } | /* sort declaration */ - DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=NUMERAL_TOK + DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=NUMERAL { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl; if( AntlrInput::tokenToInteger(n) > 0 ) { Unimplemented("Parameterized user sorts."); @@ -162,36 +169,31 @@ command returns [CVC4::Command* cmd] | /* checksat */ CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(true)); } + | EXIT_TOK + { // TODO: Explicitly represent exit as command? + cmd = 0; } ; -setInfo returns [CVC4::Command* cmd] -@declarations { - BenchmarkStatus status; +symbolicExpr[CVC4::SExpr& sexpr] +@declarations { + std::vector children; } - : CATEGORY_TOK sym=SYMBOL { - // FIXME? - cmd = new EmptyCommand(":category"); - } - | DIFFICULTY_TOK RATIONAL_TOK { - // FIXME? - cmd = new EmptyCommand(":difficulty"); - } - | NOTES_TOK sym=SYMBOL { - // FIXME? - cmd = new EmptyCommand(":notes"); - } - | SMT_VERSION_TOK RATIONAL_TOK { - // FIXME? - cmd = new EmptyCommand(":smt-lib-version"); - } - | SOURCE_TOK sym=SYMBOL { - // FIXME? - cmd = new EmptyCommand(":source"); - } - | STATUS_TOK benchmarkStatus[status] - { cmd = new SetBenchmarkStatusCommand(status); } -; - + : NUMERAL + { sexpr = SExpr(AntlrInput::tokenText($NUMERAL)); } + | RATIONAL + { sexpr = SExpr(AntlrInput::tokenText($RATIONAL)); } + | STRING_LITERAL + { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); } + | SYMBOL + { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); } + | KEYWORD + { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } + | LPAREN_TOK + (symbolicExpr[sexpr] { children.push_back(sexpr); } )* + RPAREN_TOK + { sexpr = SExpr(children); } + ; + /** * Matches a term. * @return the expression representing the formula @@ -251,11 +253,11 @@ term[CVC4::Expr& expr] /* constants */ | TRUE_TOK { expr = MK_CONST(true); } | FALSE_TOK { expr = MK_CONST(false); } - | NUMERAL_TOK - { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); } - | RATIONAL_TOK + | NUMERAL + { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL) ); } + | RATIONAL { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string - expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } + expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL) ); } // NOTE: Theory constants go here ; @@ -377,26 +379,27 @@ symbol[std::string& id, // Base SMT-LIB tokens ASSERT_TOK : 'assert'; BOOL_TOK : 'Bool'; -CATEGORY_TOK : ':category'; +//CATEGORY_TOK : ':category'; CHECKSAT_TOK : 'check-sat'; -DIFFICULTY_TOK : ':difficulty'; +//DIFFICULTY_TOK : ':difficulty'; DECLARE_FUN_TOK : 'declare-fun'; DECLARE_SORT_TOK : 'declare-sort'; +EXIT_TOK : 'exit'; FALSE_TOK : 'false'; ITE_TOK : 'ite'; LET_TOK : 'let'; LPAREN_TOK : '('; -NOTES_TOK : ':notes'; +//NOTES_TOK : ':notes'; RPAREN_TOK : ')'; -SAT_TOK : 'sat'; +//SAT_TOK : 'sat'; SET_LOGIC_TOK : 'set-logic'; SET_INFO_TOK : 'set-info'; -SMT_VERSION_TOK : ':smt-lib-version'; -SOURCE_TOK : ':source'; -STATUS_TOK : ':status'; +//SMT_VERSION_TOK : ':smt-lib-version'; +//SOURCE_TOK : ':source'; +//STATUS_TOK : ':status'; TRUE_TOK : 'true'; -UNKNOWN_TOK : 'unknown'; -UNSAT_TOK : 'unsat'; +//UNKNOWN_TOK : 'unknown'; +//UNSAT_TOK : 'unsat'; // operators (NOTE: theory symbols go here) AMPERSAND_TOK : '&'; @@ -422,14 +425,29 @@ TILDE_TOK : '~'; XOR_TOK : 'xor'; /** - * Matches a symbol from the input. A symbol a non-empty sequence of - * letters, digits and the characters + - / * = % ? ! . $ ~ & ^ < > @ that - * does not start with a digit or a sequence of printable ASCII characters - * that starts and ends with | and does not otherwise contain |. + * Matches a symbol from the input. A symbol is a "simple" symbole or a + * sequence of printable ASCII characters that starts and ends with | and + * does not otherwise contain |. */ SYMBOL + : SIMPLE_SYMBOL + | '|' ~('|')+ '|' + ; + +/** + * Matches a keyword from the input. A keyword is a symbol symbol, prefixed + * with a colon. + */ +KEYWORD + : ':' SIMPLE_SYMBOL + ; + +/** Matches a "simple" symbol: a non-empty sequence of letters, digits and + * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a + * digit. + */ +fragment SIMPLE_SYMBOL : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)* - | '|' ~('|') '|' ; /** @@ -442,11 +460,11 @@ WHITESPACE /** * Matches a numeral from the input (non-empty sequence of digits). */ -NUMERAL_TOK +NUMERAL : DIGIT+ ; -RATIONAL_TOK +RATIONAL : DIGIT+ '.' DIGIT+ ; @@ -479,12 +497,12 @@ ALPHA * Matches the digits (0-9) */ fragment DIGIT : '0'..'9'; -// fragment NON_ZERO_DIGIT : '1'..'9'; -// fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*; +/** Matches the characters that may appear in a "symbol" (i.e., an identifier) + */ fragment SYMBOL_CHAR - : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~' | '&' - | '^' | '<' | '>' | '@' + : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~' + | '&' | '^' | '<' | '>' | '@' ; /** diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index f962578e9..bcefe166b 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -27,9 +27,9 @@ namespace CVC4 { namespace parser { /* Use lookahead=2 */ -Smt2Input::Smt2Input(AntlrInputStream *inputStream) : +Smt2Input::Smt2Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { - pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); + pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); AlwaysAssert( input != NULL ); d_pSmt2Lexer = Smt2LexerNew(input); diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 2937d4ed8..ad32edcbc 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -40,6 +40,12 @@ class Smt2Input : public AntlrInput { /** The ANTLR3 CVC parser for the input. */ pSmt2Parser d_pSmt2Parser; + /** + * Initialize the class. Called from the constructors once the input + * stream is initialized. + */ + void init(); + public: /** @@ -47,7 +53,7 @@ public: * * @param inputStream the input stream to use */ - Smt2Input(AntlrInputStream *inputStream); + Smt2Input(AntlrInputStream& inputStream); /** * Create a string input. @@ -59,7 +65,7 @@ public: // Smt2Input(ExprManager* exprManager, const std::string& input, const std::string& name); /** Destructor. Frees the lexer and the parser. */ - ~Smt2Input(); + virtual ~Smt2Input(); protected: @@ -79,14 +85,6 @@ protected: */ Expr parseExpr() throw(ParserException); -private: - - /** - * Initialize the class. Called from the constructors once the input - * stream is initialized. - */ - void init(); - };/* class Smt2Input */ }/* CVC4::parser namespace */ -- cgit v1.2.3