From: Christopher L. Conway Date: Wed, 28 Apr 2010 18:34:11 +0000 (+0000) Subject: Refactoring Input/Parser code to support external manipulation of the parser state. X-Git-Tag: cvc5-1.0.0~9104 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a72c7a26fda2b9c268912e618fd7d71164e4800a;p=cvc5.git Refactoring Input/Parser code to support external manipulation of the parser state. --- diff --git a/src/main/main.cpp b/src/main/main.cpp index 819f7695e..bdf4f882b 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -23,6 +23,7 @@ #include "main.h" #include "usage.h" #include "parser/input.h" +#include "parser/parser.h" #include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "expr/command.h" @@ -152,17 +153,18 @@ int runCvc4(int argc, char* argv[]) { // if(inputFromStdin) { // parser = Parser::getNewParser(&exprMgr, options.lang, cin, ""); // } else { - input = Input::newFileInput(&exprMgr, options.lang, argv[firstArgIndex], - options.memoryMap); + input = Input::newFileInput(options.lang, argv[firstArgIndex], + options.memoryMap); // } + Parser parser(&exprMgr, input); if(!options.semanticChecks) { - input->disableChecks(); + parser.disableChecks(); } // Parse and execute commands until we are done Command* cmd; - while((cmd = input->parseNextCommand())) { + while((cmd = parser.nextCommand())) { if( !options.parseOnly ) { doCommand(smt, cmd); } diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 276266757..1464eeac0 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -34,20 +34,17 @@ libcvc4parser_noinst_la_LIBADD = \ libcvc4parser_la_SOURCES = libcvc4parser_noinst_la_SOURCES = \ - antlr_input.h \ - antlr_input.cpp \ - antlr_input_imports.cpp \ bounded_token_buffer.h \ bounded_token_buffer.cpp \ bounded_token_factory.h \ bounded_token_factory.cpp \ input.h \ input.cpp \ + input_imports.cpp \ memory_mapped_input_buffer.h \ memory_mapped_input_buffer.cpp \ + parser.h \ + parser.cpp \ parser_options.h \ - parser_exception.h \ - parser_state.h \ - parser_state.cpp \ - symbol_table.h + parser_exception.h diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp deleted file mode 100644 index 47420a015..000000000 --- a/src/parser/antlr_input.cpp +++ /dev/null @@ -1,163 +0,0 @@ -/********************* */ -/** antlr_input.cpp - ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** A super-class for ANTLR-generated input language parsers - **/ - -#include -#include - -#include "antlr_input.h" -#include "bounded_token_buffer.h" -#include "bounded_token_factory.h" -#include "memory_mapped_input_buffer.h" -#include "parser_exception.h" -#include "parser_state.h" - -#include "util/output.h" -#include "util/Assert.h" -#include "expr/command.h" -#include "expr/type.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::parser; -using namespace CVC4::kind; - -namespace CVC4 { -namespace parser { - -AntlrInput::AntlrInput(ExprManager* exprManager, const std::string& filename, unsigned int lookahead, bool useMmap) : - Input(exprManager, filename), - d_lookahead(lookahead), - d_lexer(NULL), - d_parser(NULL), - d_tokenStream(NULL) { - - if( useMmap ) { - d_input = MemoryMappedInputBufferNew(filename); - } else { - d_input = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str()); - } - if( d_input == NULL ) { - throw ParserException("Couldn't open file: " + filename); - } -} - -/* -AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead) - Parser(exprManager,name), - d_lookahead(lookahead) { - -} -*/ - -AntlrInput::AntlrInput(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) : - Input(exprManager,name), - d_lookahead(lookahead), - d_lexer(NULL), - d_parser(NULL), - d_tokenStream(NULL) { - char* inputStr = strdup(input.c_str()); - char* nameStr = strdup(name.c_str()); - if( inputStr==NULL || nameStr==NULL ) { - throw ParserException("Couldn't initialize string input: '" + input + "'"); - } - d_input = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr); - if( d_input == NULL ) { - throw ParserException("Couldn't create input stream for string: '" + input + "'"); - } -} - -AntlrInput::~AntlrInput() { - d_tokenStream->free(d_tokenStream); - d_input->close(d_input); -} - -pANTLR3_INPUT_STREAM AntlrInput::getInputStream() { - return d_input; -} - -pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() { - return d_tokenStream; -} - -void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { - pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super); - AlwaysAssert(lexer!=NULL); - ParserState *parserState = (ParserState*)(lexer->super); - AlwaysAssert(parserState!=NULL); - - // Call the error display routine - parserState->parseError("Error finding next token."); -} - -void AntlrInput::parseError(const std::string& message) - throw (ParserException) { - Debug("parser") << "Throwing exception: " - << getParserState()->getFilename() << ":" - << d_lexer->getLine(d_lexer) << "." - << d_lexer->getCharPositionInLine(d_lexer) << ": " - << message << endl; - throw ParserException(message, getParserState()->getFilename(), - d_lexer->getLine(d_lexer), - d_lexer->getCharPositionInLine(d_lexer)); -} - - -void AntlrInput::setLexer(pANTLR3_LEXER pLexer) { - d_lexer = pLexer; - - pANTLR3_TOKEN_FACTORY pTokenFactory = d_lexer->rec->state->tokFactory; - if( pTokenFactory != NULL ) { - pTokenFactory->close(pTokenFactory); - } - - /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */ - pTokenFactory = BoundedTokenFactoryNew(d_input, 2*d_lookahead); - if( pTokenFactory == NULL ) { - throw ParserException("Couldn't create token factory."); - } - d_lexer->rec->state->tokFactory = pTokenFactory; - - pBOUNDED_TOKEN_BUFFER buffer = BoundedTokenBufferSourceNew(d_lookahead, d_lexer->rec->state->tokSource); - if( buffer == NULL ) { - throw ParserException("Couldn't create token buffer."); - } - - d_tokenStream = buffer->commonTstream; - - // ANTLR isn't using super, AFAICT. - d_lexer->super = getParserState(); - // Override default lexer error reporting - d_lexer->rec->reportError = &lexerError; -} - -void AntlrInput::setParser(pANTLR3_PARSER pParser) { - d_parser = pParser; - // ANTLR isn't using super, AFAICT. - // We could also use @parser::context to add a field to the generated parser, but then - // it would have to be declared separately in every input's grammar and we'd have to - // pass it in as an address anyway. - d_parser->super = getParserState(); -// d_parser->rec->match = &match; - d_parser->rec->reportError = &reportError; - /* Don't try to recover from a parse error. */ - // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it. - d_parser->rec->recoverFromMismatchedToken = - (void* (*)(ANTLR3_BASE_RECOGNIZER_struct*, ANTLR3_UINT32, ANTLR3_BITSET_LIST_struct*)) - d_parser->rec->mismatch; -} - - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h deleted file mode 100644 index a36853d7b..000000000 --- a/src/parser/antlr_input.h +++ /dev/null @@ -1,138 +0,0 @@ -/********************* */ -/** antlr_input.h - ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Base for ANTLR parser classes. - **/ - -#include "cvc4parser_private.h" - -#ifndef __CVC4__PARSER__ANTLR_PARSER_H -#define __CVC4__PARSER__ANTLR_PARSER_H - -#include -#include -#include -#include - -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "parser/input.h" -#include "parser/symbol_table.h" -#include "util/Assert.h" - -namespace CVC4 { - -class Command; -class Type; -class FunctionType; - -namespace parser { - -/** - * Wrapper for an ANTLR parser that includes convenience methods to set up input and token streams. - */ -class AntlrInput : public Input { - /** The token lookahead used to lex and parse the input. This should usually be equal to - * K for an LL(k) grammar. */ - unsigned int d_lookahead; - - /** The ANTLR3 lexer associated with this input. This will be NULL initially. It - * must be set by a call to setLexer, preferably in the subclass constructor. */ - pANTLR3_LEXER d_lexer; - - /** The ANTLR3 parser associated with this input. This will be NULL initially. It - * must be set by a call to setParser, preferably in the subclass constructor. - * The super field of d_parser will be set to this and - * reportError will be set to AntlrInput::reportError. */ - pANTLR3_PARSER d_parser; - - /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit. - * This is set by setLexer. - * NOTE: We assume that we can free it on exit. No sharing! */ - pANTLR3_COMMON_TOKEN_STREAM d_tokenStream; - - /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit. - * NOTE: We assume that we can free it on exit. No sharing! */ - pANTLR3_INPUT_STREAM d_input; - - /** Turns an ANTLR3 exception into a message for the user and calls parseError. */ - static void reportError(pANTLR3_BASE_RECOGNIZER recognizer); - - /** Builds a message for a lexer error and calls parseError. */ - static void lexerError(pANTLR3_BASE_RECOGNIZER recognizer); - -public: - - /** Create a file input. - * - * @param exprManager the manager to use when building expressions from the input - * @param filename the path of the file to read - * @param lookahead the lookahead needed to parse the input (i.e., k for an LL(k) grammar) - * @param useMmap true if the input should use memory-mapped I/O; otherwise, the - * input will use the standard ANTLR3 I/O implementation. - */ - AntlrInput(ExprManager* exprManager, const std::string& filename, unsigned int lookahead, bool useMmap); - - /** Create an input from an istream. */ - // AntlrParser(ExprManager* em, std::istream& input, const std::string& name, unsigned int lookahead); - - /** Create a string input. - * - * @param exprManager the manager to use when building expressions from the input - * @param input the string to read - * @param name the "filename" to use when reporting errors - * @param lookahead the lookahead needed to parse the input (i.e., k for an LL(k) grammar) - */ - AntlrInput(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead); - - /** Destructor. Frees the token stream and closes the input. */ - ~AntlrInput(); - - /** Retrieve the text associated with a token. */ - inline static std::string tokenText(pANTLR3_COMMON_TOKEN token); - -protected: - - /** - * Throws a ParserException with the given message. - */ - void parseError(const std::string& msg) throw (ParserException); - - /** Retrieve the input stream for this parser. */ - pANTLR3_INPUT_STREAM getInputStream(); - /** Retrieve the token stream for this parser. Must not be called before - * setLexer(). */ - pANTLR3_COMMON_TOKEN_STREAM getTokenStream(); - - /** Set the ANTLR lexer for this parser. */ - void setLexer(pANTLR3_LEXER pLexer); - - /** Set the ANTLR parser implementation for this parser. */ - void setParser(pANTLR3_PARSER pParser); -}; - -std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) { - ANTLR3_MARKER start = token->getStartIndex(token); - ANTLR3_MARKER end = token->getStopIndex(token); - /* start and end are boundary pointers. The text is a string - * of (end-start+1) bytes beginning at start. */ - std::string txt( (const char *)start, end-start+1 ); - Debug("parser-extra") << "tokenText: start=" << start << std::endl - << "end=" << end << std::endl - << "txt='" << txt << "'" << std::endl; - return txt; -} - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__ANTLR_PARSER_H */ diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp deleted file mode 100644 index 3555ed06b..000000000 --- a/src/parser/antlr_input_imports.cpp +++ /dev/null @@ -1,243 +0,0 @@ -/* - * The functions in this file are based on implementations in libantlr3c, - * with only minor CVC4-specific changes. - */ - -// [The "BSD licence"] -// Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC -// http://www.temporal-wave.com -// http://www.linkedin.com/in/jimidle -// -// All rights reserved. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions -// are met: -// 1. Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// 2. Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// 3. The name of the author may not be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR -// IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES -// OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. -// IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, -// INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT -// NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF -// THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - -#include -#include - -#include "antlr_input.h" -#include "parser_state.h" -#include "util/Assert.h" - -using namespace std; - -namespace CVC4 { -namespace parser { - -/// Report a recognition problem. -/// -/// This method sets errorRecovery to indicate the parser is recovering -/// not parsing. Once in recovery mode, no errors are generated. -/// To get out of recovery mode, the parser must successfully match -/// a token (after a resync). So it will go: -/// -/// 1. error occurs -/// 2. enter recovery mode, report error -/// 3. consume until token found in resynch set -/// 4. try to resume parsing -/// 5. next match() will reset errorRecovery mode -/// -/// If you override, make sure to update errorCount if you care about that. -/// -/* *** CVC4 NOTE *** - * This function is has been modified in not-completely-trivial ways from its - * libantlr3c implementation to support more informative error messages and to - * invoke the error reporting mechanism of the AntlrInput class instead of the - * default error printer. - */ -void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { - pANTLR3_EXCEPTION ex = recognizer->state->exception; - pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames; - stringstream ss; - - // Signal we are in error recovery now - recognizer->state->errorRecovery = ANTLR3_TRUE; - - // Indicate this recognizer had an error while processing. - recognizer->state->errorCount++; - - // Call the builtin error formatter - // recognizer->displayRecognitionError(recognizer, recognizer->state->tokenNames); - - /* TODO: Make error messages more useful, maybe by including more expected tokens and information - * about the current token. */ - switch(ex->type) { - case ANTLR3_UNWANTED_TOKEN_EXCEPTION: - - // Indicates that the recognizer was fed a token which seems to be - // spurious input. We can detect this when the token that follows - // this unwanted token would normally be part of the syntactically - // correct stream. Then we can see that the token we are looking at - // is just something that should not be there and throw this exception. - // - if(tokenNames == NULL) { - ss << "Unexpected token." ; - } else { - if(ex->expecting == ANTLR3_TOKEN_EOF) { - ss << "Expected end of file."; - } else { - ss << "Expected " << tokenNames[ex->expecting] - << ", found '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; - } - } - break; - - case ANTLR3_MISSING_TOKEN_EXCEPTION: - - // Indicates that the recognizer detected that the token we just - // hit would be valid syntactically if preceded by a particular - // token. Perhaps a missing ';' at line end or a missing ',' in an - // expression list, and such like. - // - if(tokenNames == NULL) { - ss << "Missing token (" << ex->expecting << ")."; - } else { - if(ex->expecting == ANTLR3_TOKEN_EOF) { - ss << "Missing end of file marker."; - } else { - ss << "Missing " << tokenNames[ex->expecting] << "."; - } - } - break; - - case ANTLR3_RECOGNITION_EXCEPTION: - - // Indicates that the recognizer received a token - // in the input that was not predicted. This is the basic exception type - // from which all others are derived. So we assume it was a syntax error. - // You may get this if there are not more tokens and more are needed - // to complete a parse for instance. - // - ss <<"Syntax error."; - break; - - case ANTLR3_MISMATCHED_TOKEN_EXCEPTION: - - // We were expecting to see one thing and got another. This is the - // most common error if we could not detect a missing or unwanted token. - // Here you can spend your efforts to - // derive more useful error messages based on the expected - // token set and the last token and so on. The error following - // bitmaps do a good job of reducing the set that we were looking - // for down to something small. Knowing what you are parsing may be - // able to allow you to be even more specific about an error. - // - if(tokenNames == NULL) { - ss << "Syntax error."; - } else { - if(ex->expecting == ANTLR3_TOKEN_EOF) { - ss << "Expected end of file."; - } else { - ss << "Expected " << tokenNames[ex->expecting] << "."; - } - } - break; - - case ANTLR3_NO_VIABLE_ALT_EXCEPTION: - // We could not pick any alt decision from the input given - // so god knows what happened - however when you examine your grammar, - // you should. It means that at the point where the current token occurred - // that the DFA indicates nowhere to go from here. - // - ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; - break; - - case ANTLR3_MISMATCHED_SET_EXCEPTION: - - { - ANTLR3_UINT32 count; - ANTLR3_UINT32 bit; - ANTLR3_UINT32 size; - ANTLR3_UINT32 numbits; - pANTLR3_BITSET errBits; - - // This means we were able to deal with one of a set of - // possible tokens at this point, but we did not see any - // member of that set. - // - ss << "Unexpected input: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) - << "'. Expected one of: "; - - // What tokens could we have accepted at this point in the - // parse? - // - count = 0; - errBits = antlr3BitsetLoad(ex->expectingSet); - numbits = errBits->numBits(errBits); - size = errBits->size(errBits); - - if(size > 0) { - // However many tokens we could have dealt with here, it is usually - // not useful to print ALL of the set here. I arbitrarily chose 8 - // here, but you should do whatever makes sense for you of course. - // No token number 0, so look for bit 1 and on. - // - for(bit = 1; bit < numbits && count < 8 && count < size; bit++) { - // TODO: This doesn;t look right - should be asking if the bit is set!! - // - if(tokenNames[bit]) { - if( count++ > 0 ) { - ss << ", "; - } - ss << tokenNames[bit]; - } - } - } else { - Unreachable("Parse error with empty set of expected tokens."); - } - } - break; - - case ANTLR3_EARLY_EXIT_EXCEPTION: - - // We entered a loop requiring a number of token sequences - // but found a token that ended that sequence earlier than - // we should have done. - // - ss << "Sequence terminated early by token: '" - << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; - break; - - default: - - // We don't handle any other exceptions here, but you can - // if you wish. If we get an exception that hits this point - // then we are just going to report what we know about the - // token. - // - Unhandled("Unexpected exception in parser."); - break; - } - - // Now get ready to throw an exception - pANTLR3_PARSER parser = (pANTLR3_PARSER)(recognizer->super); - AlwaysAssert(parser!=NULL); - ParserState *parserState = (ParserState*)(parser->super); - AlwaysAssert(parserState!=NULL); - - // Call the error display routine - parserState->parseError(ss.str()); -} - -} // namespace parser -} // namespace CVC4 diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 3f4435966..94a8a6a32 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -48,7 +48,7 @@ options { @parser::includes { #include "expr/command.h" -#include "parser/parser_state.h" +#include "parser/parser.h" namespace CVC4 { class Expr; @@ -59,8 +59,8 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "parser/antlr_input.h" -#include "parser/parser_state.h" +#include "parser/input.h" +#include "parser/parser.h" #include "util/output.h" #include @@ -70,7 +70,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ #undef PARSER_STATE -#define PARSER_STATE ((ParserState*)PARSER->super) +#define PARSER_STATE ((Parser*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR @@ -104,7 +104,7 @@ parseCommand returns [CVC4::Command* cmd] command returns [CVC4::Command* cmd = 0] @init { Expr f; - Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "command: " << Input::tokenText(LT(1)) << std::endl; } : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); } | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f); } @@ -124,7 +124,7 @@ declaration[CVC4::Command*& cmd] @init { std::vector ids; Type t; - Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "declaration: " << Input::tokenText(LT(1)) << std::endl; } : // FIXME: These could be type or function declarations, if that matters. identifierList[ids, CHECK_UNDECLARED, SYM_VARIABLE] COLON declType[t,ids] SEMICOLON @@ -134,7 +134,7 @@ declaration[CVC4::Command*& cmd] /** Match the right-hand side of a declaration. Returns the type. */ declType[CVC4::Type& t, std::vector& idList] @init { - Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "declType: " << Input::tokenText(LT(1)) << std::endl; } : /* A sort declaration (e.g., "T : TYPE") */ TYPE_TOK @@ -152,7 +152,7 @@ type[CVC4::Type& t] @init { Type t2; std::vector typeList; - Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "type: " << Input::tokenText(LT(1)) << std::endl; } : /* Simple type */ baseType[t] @@ -191,7 +191,7 @@ identifier[std::string& id, CVC4::parser::DeclarationCheck check, CVC4::parser::SymbolType type] : IDENTIFIER - { id = AntlrInput::tokenText($IDENTIFIER); + { id = Input::tokenText($IDENTIFIER); PARSER_STATE->checkDeclaration(id, check, type); } ; @@ -202,7 +202,7 @@ identifier[std::string& id, baseType[CVC4::Type& t] @init { std::string id; - Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "base type: " << Input::tokenText(LT(1)) << std::endl; } : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); } | typeSymbol[t] @@ -214,7 +214,7 @@ baseType[CVC4::Type& t] typeSymbol[CVC4::Type& t] @init { std::string id; - Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "type symbol: " << Input::tokenText(LT(1)) << std::endl; } : identifier[id,CHECK_DECLARED,SYM_SORT] { t = PARSER_STATE->getSort(id); } @@ -226,7 +226,7 @@ typeSymbol[CVC4::Type& t] */ formula[CVC4::Expr& formula] @init { - Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "formula: " << Input::tokenText(LT(1)) << std::endl; } : iffFormula[formula] ; @@ -250,7 +250,7 @@ formulaList[std::vector& formulas] iffFormula[CVC4::Expr& f] @init { Expr e; - Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "<=> formula: " << Input::tokenText(LT(1)) << std::endl; } : impliesFormula[f] ( IFF_TOK @@ -265,7 +265,7 @@ iffFormula[CVC4::Expr& f] impliesFormula[CVC4::Expr& f] @init { Expr e; - Debug("parser-extra") << "=> Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "=> Formula: " << Input::tokenText(LT(1)) << std::endl; } : orFormula[f] ( IMPLIES_TOK impliesFormula[e] @@ -279,7 +279,7 @@ impliesFormula[CVC4::Expr& f] orFormula[CVC4::Expr& f] @init { std::vector exprs; - Debug("parser-extra") << "OR Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "OR Formula: " << Input::tokenText(LT(1)) << std::endl; } : xorFormula[f] ( OR_TOK { exprs.push_back(f); } @@ -297,7 +297,7 @@ orFormula[CVC4::Expr& f] xorFormula[CVC4::Expr& f] @init { Expr e; - Debug("parser-extra") << "XOR formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "XOR formula: " << Input::tokenText(LT(1)) << std::endl; } : andFormula[f] ( XOR_TOK andFormula[e] @@ -311,7 +311,7 @@ xorFormula[CVC4::Expr& f] andFormula[CVC4::Expr& f] @init { std::vector exprs; - Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "AND Formula: " << Input::tokenText(LT(1)) << std::endl; } : notFormula[f] ( AND_TOK { exprs.push_back(f); } @@ -329,7 +329,7 @@ andFormula[CVC4::Expr& f] */ notFormula[CVC4::Expr& f] @init { - Debug("parser-extra") << "NOT formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "NOT formula: " << Input::tokenText(LT(1)) << std::endl; } : /* negation */ NOT_TOK notFormula[f] @@ -341,7 +341,7 @@ notFormula[CVC4::Expr& f] predFormula[CVC4::Expr& f] @init { Expr e; - Debug("parser-extra") << "predicate formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "predicate formula: " << Input::tokenText(LT(1)) << std::endl; } : term[f] (EQUAL_TOK term[e] @@ -356,10 +356,10 @@ term[CVC4::Expr& f] @init { std::string name; std::vector args; - Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "term: " << Input::tokenText(LT(1)) << std::endl; } : /* function application */ - // { isFunction(AntlrInput::tokenText(LT(1))) }? + // { isFunction(Input::tokenText(LT(1))) }? functionSymbol[f] { args.push_back( f ); } LPAREN formulaList[args] RPAREN @@ -387,7 +387,7 @@ term[CVC4::Expr& f] iteTerm[CVC4::Expr& f] @init { std::vector args; - Debug("parser-extra") << "ite: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "ite: " << Input::tokenText(LT(1)) << std::endl; } : IF_TOK formula[f] { args.push_back(f); } THEN_TOK formula[f] { args.push_back(f); } @@ -402,7 +402,7 @@ iteTerm[CVC4::Expr& f] iteElseTerm[CVC4::Expr& f] @init { std::vector args; - Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "else: " << Input::tokenText(LT(1)) << std::endl; } : ELSE_TOK formula[f] | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); } @@ -418,7 +418,7 @@ iteElseTerm[CVC4::Expr& f] */ functionSymbol[CVC4::Expr& f] @init { - Debug("parser-extra") << "function symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "function symbol: " << Input::tokenText(LT(1)) << std::endl; std::string name; } : identifier[name,CHECK_DECLARED,SYM_VARIABLE] diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index f247a651d..4595c52db 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -16,6 +16,7 @@ #include #include "expr/expr_manager.h" +#include "parser/input.h" #include "parser/parser_exception.h" #include "parser/cvc/cvc_input.h" #include "parser/cvc/generated/CvcLexer.h" @@ -25,18 +26,9 @@ namespace CVC4 { namespace parser { /* Use lookahead=2 */ -CvcInput::CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap) : - AntlrInput(exprManager,filename,2,useMmap) { - init(); -} - -CvcInput::CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name) : - AntlrInput(exprManager,input,name,2) { - init(); -} - -void CvcInput::init() { - pANTLR3_INPUT_STREAM input = getInputStream(); +CvcInput::CvcInput(AntlrInputStream *inputStream) : + Input(inputStream,2) { + pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); AlwaysAssert( input != NULL ); d_pCvcLexer = CvcLexerNew(input); @@ -44,7 +36,7 @@ void CvcInput::init() { throw ParserException("Failed to create CVC lexer."); } - setLexer( d_pCvcLexer->pLexer ); + setAntlr3Lexer( d_pCvcLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); AlwaysAssert( tokenStream != NULL ); @@ -54,7 +46,7 @@ void CvcInput::init() { throw ParserException("Failed to create CVC parser."); } - setParser(d_pCvcParser->pParser); + setAntlr3Parser(d_pCvcParser->pParser); } @@ -63,11 +55,11 @@ CvcInput::~CvcInput() { d_pCvcParser->free(d_pCvcParser); } -Command* CvcInput::doParseCommand() throw (ParserException) { +Command* CvcInput::parseCommand() throw (ParserException) { return d_pCvcParser->parseCommand(d_pCvcParser); } -Expr CvcInput::doParseExpr() throw (ParserException) { +Expr CvcInput::parseExpr() throw (ParserException) { return d_pCvcParser->parseExpr(d_pCvcParser); } diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 4878d015e..0d264f606 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -18,7 +18,7 @@ #ifndef __CVC4__PARSER__CVC_INPUT_H #define __CVC4__PARSER__CVC_INPUT_H -#include "parser/antlr_input.h" +#include "parser/input.h" #include "parser/cvc/generated/CvcLexer.h" #include "parser/cvc/generated/CvcParser.h" @@ -32,7 +32,7 @@ class ExprManager; namespace parser { -class CvcInput : public AntlrInput { +class CvcInput : public Input { /** The ANTLR3 CVC lexer for the input. */ pCvcLexer d_pCvcLexer; @@ -41,14 +41,11 @@ class CvcInput : public AntlrInput { public: - /** Create a file input. + /** Create an input. * - * @param exprManager the manager to use when building expressions from the input - * @param filename the path of the file to read - * @param useMmap true if the input should use memory-mapped - * I/O; otherwise, the input will use the standard ANTLR3 I/O implementation. + * @param inputStream the input to parse */ - CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap); + CvcInput(AntlrInputStream *inputStream); /** Create a string input. * @@ -56,8 +53,10 @@ public: * @param input the string to read * @param name the "filename" to use when reporting errors */ +/* CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name); +*/ /* Destructor. Frees the lexer and the parser. */ ~CvcInput(); @@ -69,14 +68,14 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* doParseCommand() throw(ParserException); + Command* parseCommand() throw(ParserException); /** 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 doParseExpr() throw(ParserException); + Expr parseExpr() throw(ParserException); private: diff --git a/src/parser/input.cpp b/src/parser/input.cpp index fd1a4cbd6..5df017f16 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -1,7 +1,7 @@ /********************* */ /** input.cpp - ** Original author: dejan - ** Major contributors: mdeters, cconway + ** Original author: cconway + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) @@ -10,113 +10,176 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Parser implementation. + ** A super-class for ANTLR-generated input language parsers **/ -#include +#include +#include #include "input.h" +#include "bounded_token_buffer.h" +#include "bounded_token_factory.h" +#include "memory_mapped_input_buffer.h" #include "parser_exception.h" -#include "parser_options.h" -#include "parser_state.h" +#include "parser.h" + #include "expr/command.h" -#include "expr/expr.h" +#include "expr/type.h" #include "parser/cvc/cvc_input.h" #include "parser/smt/smt_input.h" #include "util/output.h" #include "util/Assert.h" using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::kind; namespace CVC4 { namespace parser { -bool Input::done() const { - return d_parserState->done(); +AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) : + d_name(name), + d_input(input) { } -void Input::disableChecks() { - d_parserState->disableChecks(); +AntlrInputStream::~AntlrInputStream() { + d_input->free(d_input); } -void Input::enableChecks() { - d_parserState->enableChecks(); +pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { + return d_input; } -Command* Input::parseNextCommand() throw(ParserException) { - Debug("parser") << "parseNextCommand()" << std::endl; - Command* cmd = NULL; - if(!done()) { - try { - cmd = doParseCommand(); - if(cmd == NULL) { - d_parserState->setDone(); - } - } catch(ParserException& e) { - d_parserState->setDone(); - throw; - } +const std::string AntlrInputStream::getName() const { + return d_name; +} + +AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) { + if( useMmap ) { + return new AntlrInputStream( name, MemoryMappedInputBufferNew(name) ); + } else { + return new AntlrInputStream( name, antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str()) ); } - Debug("parser") << "parseNextCommand() => " << cmd << std::endl; - return cmd; -} - -Expr Input::parseNextExpression() throw(ParserException) { - Debug("parser") << "parseNextExpression()" << std::endl; - Expr result; - if(!done()) { - try { - result = doParseExpr(); - if(result.isNull()) - d_parserState->setDone(); - } catch(ParserException& e) { - d_parserState->setDone(); - throw; +/* + if( d_inputStream == NULL ) { + throw ParserException("Couldn't open file: " + filename); } +*/ +} + +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 ) { + throw InputStreamException("Couldn't initialize string input: '" + input + "'"); } - Debug("parser") << "parseNextExpression() => " << result << std::endl; - return result; +*/ + return new AntlrInputStream( name, + antlr3NewAsciiStringInPlaceStream( + (pANTLR3_UINT8)inputStr,input.size(), + (pANTLR3_UINT8)nameStr) ); +} + + +Input::Input(AntlrInputStream *inputStream, unsigned int lookahead) : + d_lookahead(lookahead), + d_lexer(NULL), + d_parser(NULL), + d_tokenStream(NULL), + d_inputStream( inputStream ) { + +/* + if( useMmap ) { + d_inputStream = MemoryMappedInputBufferNew(filename); + } else { + d_inputStream = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str()); + } +*/ +/* + if( d_inputStream == NULL ) { + throw ParserException("Couldn't open file: " + filename); + } +*/ +} + +/* +AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead) + Parser(exprManager,name), + d_lookahead(lookahead) { + } +*/ + +/* +Input::Input(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) : + Input(exprManager,name), + d_lookahead(lookahead), + d_lexer(NULL), + d_parser(NULL), + d_tokenStream(NULL) { + + char* inputStr = strdup(input.c_str()); + char* nameStr = strdup(name.c_str()); + if( inputStr==NULL || nameStr==NULL ) { + throw ParserException("Couldn't initialize string input: '" + input + "'"); + } + d_inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr); + if( d_inputStream == NULL ) { + throw ParserException("Couldn't create input stream for string: '" + input + "'"); + } -Input::Input(ExprManager* exprManager, const std::string& filename) { - d_parserState = new ParserState(exprManager,filename,this); } +*/ Input::~Input() { - delete d_parserState; + d_tokenStream->free(d_tokenStream); + delete d_inputStream; } -Input* Input::newFileInput(ExprManager* em, InputLanguage lang, - const std::string& filename, bool useMmap) { +AntlrInputStream *Input::getInputStream() { + return d_inputStream; +} - Input* input = 0; +pANTLR3_COMMON_TOKEN_STREAM Input::getTokenStream() { + return d_tokenStream; +} - switch(lang) { - case LANG_CVC4: - input = new CvcInput(em,filename,useMmap); - break; - case LANG_SMTLIB: - input = new SmtInput(em,filename,useMmap); - break; +void Input::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { + pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super); + AlwaysAssert(lexer!=NULL); + Parser *parser = (Parser*)(lexer->super); + AlwaysAssert(parser!=NULL); + Input *input = parser->getInput(); + AlwaysAssert(input!=NULL); - default: - Unhandled(lang); - } + // Call the error display routine + input->parseError("Error finding next token."); +} - return input; +Input* Input::newFileInput(InputLanguage lang, + const std::string& filename, bool useMmap) { + AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap); + return newInput(lang,inputStream); } -Input* Input::newStringInput(ExprManager* em, InputLanguage lang, +Input* Input::newStringInput(InputLanguage lang, const std::string& str, const std::string& name) { - Input* input = 0; + AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name); + return newInput(lang,inputStream); +} + +Input* Input::newInput(InputLanguage lang, AntlrInputStream *inputStream) { + Input* input; switch(lang) { case LANG_CVC4: { - input = new CvcInput(em,str,name); + input = new CvcInput(inputStream); break; } case LANG_SMTLIB: - input = new SmtInput(em,str,name); + input = new SmtInput(inputStream); break; default: @@ -125,5 +188,67 @@ Input* Input::newStringInput(ExprManager* em, InputLanguage lang, return input; } + +void Input::parseError(const std::string& message) + throw (ParserException) { + Debug("parser") << "Throwing exception: " + << d_inputStream->getName() << ":" + << d_lexer->getLine(d_lexer) << "." + << d_lexer->getCharPositionInLine(d_lexer) << ": " + << message << endl; + throw ParserException(message, d_inputStream->getName(), + d_lexer->getLine(d_lexer), + d_lexer->getCharPositionInLine(d_lexer)); +} + + +void Input::setAntlr3Lexer(pANTLR3_LEXER pLexer) { + d_lexer = pLexer; + + pANTLR3_TOKEN_FACTORY pTokenFactory = d_lexer->rec->state->tokFactory; + if( pTokenFactory != NULL ) { + pTokenFactory->close(pTokenFactory); + } + + /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */ + pTokenFactory = BoundedTokenFactoryNew(d_inputStream->getAntlr3InputStream(), 2*d_lookahead); + if( pTokenFactory == NULL ) { + throw ParserException("Couldn't create token factory."); + } + d_lexer->rec->state->tokFactory = pTokenFactory; + + pBOUNDED_TOKEN_BUFFER buffer = BoundedTokenBufferSourceNew(d_lookahead, d_lexer->rec->state->tokSource); + if( buffer == NULL ) { + throw ParserException("Couldn't create token buffer."); + } + + d_tokenStream = buffer->commonTstream; + + // Override default lexer error reporting + d_lexer->rec->reportError = &lexerError; +} + +void Input::setParser(Parser *parser) { + // ANTLR isn't using super in the lexer or the parser, AFAICT. + // We could also use @lexer/parser::context to add a field to the generated + // objects, but then it would have to be declared separately in every + // language's grammar and we'd have to in the address of the field anyway. + d_lexer->super = parser; + d_parser->super = parser; + +} + +void Input::setAntlr3Parser(pANTLR3_PARSER pParser) { + d_parser = pParser; +// d_parser->rec->match = &match; + d_parser->rec->reportError = &reportError; + /* Don't try to recover from a parse error. */ + // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it. + d_parser->rec->recoverFromMismatchedToken = + (void* (*)(ANTLR3_BASE_RECOGNIZER_struct*, ANTLR3_UINT32, ANTLR3_BITSET_LIST_struct*)) + d_parser->rec->mismatch; +} + + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/input.h b/src/parser/input.h index a32416305..21c5c4869 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -2,7 +2,7 @@ /** input.h ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -10,157 +10,228 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Parser abstraction. + ** Base for ANTLR parser classes. **/ -#include "cvc4parser_public.h" +#include "cvc4parser_private.h" -#ifndef __CVC4__PARSER__INPUT_H -#define __CVC4__PARSER__INPUT_H +#ifndef __CVC4__PARSER__ANTLR_INPUT_H +#define __CVC4__PARSER__ANTLR_INPUT_H +#include +#include #include +#include #include "expr/expr.h" +#include "expr/expr_manager.h" #include "parser/parser_exception.h" #include "parser/parser_options.h" +#include "util/Assert.h" namespace CVC4 { -// Forward declarations -class ExprManager; class Command; class Type; +class FunctionType; namespace parser { -class ParserState; +/** Wrapper around an ANTLR3 input stream. */ +class AntlrInputStream { + std::string d_name; + pANTLR3_INPUT_STREAM d_input; + + AntlrInputStream(std::string name,pANTLR3_INPUT_STREAM input); + /* This is private and throws an exception, because you should never use it. */ + AntlrInputStream(const AntlrInputStream& inputStream) { + Unimplemented("copy constructor for AntlrInputStream"); + } + /* This is private and throws an exception, because you should never use it. */ + AntlrInputStream& operator=(const AntlrInputStream& inputStream) { + Unimplemented("operator= for AntlrInputStream"); + } + +public: + + virtual ~AntlrInputStream(); + + pANTLR3_INPUT_STREAM getAntlr3InputStream() const; + const std::string getName() const; + + /** Create a file input. + * + * @param filename the path of the file to read + * @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); + + /** Create an input from an istream. */ + // AntlrInputStream newInputStream(std::istream& input, const std::string& name); + + /** Create a string input. + * + * @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); +}; + +class Parser; /** - * An input to be parsed. This class serves two purposes: to the client, it provides - * the methods parseNextCommand and parseNextExpression to - * extract a stream of Command's and Expr's from the input; - * to the parser, it provides a repository for state data, like the variable symbol - * table, and a variety of convenience functions for updating and checking the state. - * - * An Input should be created using the static factory methods, - * e.g., newFileParser and newStringInput, and - * should be deleted when done. + * An input to be parsed. The static factory methods in this class (e.g., + * newFileInput, newStringInput) create a parser + * for the given input language and attach it to an input source of the + * appropriate type. */ class CVC4_PUBLIC Input { - friend class ParserState; + friend class Parser; // for parseError, parseCommand, parseExpr - /** Whether to de-allocate the input */ - // bool d_deleteInput; + /** The display name of the input (e.g., the filename). */ + std::string d_name; - ParserState *d_parserState; + /** The token lookahead used to lex and parse the input. This should usually be equal to + * K for an LL(k) grammar. */ + unsigned int d_lookahead; -public: + /** The ANTLR3 lexer associated with this input. This will be NULL initially. It + * must be set by a call to setLexer, preferably in the subclass constructor. */ + pANTLR3_LEXER d_lexer; - /** - * Create a new parser for the given file. - * @param exprManager the ExprManager to use - * @param filename the path of the file to parse - */ - Input(ExprManager* exprManager, const std::string& filename); + /** The ANTLR3 parser associated with this input. This will be NULL initially. It + * must be set by a call to setParser, preferably in the subclass constructor. + * The super field of d_parser will be set to this and + * reportError will be set to Input::reportError. */ + pANTLR3_PARSER d_parser; - /** - * Destructor. + /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit. + * This is set by setLexer. + * NOTE: We assume that we can free it on exit. No sharing! */ + pANTLR3_COMMON_TOKEN_STREAM d_tokenStream; + + /** The ANTLR3 input stream associated with this input. We only need this so we can free it on exit. + * NOTE: We assume that we can free it on exit. No sharing! */ + AntlrInputStream *d_inputStream; + + /** Turns an ANTLR3 exception into a message for the user and calls parseError. */ + static void reportError(pANTLR3_BASE_RECOGNIZER recognizer); + + /** Builds a message for a lexer error and calls parseError. */ + static void lexerError(pANTLR3_BASE_RECOGNIZER recognizer); + + /* Since we own d_tokenStream and it needs to be freed, we need to prevent + * copy construction and assignment. */ + Input(const Input& input) { Unimplemented("Copy constructor for Input."); } + Input& operator=(const Input& input) { Unimplemented("operator= for Input."); } + +public: + + /** Destructor. Frees the token stream and closes the input. */ virtual ~Input(); /** Create an input for the given file. * - * @param exprManager the ExprManager for creating expressions from the input * @param lang the input language * @param filename the input filename * @param useMmap true if the parser should use memory-mapped I/O (default: false) */ - static Input* newFileInput(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false); + static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false); + + /** Create an input for the given AntlrInputStream. NOTE: the new Input + * will take ownership of the input stream and delete it at destruction time. + * + * @param lang the input language + * @param inputStream the input stream + * + * */ + static Input* newInput(InputLanguage lang, AntlrInputStream *inputStream); /** Create an input for the given stream. * - * @param exprManager the ExprManager for creating expressions from the input * @param lang the input language * @param input the input stream * @param name the name of the stream, for use in error messages */ - //static Parser* getNewParser(ExprManager* exprManager, InputLanguage lang, std::istream& input, const std::string& name); + //static Parser* newStreamInput(InputLanguage lang, std::istream& input, const std::string& name); /** Create an input for the given string * - * @param exprManager the ExprManager for creating expressions from the input * @param lang the input language * @param input the input string * @param name the name of the stream, for use in error messages */ - static Input* newStringInput(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name); + static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name); - /** - * Check if we are done -- either the end of input has been reached, or some - * error has been encountered. - * @return true if parser is done - */ - bool done() const; + /** Retrieve the text associated with a token. */ + inline static std::string tokenText(pANTLR3_COMMON_TOKEN token); - /** Enable semantic checks during parsing. */ - void enableChecks(); - /** - * Disable semantic checks during parsing. Disabling checks may lead - * to crashes on bad inputs. - */ - void disableChecks(); - - /** - * Parse the next command of the input. If EOF is encountered a EmptyCommand - * is returned and done flag is set. +protected: + /** Create an input. This input takes ownership of the given input stream, + * and will delete it at destruction time. * - * @throws ParserException if an error is encountered during parsing. + * @param inputStream the input stream to use + * @param lookahead the lookahead needed to parse the input (i.e., k for + * an LL(k) grammar) */ - Command* parseNextCommand() throw(ParserException); + Input(AntlrInputStream *inputStream, unsigned int lookahead); - /** - * Parse the next expression of the stream. If EOF is encountered a null - * expression is returned and done flag is set. - * @return the parsed expression - * @throws ParserException if an error is encountered during parsing. - */ - Expr parseNextExpression() throw(ParserException); + /** Retrieve the input stream for this parser. */ + AntlrInputStream *getInputStream(); -protected: + /** Retrieve the token stream for this parser. Must not be called before + * setLexer(). */ + pANTLR3_COMMON_TOKEN_STREAM getTokenStream(); - /** Called by parseNextCommand to actually parse a command from + /** Parse a command from * the input by invoking the implementation-specific parsing method. Returns * NULL if there is no command there to parse. * * @throws ParserException if an error is encountered during parsing. */ - virtual Command* doParseCommand() throw(ParserException) = 0; + virtual Command* parseCommand() throw(ParserException) = 0; + + /** + * Throws a ParserException with the given message. + */ + void parseError(const std::string& msg) throw (ParserException); - /** Called by parseNextExpression to actually parse an + /** Parse an * expression from the input by invoking the implementation-specific * parsing method. Returns a null Expr if there is no * expression there to parse. * * @throws ParserException if an error is encountered during parsing. */ - virtual Expr doParseExpr() throw(ParserException) = 0; - - inline ParserState* getParserState() const { - return d_parserState; - } - -private: - - /** Throws a ParserException with the given error message. - * Implementations should fill in the ParserException with - * line number information, etc. */ - virtual void parseError(const std::string& msg) throw (ParserException) = 0; - -}; // end of class Input + virtual Expr parseExpr() throw(ParserException) = 0; + + /** Set the ANTLR3 lexer for this input. */ + void setAntlr3Lexer(pANTLR3_LEXER pLexer); + + /** Set the ANTLR3 parser implementation for this input. */ + void setAntlr3Parser(pANTLR3_PARSER pParser); + + /** Set the Parser object for this input. */ + void setParser(Parser *parser); +}; + +std::string Input::tokenText(pANTLR3_COMMON_TOKEN token) { + ANTLR3_MARKER start = token->getStartIndex(token); + ANTLR3_MARKER end = token->getStopIndex(token); + /* start and end are boundary pointers. The text is a string + * of (end-start+1) bytes beginning at start. */ + std::string txt( (const char *)start, end-start+1 ); + Debug("parser-extra") << "tokenText: start=" << start << std::endl + << "end=" << end << std::endl + << "txt='" << txt << "'" << std::endl; + return txt; +} }/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PARSER__INPUT_H */ +#endif /* __CVC4__PARSER__ANTLR_INPUT_H */ diff --git a/src/parser/input_imports.cpp b/src/parser/input_imports.cpp new file mode 100644 index 000000000..73d804f95 --- /dev/null +++ b/src/parser/input_imports.cpp @@ -0,0 +1,245 @@ +/* + * The functions in this file are based on implementations in libantlr3c, + * with only minor CVC4-specific changes. + */ + +// [The "BSD licence"] +// Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC +// http://www.temporal-wave.com +// http://www.linkedin.com/in/jimidle +// +// All rights reserved. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions +// are met: +// 1. Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// 2. Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// 3. The name of the author may not be used to endorse or promote products +// derived from this software without specific prior written permission. +// +// THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR +// IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES +// OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. +// IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, +// INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT +// NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF +// THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +#include +#include + +#include "input.h" +#include "parser.h" +#include "util/Assert.h" + +using namespace std; + +namespace CVC4 { +namespace parser { + +/// Report a recognition problem. +/// +/// This method sets errorRecovery to indicate the parser is recovering +/// not parsing. Once in recovery mode, no errors are generated. +/// To get out of recovery mode, the parser must successfully match +/// a token (after a resync). So it will go: +/// +/// 1. error occurs +/// 2. enter recovery mode, report error +/// 3. consume until token found in resynch set +/// 4. try to resume parsing +/// 5. next match() will reset errorRecovery mode +/// +/// If you override, make sure to update errorCount if you care about that. +/// +/* *** CVC4 NOTE *** + * This function is has been modified in not-completely-trivial ways from its + * libantlr3c implementation to support more informative error messages and to + * invoke the error reporting mechanism of the Input class instead of the + * default error printer. + */ +void Input::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { + pANTLR3_EXCEPTION ex = recognizer->state->exception; + pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames; + stringstream ss; + + // Signal we are in error recovery now + recognizer->state->errorRecovery = ANTLR3_TRUE; + + // Indicate this recognizer had an error while processing. + recognizer->state->errorCount++; + + // Call the builtin error formatter + // recognizer->displayRecognitionError(recognizer, recognizer->state->tokenNames); + + /* TODO: Make error messages more useful, maybe by including more expected tokens and information + * about the current token. */ + switch(ex->type) { + case ANTLR3_UNWANTED_TOKEN_EXCEPTION: + + // Indicates that the recognizer was fed a token which seems to be + // spurious input. We can detect this when the token that follows + // this unwanted token would normally be part of the syntactically + // correct stream. Then we can see that the token we are looking at + // is just something that should not be there and throw this exception. + // + if(tokenNames == NULL) { + ss << "Unexpected token." ; + } else { + if(ex->expecting == ANTLR3_TOKEN_EOF) { + ss << "Expected end of file."; + } else { + ss << "Expected " << tokenNames[ex->expecting] + << ", found '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; + } + } + break; + + case ANTLR3_MISSING_TOKEN_EXCEPTION: + + // Indicates that the recognizer detected that the token we just + // hit would be valid syntactically if preceded by a particular + // token. Perhaps a missing ';' at line end or a missing ',' in an + // expression list, and such like. + // + if(tokenNames == NULL) { + ss << "Missing token (" << ex->expecting << ")."; + } else { + if(ex->expecting == ANTLR3_TOKEN_EOF) { + ss << "Missing end of file marker."; + } else { + ss << "Missing " << tokenNames[ex->expecting] << "."; + } + } + break; + + case ANTLR3_RECOGNITION_EXCEPTION: + + // Indicates that the recognizer received a token + // in the input that was not predicted. This is the basic exception type + // from which all others are derived. So we assume it was a syntax error. + // You may get this if there are not more tokens and more are needed + // to complete a parse for instance. + // + ss <<"Syntax error."; + break; + + case ANTLR3_MISMATCHED_TOKEN_EXCEPTION: + + // We were expecting to see one thing and got another. This is the + // most common error if we could not detect a missing or unwanted token. + // Here you can spend your efforts to + // derive more useful error messages based on the expected + // token set and the last token and so on. The error following + // bitmaps do a good job of reducing the set that we were looking + // for down to something small. Knowing what you are parsing may be + // able to allow you to be even more specific about an error. + // + if(tokenNames == NULL) { + ss << "Syntax error."; + } else { + if(ex->expecting == ANTLR3_TOKEN_EOF) { + ss << "Expected end of file."; + } else { + ss << "Expected " << tokenNames[ex->expecting] << "."; + } + } + break; + + case ANTLR3_NO_VIABLE_ALT_EXCEPTION: + // We could not pick any alt decision from the input given + // so god knows what happened - however when you examine your grammar, + // you should. It means that at the point where the current token occurred + // that the DFA indicates nowhere to go from here. + // + ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; + break; + + case ANTLR3_MISMATCHED_SET_EXCEPTION: + + { + ANTLR3_UINT32 count; + ANTLR3_UINT32 bit; + ANTLR3_UINT32 size; + ANTLR3_UINT32 numbits; + pANTLR3_BITSET errBits; + + // This means we were able to deal with one of a set of + // possible tokens at this point, but we did not see any + // member of that set. + // + ss << "Unexpected input: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) + << "'. Expected one of: "; + + // What tokens could we have accepted at this point in the + // parse? + // + count = 0; + errBits = antlr3BitsetLoad(ex->expectingSet); + numbits = errBits->numBits(errBits); + size = errBits->size(errBits); + + if(size > 0) { + // However many tokens we could have dealt with here, it is usually + // not useful to print ALL of the set here. I arbitrarily chose 8 + // here, but you should do whatever makes sense for you of course. + // No token number 0, so look for bit 1 and on. + // + for(bit = 1; bit < numbits && count < 8 && count < size; bit++) { + // TODO: This doesn;t look right - should be asking if the bit is set!! + // + if(tokenNames[bit]) { + if( count++ > 0 ) { + ss << ", "; + } + ss << tokenNames[bit]; + } + } + } else { + Unreachable("Parse error with empty set of expected tokens."); + } + } + break; + + case ANTLR3_EARLY_EXIT_EXCEPTION: + + // We entered a loop requiring a number of token sequences + // but found a token that ended that sequence earlier than + // we should have done. + // + ss << "Sequence terminated early by token: '" + << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; + break; + + default: + + // We don't handle any other exceptions here, but you can + // if you wish. If we get an exception that hits this point + // then we are just going to report what we know about the + // token. + // + Unhandled("Unexpected exception in parser."); + break; + } + + // Now get ready to throw an exception + pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); + AlwaysAssert(antlr3Parser!=NULL); + Parser *parser = (Parser*)(antlr3Parser->super); + AlwaysAssert(parser!=NULL); + Input *input = parser->getInput(); + AlwaysAssert(input!=NULL); + + // Call the error display routine + input->parseError(ss.str()); +} + +} // namespace parser +} // namespace CVC4 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp new file mode 100644 index 000000000..01cc99c3d --- /dev/null +++ b/src/parser/parser.cpp @@ -0,0 +1,257 @@ +/********************* */ +/** parser.cpp + ** Original author: cconway + ** Major contributors: dejan, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Parser state implementation. + **/ + +#include +#include +#include + +#include "input.h" +#include "parser.h" +#include "parser_exception.h" +#include "expr/command.h" +#include "expr/expr.h" +#include "expr/kind.h" +#include "expr/type.h" +#include "util/output.h" +#include "util/Assert.h" +#include "parser/cvc/cvc_input.h" +#include "parser/smt/smt_input.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace parser { + +Parser::Parser(ExprManager* exprManager, Input* input) : + d_exprManager(exprManager), + d_input(input), + d_done(false), + d_checksEnabled(true) { + d_input->setParser(this); +} + +Expr Parser::getSymbol(const std::string& name, SymbolType type) { + Assert( isDeclared(name, type) ); + + switch( type ) { + + case SYM_VARIABLE: // Functions share var namespace + return d_declScope.lookup(name); + + default: + Unhandled(type); + } +} + + +Expr Parser::getVariable(const std::string& name) { + return getSymbol(name, SYM_VARIABLE); +} + +Type +Parser::getType(const std::string& var_name, + SymbolType type) { + Assert( isDeclared(var_name, type) ); + Type t = getSymbol(var_name,type).getType(); + return t; +} + +Type Parser::getSort(const std::string& name) { + Assert( isDeclared(name, SYM_SORT) ); + Type t = d_declScope.lookupType(name); + return t; +} + +/* Returns true if name is bound to a boolean variable. */ +bool Parser::isBoolean(const std::string& name) { + return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean(); +} + +/* Returns true if name is bound to a function. */ +bool Parser::isFunction(const std::string& name) { + return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction(); +} + +/* Returns true if name is bound to a function returning boolean. */ +bool Parser::isPredicate(const std::string& name) { + return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); +} + +Expr +Parser::mkVar(const std::string& name, const Type& type) { + Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl; + Expr expr = d_exprManager->mkVar(name, type); + defineVar(name,expr); + return expr; +} + +const std::vector +Parser::mkVars(const std::vector names, + const Type& type) { + std::vector vars; + for(unsigned i = 0; i < names.size(); ++i) { + vars.push_back(mkVar(names[i],type)); + } + return vars; +} + +void +Parser::defineVar(const std::string& name, const Expr& val) { + Assert(!isDeclared(name)); + d_declScope.bind(name,val); + Assert(isDeclared(name)); +} + +void +Parser::defineType(const std::string& name, const Type& type) { + Assert( !isDeclared(name, SYM_SORT) ); + d_declScope.bindType(name,type); + Assert( isDeclared(name, SYM_SORT) ) ; +} + +Type +Parser::mkSort(const std::string& name) { + Debug("parser") << "newSort(" << name << ")" << std::endl; + Type type = d_exprManager->mkSort(name); + defineType(name,type); + return type; +} + +const std::vector +Parser::mkSorts(const std::vector& names) { + std::vector types; + for(unsigned i = 0; i < names.size(); ++i) { + types.push_back(mkSort(names[i])); + } + return types; +} + +bool Parser::isDeclared(const std::string& name, SymbolType type) { + switch(type) { + case SYM_VARIABLE: + return d_declScope.isBound(name); + case SYM_SORT: + return d_declScope.isBoundType(name); + default: + Unhandled(type); + } +} + +void Parser::checkDeclaration(const std::string& varName, + DeclarationCheck check, + SymbolType type) + throw (ParserException) { + if(!d_checksEnabled) { + return; + } + + switch(check) { + case CHECK_DECLARED: + if( !isDeclared(varName, type) ) { + parseError("Symbol " + varName + " not declared"); + } + break; + + case CHECK_UNDECLARED: + if( isDeclared(varName, type) ) { + parseError("Symbol " + varName + " previously declared"); + } + break; + + case CHECK_NONE: + break; + + default: + Unhandled(check); + } +} + +void Parser::checkFunction(const std::string& name) + throw (ParserException) { + if( d_checksEnabled && !isFunction(name) ) { + parseError("Expecting function symbol, found '" + name + "'"); + } +} + +void Parser::checkArity(Kind kind, unsigned int numArgs) + throw (ParserException) { + if(!d_checksEnabled) { + return; + } + + unsigned int min = d_exprManager->minArity(kind); + unsigned int max = d_exprManager->maxArity(kind); + + if( numArgs < min || numArgs > max ) { + stringstream ss; + ss << "Expecting "; + if( numArgs < min ) { + ss << "at least " << min << " "; + } else { + ss << "at most " << max << " "; + } + ss << "arguments for operator '" << kind << "', "; + ss << "found " << numArgs; + parseError(ss.str()); + } +} + +void Parser::enableChecks() { + d_checksEnabled = true; +} + +void Parser::disableChecks() { + d_checksEnabled = false; +} + +Command* Parser::nextCommand() throw(ParserException) { + Debug("parser") << "nextCommand()" << std::endl; + Command* cmd = NULL; + if(!done()) { + try { + cmd = d_input->parseCommand(); + if(cmd == NULL) { + setDone(); + } + } catch(ParserException& e) { + setDone(); + throw; + } + } + Debug("parser") << "nextCommand() => " << cmd << std::endl; + return cmd; +} + +Expr Parser::nextExpression() throw(ParserException) { + Debug("parser") << "nextExpression()" << std::endl; + Expr result; + if(!done()) { + try { + result = d_input->parseExpr(); + if(result.isNull()) + setDone(); + } catch(ParserException& e) { + setDone(); + throw; + } + } + Debug("parser") << "nextExpression() => " << result << std::endl; + return result; +} + + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h new file mode 100644 index 000000000..a84021c10 --- /dev/null +++ b/src/parser/parser.h @@ -0,0 +1,283 @@ +/********************* */ +/** parser.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** A collection of state for use by parser implementations. + **/ + +#include "cvc4parser_private.h" + +#ifndef __CVC4__PARSER__PARSER_STATE_H +#define __CVC4__PARSER__PARSER_STATE_H + +#include + +#include "input.h" +#include "parser_exception.h" +#include "parser_options.h" +#include "expr/declaration_scope.h" +#include "expr/expr.h" +#include "expr/kind.h" +#include "util/Assert.h" + +namespace CVC4 { + +// Forward declarations +class BooleanType; +class ExprManager; +class Command; +class FunctionType; +class KindType; +class Type; + +namespace parser { + +/** Types of check for the symols */ +enum DeclarationCheck { + /** Enforce that the symbol has been declared */ + CHECK_DECLARED, + /** Enforce that the symbol has not been declared */ + CHECK_UNDECLARED, + /** Don't check anything */ + CHECK_NONE +}; + +/** Returns a string representation of the given object (for + debugging). */ +inline std::string toString(DeclarationCheck check) { + switch(check) { + case CHECK_NONE: + return "CHECK_NONE"; + case CHECK_DECLARED: + return "CHECK_DECLARED"; + case CHECK_UNDECLARED: + return "CHECK_UNDECLARED"; + default: + Unreachable(); + } +} + +/** + * Types of symbols. Used to define namespaces. + */ +enum SymbolType { + /** Variables */ + SYM_VARIABLE, + /** Sorts */ + SYM_SORT +}; + +/** Returns a string representation of the given object (for + debugging). */ +inline std::string toString(SymbolType type) { + switch(type) { + case SYM_VARIABLE: + return "SYM_VARIABLE"; + case SYM_SORT: + return "SYM_SORT"; + default: + Unreachable(); + } +} + +/** + * This class encapsulates all of the state of a parser, including the + * name of the file, line number and column information, and in-scope + * declarations. + */ +class CVC4_PUBLIC Parser { + + /** The expression manager */ + ExprManager *d_exprManager; + + /** The input that we're parsing. */ + Input *d_input; + + /** The symbol table */ + DeclarationScope d_declScope; + + /** The name of the input file. */ +// std::string d_filename; + + /** Are we done */ + bool d_done; + + /** Are semantic checks enabled during parsing? */ + bool d_checksEnabled; + + + /** Lookup a symbol in the given namespace. */ + Expr getSymbol(const std::string& var_name, SymbolType type); + +public: + /** Create a parser state. + * + * @param exprManager the expression manager to use when creating expressions + * @param input the parser input + */ + Parser(ExprManager* exprManager, Input* input); + + virtual ~Parser() { } + + /** Get the associated ExprManager. */ + inline ExprManager* getExprManager() const { + return d_exprManager; + } + + /** Get the associated input. */ + inline Input* getInput() const { + return d_input; + } + + /** Set the declaration scope manager for this input. NOTE: This should only be + * called before parsing begins. Otherwise, previous declarations will be lost. */ + inline void setDeclarationScope(DeclarationScope declScope) { + d_declScope = declScope; + } + + /** + * Check if we are done -- either the end of input has been reached, or some + * error has been encountered. + * @return true if parser is done + */ + inline bool done() const { + return d_done; + } + + /** Sets the done flag */ + inline void setDone(bool done = true) { + d_done = done; + } + + /** Enable semantic checks during parsing. */ + void enableChecks(); + + /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */ + void disableChecks(); + + /** Get the name of the input file. */ +/* + inline const std::string getFilename() { + return d_filename; + } +*/ + + /** + * Sets the logic for the current benchmark. Declares any logic symbols. + * + * @param name the name of the logic (e.g., QF_UF, AUFLIA) + */ + void setLogic(const std::string& name); + + /** + * Returns a variable, given a name and a type. + * @param var_name the name of the variable + * @return the variable expression + */ + Expr getVariable(const std::string& var_name); + + /** + * Returns a sort, given a name + */ + Type getSort(const std::string& sort_name); + + /** + * Checks if a symbol has been declared. + * @param name the symbol name + * @param type the symbol type + * @return true iff the symbol has been declared with the given type + */ + bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE); + + /** + * Checks if the declaration policy we want to enforce holds + * for the given symbol. + * @param name the symbol to check + * @param check the kind of check to perform + * @param type the type of the symbol + * @throws ParserException if checks are enabled and the check fails + */ + void checkDeclaration(const std::string& name, DeclarationCheck check, + SymbolType type = SYM_VARIABLE) throw (ParserException); + + /** + * Checks whether the given name is bound to a function. + * @param name the name to check + * @throws ParserException if checks are enabled and name is not bound to a function + */ + void checkFunction(const std::string& name) throw (ParserException); + + /** + * Check that kind can accept numArgs arguments. + * @param kind the built-in operator to check + * @param numArgs the number of actual arguments + * @throws ParserException if checks are enabled and the operator kind cannot be + * applied to numArgs arguments. + */ + void checkArity(Kind kind, unsigned int numArgs) throw (ParserException); + + /** + * Returns the type for the variable with the given name. + * @param var_name the symbol to lookup + * @param type the (namespace) type of the symbol + */ + Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); + + /** Create a new CVC4 variable expression of the given type. */ + Expr mkVar(const std::string& name, const Type& type); + + /** Create a set of new CVC4 variable expressions of the given + type. */ + const std::vector + mkVars(const std::vector names, const Type& type); + + /** Create a new variable definition (e.g., from a let binding). */ + void defineVar(const std::string& name, const Expr& val); + + /** Create a new type definition. */ + void defineType(const std::string& name, const Type& type); + + /** + * Creates a new sort with the given name. + */ + Type mkSort(const std::string& name); + + /** + * Creates a new sorts with the given names. + */ + const std::vector + mkSorts(const std::vector& names); + + /** Is the symbol bound to a boolean variable? */ + bool isBoolean(const std::string& name); + + /** Is the symbol bound to a function? */ + bool isFunction(const std::string& name); + + /** Is the symbol bound to a predicate? */ + bool isPredicate(const std::string& name); + + Command* nextCommand() throw(ParserException); + Expr nextExpression() throw(ParserException); + + inline void parseError(const std::string& msg) throw (ParserException) { + d_input->parseError(msg); + } + + inline void pushScope() { d_declScope.pushScope(); } + inline void popScope() { d_declScope.popScope(); } +}; // class Parser + +} // namespace parser + +} // namespace CVC4 + +#endif /* __CVC4__PARSER__PARSER_STATE_H */ diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp deleted file mode 100644 index 204dd3469..000000000 --- a/src/parser/parser_state.cpp +++ /dev/null @@ -1,217 +0,0 @@ -/********************* */ -/** parser_state.cpp - ** Original author: cconway - ** Major contributors: dejan, mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Parser state implementation. - **/ - -#include -#include -#include - -#include "input.h" -#include "expr/command.h" -#include "expr/expr.h" -#include "expr/kind.h" -#include "expr/type.h" -#include "util/output.h" -#include "util/Assert.h" -#include "parser/parser_exception.h" -#include "parser/symbol_table.h" -#include "parser/cvc/cvc_input.h" -#include "parser/smt/smt_input.h" - -using namespace std; -using namespace CVC4::kind; - -namespace CVC4 { -namespace parser { - -ParserState::ParserState(ExprManager* exprManager, const std::string& filename, Input* input) : - d_exprManager(exprManager), - d_input(input), - d_filename(filename), - d_done(false), - d_checksEnabled(true) { -} - -Expr ParserState::getSymbol(const std::string& name, SymbolType type) { - Assert( isDeclared(name, type) ); - - switch( type ) { - - case SYM_VARIABLE: // Functions share var namespace - return d_declScope.lookup(name); - - default: - Unhandled(type); - } -} - - -Expr ParserState::getVariable(const std::string& name) { - return getSymbol(name, SYM_VARIABLE); -} - -Type -ParserState::getType(const std::string& var_name, - SymbolType type) { - Assert( isDeclared(var_name, type) ); - Type t = getSymbol(var_name,type).getType(); - return t; -} - -Type ParserState::getSort(const std::string& name) { - Assert( isDeclared(name, SYM_SORT) ); - Type t = d_declScope.lookupType(name); - return t; -} - -/* Returns true if name is bound to a boolean variable. */ -bool ParserState::isBoolean(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean(); -} - -/* Returns true if name is bound to a function. */ -bool ParserState::isFunction(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction(); -} - -/* Returns true if name is bound to a function returning boolean. */ -bool ParserState::isPredicate(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); -} - -Expr -ParserState::mkVar(const std::string& name, const Type& type) { - Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl; - Expr expr = d_exprManager->mkVar(name, type); - defineVar(name,expr); - return expr; -} - -const std::vector -ParserState::mkVars(const std::vector names, - const Type& type) { - std::vector vars; - for(unsigned i = 0; i < names.size(); ++i) { - vars.push_back(mkVar(names[i],type)); - } - return vars; -} - -void -ParserState::defineVar(const std::string& name, const Expr& val) { - Assert(!isDeclared(name)); - d_declScope.bind(name,val); - Assert(isDeclared(name)); -} - -Type -ParserState::mkSort(const std::string& name) { - Debug("parser") << "newSort(" << name << ")" << std::endl; - Assert( !isDeclared(name, SYM_SORT) ) ; - Type type = d_exprManager->mkSort(name); - d_declScope.bindType(name, type); - Assert( isDeclared(name, SYM_SORT) ) ; - return type; -} - -const std::vector -ParserState::mkSorts(const std::vector& names) { - std::vector types; - for(unsigned i = 0; i < names.size(); ++i) { - types.push_back(mkSort(names[i])); - } - return types; -} - -bool ParserState::isDeclared(const std::string& name, SymbolType type) { - switch(type) { - case SYM_VARIABLE: - return d_declScope.isBound(name); - case SYM_SORT: - return d_declScope.isBoundType(name); - default: - Unhandled(type); - } -} - -void ParserState::checkDeclaration(const std::string& varName, - DeclarationCheck check, - SymbolType type) - throw (ParserException) { - if(!d_checksEnabled) { - return; - } - - switch(check) { - case CHECK_DECLARED: - if( !isDeclared(varName, type) ) { - parseError("Symbol " + varName + " not declared"); - } - break; - - case CHECK_UNDECLARED: - if( isDeclared(varName, type) ) { - parseError("Symbol " + varName + " previously declared"); - } - break; - - case CHECK_NONE: - break; - - default: - Unhandled(check); - } -} - -void ParserState::checkFunction(const std::string& name) - throw (ParserException) { - if( d_checksEnabled && !isFunction(name) ) { - parseError("Expecting function symbol, found '" + name + "'"); - } -} - -void ParserState::checkArity(Kind kind, unsigned int numArgs) - throw (ParserException) { - if(!d_checksEnabled) { - return; - } - - unsigned int min = d_exprManager->minArity(kind); - unsigned int max = d_exprManager->maxArity(kind); - - if( numArgs < min || numArgs > max ) { - stringstream ss; - ss << "Expecting "; - if( numArgs < min ) { - ss << "at least " << min << " "; - } else { - ss << "at most " << max << " "; - } - ss << "arguments for operator '" << kind << "', "; - ss << "found " << numArgs; - parseError(ss.str()); - } -} - -void ParserState::enableChecks() { - d_checksEnabled = true; -} - -void ParserState::disableChecks() { - d_checksEnabled = false; -} - - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h deleted file mode 100644 index 3ca9c2c0e..000000000 --- a/src/parser/parser_state.h +++ /dev/null @@ -1,266 +0,0 @@ -/********************* */ -/** parser_state.h - ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** A collection of state for use by parser implementations. - **/ - -#include "cvc4parser_private.h" - -#ifndef __CVC4__PARSER__PARSER_STATE_H -#define __CVC4__PARSER__PARSER_STATE_H - -#include - -#include "expr/declaration_scope.h" -#include "expr/expr.h" -#include "expr/kind.h" -#include "parser/input.h" -#include "parser/parser_exception.h" -#include "parser/parser_options.h" -#include "parser/symbol_table.h" -#include "util/Assert.h" - -namespace CVC4 { - -// Forward declarations -class BooleanType; -class ExprManager; -class Command; -class FunctionType; -class KindType; -class Type; - -namespace parser { - -/** Types of check for the symols */ -enum DeclarationCheck { - /** Enforce that the symbol has been declared */ - CHECK_DECLARED, - /** Enforce that the symbol has not been declared */ - CHECK_UNDECLARED, - /** Don't check anything */ - CHECK_NONE -}; - -/** Returns a string representation of the given object (for - debugging). */ -inline std::string toString(DeclarationCheck check) { - switch(check) { - case CHECK_NONE: - return "CHECK_NONE"; - case CHECK_DECLARED: - return "CHECK_DECLARED"; - case CHECK_UNDECLARED: - return "CHECK_UNDECLARED"; - default: - Unreachable(); - } -} - -/** - * Types of symbols. Used to define namespaces. - */ -enum SymbolType { - /** Variables */ - SYM_VARIABLE, - /** Sorts */ - SYM_SORT -}; - -/** Returns a string representation of the given object (for - debugging). */ -inline std::string toString(SymbolType type) { - switch(type) { - case SYM_VARIABLE: - return "SYM_VARIABLE"; - case SYM_SORT: - return "SYM_SORT"; - default: - Unreachable(); - } -} - -class ParserState { - - /** The expression manager */ - ExprManager *d_exprManager; - - /** The input that we're parsing. */ - Input *d_input; - - /** The symbol table */ - DeclarationScope d_declScope; - - /** The name of the input file. */ - std::string d_filename; - - /** Are we done */ - bool d_done; - - /** Are semantic checks enabled during parsing? */ - bool d_checksEnabled; - - - /** Lookup a symbol in the given namespace. */ - Expr getSymbol(const std::string& var_name, SymbolType type); - -public: - ParserState(ExprManager* exprManager, const std::string& filename, Input* input); - - /** Get the associated ExprManager. */ - inline ExprManager* getExprManager() const { - return d_exprManager; - } - - /** Get the associated input. */ - inline Input* getInput() const { - return d_input; - } - - /** Set the declaration scope manager for this input. NOTE: This should only be - * called before parsing begins. Otherwise, previous declarations will be lost. */ - inline void setDeclarationScope(DeclarationScope declScope) { - d_declScope = declScope; - } - - /** - * Check if we are done -- either the end of input has been reached, or some - * error has been encountered. - * @return true if parser is done - */ - inline bool done() const { - return d_done; - } - - /** Sets the done flag */ - inline void setDone(bool done = true) { - d_done = done; - } - - /** Enable semantic checks during parsing. */ - void enableChecks(); - - /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */ - void disableChecks(); - - /** Get the name of the input file. */ - inline const std::string getFilename() { - return d_filename; - } - - /** - * Sets the logic for the current benchmark. Declares any logic symbols. - * - * @param name the name of the logic (e.g., QF_UF, AUFLIA) - */ - void setLogic(const std::string& name); - - /** - * Returns a variable, given a name and a type. - * @param var_name the name of the variable - * @return the variable expression - */ - Expr getVariable(const std::string& var_name); - - /** - * Returns a sort, given a name - */ - Type getSort(const std::string& sort_name); - - /** - * Checks if a symbol has been declared. - * @param name the symbol name - * @param type the symbol type - * @return true iff the symbol has been declared with the given type - */ - bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE); - - /** - * Checks if the declaration policy we want to enforce holds - * for the given symbol. - * @param name the symbol to check - * @param check the kind of check to perform - * @param type the type of the symbol - * @throws ParserException if checks are enabled and the check fails - */ - void checkDeclaration(const std::string& name, DeclarationCheck check, - SymbolType type = SYM_VARIABLE) throw (ParserException); - - /** - * Checks whether the given name is bound to a function. - * @param name the name to check - * @throws ParserException if checks are enabled and name is not bound to a function - */ - void checkFunction(const std::string& name) throw (ParserException); - - /** - * Check that kind can accept numArgs arguments. - * @param kind the built-in operator to check - * @param numArgs the number of actual arguments - * @throws ParserException if checks are enabled and the operator kind cannot be - * applied to numArgs arguments. - */ - void checkArity(Kind kind, unsigned int numArgs) throw (ParserException); - - /** - * Returns the type for the variable with the given name. - * @param var_name the symbol to lookup - * @param type the (namespace) type of the symbol - */ - Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); - - /** Create a new CVC4 variable expression of the given type. */ - Expr mkVar(const std::string& name, const Type& type); - - /** Create a set of new CVC4 variable expressions of the given - type. */ - const std::vector - mkVars(const std::vector names, const Type& type); - - /** Create a new variable definition (e.g., from a let binding). */ - void defineVar(const std::string& name, const Expr& val); - /** Remove a variable definition (e.g., from a let binding). */ - void undefineVar(const std::string& name); - - /** - * Creates a new sort with the given name. - */ - Type mkSort(const std::string& name); - - /** - * Creates a new sorts with the given names. - */ - const std::vector - mkSorts(const std::vector& names); - - /** Is the symbol bound to a boolean variable? */ - bool isBoolean(const std::string& name); - - /** Is the symbol bound to a function? */ - bool isFunction(const std::string& name); - - /** Is the symbol bound to a predicate? */ - bool isPredicate(const std::string& name); - - inline void parseError(const std::string& msg) throw (ParserException) { - d_input->parseError(msg); - } - - inline void pushScope() { d_declScope.pushScope(); } - inline void popScope() { d_declScope.popScope(); } -}; // class ParserState - -} // namespace parser - -} // namespace CVC4 - -#endif /* __CVC4__PARSER__PARSER_STATE_H */ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 4539a6d43..cf22c5290 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -50,7 +50,7 @@ options { @parser::includes { #include "expr/command.h" -#include "parser/parser_state.h" +#include "parser/parser.h" namespace CVC4 { class Expr; @@ -61,8 +61,8 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "parser/antlr_input.h" -#include "parser/parser_state.h" +#include "parser/input.h" +#include "parser/parser.h" #include "util/integer.h" #include "util/output.h" #include "util/rational.h" @@ -74,7 +74,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ #undef PARSER_STATE -#define PARSER_STATE ((ParserState*)PARSER->super) +#define PARSER_STATE ((Parser*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR @@ -85,11 +85,11 @@ using namespace CVC4::parser; /** * Sets the logic for the current benchmark. Declares any logic symbols. * - * @param parserState pointer to the current parser state + * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ void -setLogic(ParserState *parserState, const std::string& name) { +setLogic(Parser *parser, const std::string& name) { if( name == "QF_UF" ) { parserState->mkSort("U"); } else if(name == "QF_LRA"){ @@ -174,7 +174,7 @@ benchAttribute returns [CVC4::Command* smt_command] */ annotatedFormula[CVC4::Expr& expr] @init { - Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser") << "annotated formula: " << Input::tokenText(LT(1)) << std::endl; Kind kind; std::string name; std::vector args; /* = getExprVector(); */ @@ -236,11 +236,11 @@ annotatedFormula[CVC4::Expr& expr] | TRUE_TOK { expr = MK_CONST(true); } | FALSE_TOK { expr = MK_CONST(false); } | NUMERAL_TOK - { Integer num( AntlrInput::tokenText($NUMERAL_TOK) ); + { Integer num( Input::tokenText($NUMERAL_TOK) ); expr = MK_CONST(num); } | RATIONAL_TOK { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string - Rational rat( AntlrInput::tokenText($RATIONAL_TOK) ); + Rational rat( Input::tokenText($RATIONAL_TOK) ); expr = MK_CONST(rat); } // NOTE: Theory constants go here /* TODO: let, flet, quantifiers, arithmetic constants */ @@ -263,7 +263,7 @@ annotatedFormulas[std::vector& formulas, CVC4::Expr& expr] */ builtinOp[CVC4::Kind& kind] @init { - Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser") << "builtin: " << Input::tokenText(LT(1)) << std::endl; } : NOT_TOK { $kind = CVC4::kind::NOT; } | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; } @@ -417,7 +417,7 @@ identifier[std::string& id, CVC4::parser::DeclarationCheck check, CVC4::parser::SymbolType type] : IDENTIFIER - { id = AntlrInput::tokenText($IDENTIFIER); + { id = Input::tokenText($IDENTIFIER); Debug("parser") << "identifier: " << id << " check? " << toString(check) << " type? " << toString(type) << std::endl; @@ -432,7 +432,7 @@ identifier[std::string& id, let_identifier[std::string& id, CVC4::parser::DeclarationCheck check] : LET_IDENTIFIER - { id = AntlrInput::tokenText($LET_IDENTIFIER); + { id = Input::tokenText($LET_IDENTIFIER); Debug("parser") << "let_identifier: " << id << " check? " << toString(check) << std::endl; PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); } @@ -446,7 +446,7 @@ let_identifier[std::string& id, flet_identifier[std::string& id, CVC4::parser::DeclarationCheck check] : FLET_IDENTIFIER - { id = AntlrInput::tokenText($FLET_IDENTIFIER); + { id = Input::tokenText($FLET_IDENTIFIER); Debug("parser") << "flet_identifier: " << id << " check? " << toString(check) << std::endl; PARSER_STATE->checkDeclaration(id, check); } diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp index 1bff3d18f..451310cfd 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -15,9 +15,10 @@ #include +#include "smt_input.h" #include "expr/expr_manager.h" +#include "parser/parser.h" #include "parser/parser_exception.h" -#include "parser/smt/smt_input.h" #include "parser/smt/generated/SmtLexer.h" #include "parser/smt/generated/SmtParser.h" @@ -25,20 +26,9 @@ namespace CVC4 { namespace parser { /* Use lookahead=2 */ -SmtInput::SmtInput(ExprManager* exprManager, const std::string& filename, - bool useMmap) : - AntlrInput(exprManager, filename, 2, useMmap) { - init(); -} - -SmtInput::SmtInput(ExprManager* exprManager, const std::string& input, - const std::string& name) : - AntlrInput(exprManager, input, name, 2) { - init(); -} - -void SmtInput::init() { - pANTLR3_INPUT_STREAM input = getInputStream(); +SmtInput::SmtInput(AntlrInputStream *inputStream) : + Input(inputStream, 2) { + pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); AlwaysAssert( input != NULL ); d_pSmtLexer = SmtLexerNew(input); @@ -46,7 +36,7 @@ void SmtInput::init() { throw ParserException("Failed to create SMT lexer."); } - setLexer( d_pSmtLexer->pLexer ); + setAntlr3Lexer( d_pSmtLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); AlwaysAssert( tokenStream != NULL ); @@ -56,7 +46,7 @@ void SmtInput::init() { throw ParserException("Failed to create SMT parser."); } - setParser(d_pSmtParser->pParser); + setAntlr3Parser(d_pSmtParser->pParser); } @@ -65,11 +55,11 @@ SmtInput::~SmtInput() { d_pSmtParser->free(d_pSmtParser); } -Command* SmtInput::doParseCommand() throw (ParserException) { +Command* SmtInput::parseCommand() throw (ParserException) { return d_pSmtParser->parseCommand(d_pSmtParser); } -Expr SmtInput::doParseExpr() throw (ParserException) { +Expr SmtInput::parseExpr() throw (ParserException) { return d_pSmtParser->parseExpr(d_pSmtParser); } diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index f93a1bf0d..e9f4d2578 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -18,7 +18,7 @@ #ifndef __CVC4__PARSER__SMT_INPUT_H #define __CVC4__PARSER__SMT_INPUT_H -#include "parser/antlr_input.h" +#include "parser/input.h" #include "parser/smt/generated/SmtLexer.h" #include "parser/smt/generated/SmtParser.h" @@ -32,7 +32,7 @@ class ExprManager; namespace parser { -class SmtInput : public AntlrInput { +class SmtInput : public Input { /** The ANTLR3 SMT lexer for the input. */ pSmtLexer d_pSmtLexer; @@ -43,14 +43,11 @@ class SmtInput : public AntlrInput { public: /** - * Create a file input. + * Create an input. * - * @param exprManager the manager to use when building expressions from the input - * @param filename the path of the file to read - * @param useMmap true if the input should use memory-mapped - * I/O; otherwise, the input will use the standard ANTLR3 I/O implementation. + * @param inputStream the input stream to use */ - SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap); + SmtInput(AntlrInputStream *inputStream); /** * Create a string input. @@ -59,7 +56,7 @@ public: * @param input the string to read * @param name the "filename" to use when reporting errors */ - SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name); +// SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name); /** Destructor. Frees the lexer and the parser. */ ~SmtInput(); @@ -72,7 +69,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* doParseCommand() throw(ParserException); + Command* parseCommand() throw(ParserException); /** * Parse an expression from the input. Returns a null @@ -80,7 +77,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr doParseExpr() throw(ParserException); + Expr parseExpr() throw(ParserException); private: diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h deleted file mode 100644 index d6467f4e9..000000000 --- a/src/parser/symbol_table.h +++ /dev/null @@ -1,105 +0,0 @@ -/********************* */ -/** symbol_table.h - ** Original author: cconway - ** Major contributors: dejan, mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** A symbol table for the parsers' use. - **/ - -#include "cvc4parser_private.h" - -#ifndef __CVC4__PARSER__SYMBOL_TABLE_H -#define __CVC4__PARSER__SYMBOL_TABLE_H - -#include -#include - -#include - -#include "util/Assert.h" - -namespace CVC4 { -namespace parser { - -struct StringHashFunction { - size_t operator()(const std::string& str) const { - return __gnu_cxx::hash()(str.c_str()); - } -}; - -/** - * Generic symbol table for looking up variables by name. - */ -template -class SymbolTable { - -private: - - /** The name to expression bindings */ - typedef __gnu_cxx::hash_map - LookupTable; - - /** The table iterator */ - typedef typename LookupTable::iterator table_iterator; - /** The table iterator */ - typedef typename LookupTable::const_iterator const_table_iterator; - - /** Bindings for the names */ - LookupTable d_nameBindings; - -public: - - /** - * Bind the name of the variable to the given expression. If the variable - * has been bind before, this will redefine it until its undefined. - */ - void bindName(const std::string& name, const ObjectType& obj) throw () { - d_nameBindings[name] = obj; - Assert(isBound(name), "Expected name to be bound!"); - } - - /** - * Unbinds the last binding of the name to the expression. - */ - void unbindName(const std::string& name) throw () { - table_iterator find = d_nameBindings.find(name); - if(find != d_nameBindings.end()) { -/* - find->second.pop(); - if(find->second.empty()) { -*/ - d_nameBindings.erase(find); -/* }*/ - } - } - - /** - * Returns the last binding expression of the name. - * Requires the name to have a binding in the table. - */ - ObjectType getObject(const std::string& name) throw () { - table_iterator find = d_nameBindings.find(name); - Assert(find != d_nameBindings.end()); - return find->second; /*.top()*/ - } - - /** - * Returns true is name is bound to an expression. - */ - bool isBound(const std::string& name) const throw () { - const_table_iterator find = d_nameBindings.find(name); - return (find != d_nameBindings.end()); - } -}; - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__SYMBOL_TABLE_H */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 1f56434c9..666d1c285 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -10,7 +10,7 @@ UNIT_TESTS = \ expr/attribute_white \ expr/attribute_black \ expr/declaration_scope_black \ - parser/parser_white \ + parser/parser_black \ context/context_black \ context/context_white \ context/context_mm_black \ @@ -37,7 +37,7 @@ if HAVE_CXXTESTGEN AM_CPPFLAGS = \ -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \ - $(TEST_CPPFLAGS) + $(ANTLR_INCLUDES) $(TEST_CPPFLAGS) AM_CXXFLAGS = -Wall $(TEST_CXXFLAGS) AM_LDFLAGS = $(TEST_LDFLAGS) diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h new file mode 100644 index 000000000..9a2864781 --- /dev/null +++ b/test/unit/parser/parser_black.h @@ -0,0 +1,309 @@ +/********************* */ +/** parser_white.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan, mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** White box testing of CVC4::parser::SmtParser. + **/ + +#include +//#include +#include + +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "parser/input.h" +#include "parser/parser.h" +#include "expr/command.h" +#include "util/output.h" + +using namespace CVC4; +using namespace CVC4::parser; +using namespace std; + + +/************************** CVC test inputs ********************************/ + +const string goodCvc4Inputs[] = { + "", // empty string is OK + "ASSERT TRUE;", + "QUERY TRUE;", + "CHECKSAT FALSE;", + "a, b : BOOLEAN;", + "a, b : BOOLEAN; QUERY (a => b) AND a => b;", + "T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;", + "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;", + "%% nothing but a comment", + "% a comment\nASSERT TRUE; %a command\n% another comment", + }; + +const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string); + + +/* The following expressions are valid after setupContext. */ +const string goodCvc4Exprs[] = { + "a AND b", + "a AND b OR c", + "(a => b) AND a => b", + "(a <=> b) AND (NOT a)", + "(a XOR b) <=> (a OR b) AND (NOT (a AND b))" +}; + +const int numGoodCvc4Exprs = sizeof(goodCvc4Exprs) / sizeof(string); + +const string badCvc4Inputs[] = { + ";", // no command + "ASSERT;", // no args + "QUERY", + "CHECKSAT", + "a, b : boolean;", // lowercase boolean isn't a type + "0x : INT;", // 0x isn't an identifier + "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl + "a : BOOLEAN; a: BOOLEAN;" // double decl + "a, b: BOOLEAN; QUERY a(b);" // non-function used as function + }; + +const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string); + +/* The following expressions are invalid even after setupContext. */ +const string badCvc4Exprs[] = { + "a AND", // wrong arity + "AND(a,b)", // not infix + "(OR (AND a b) c)", // not infix + "a IMPLIES b", // should be => + "a NOT b", // wrong arity, not infix + "a and b" // wrong case +}; + +const int numBadCvc4Exprs = sizeof(badCvc4Exprs) / sizeof(string); + +/************************** SMT test inputs ********************************/ + +const string goodSmtInputs[] = { + "", // empty string is OK + "(benchmark foo :assumption true)", + "(benchmark bar :formula true)", + "(benchmark qux :formula false)", + "(benchmark baz :extrapreds ( (a) (b) ) )", + "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))", + "(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) ) :formula (= (f x) x))", + "(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))", + ";; nothing but a comment", + "; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)" + }; + +const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string); + +/* The following expressions are valid after setupContext. */ +const string goodSmtExprs[] = { + "(and a b)", + "(or (and a b) c)", + "(implies (and (implies a b) a) b)", + "(and (iff a b) (not a))", + "(iff (xor a b) (and (or a b) (not (and a b))))", + "(ite a (f x) y)", + "(if_then_else a (f x) y)", + "1", + "0"// , +// "1.5" +}; + +const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); + +const string badSmtInputs[] = { + "(benchmark foo)", // empty benchmark is not OK + "(benchmark bar :assumption)", // no args + "(benchmark bar :formula)", + "(benchmark baz :extrapreds ( (a) (a) ) )", // double decl + "(benchmark zub :extrasorts (a) :extrapreds (p a))" // (p a) needs parens + }; + +const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string); + +/* The following expressions are invalid even after setupContext. */ +const string badSmtExprs[] = { + "(and)", // wrong arity + "(and a b", // no closing paren + "(a and b)", // infix + "(OR (AND a b) c)", // wrong case + "(a IMPLIES b)", // infix AND wrong case + "(not a b)", // wrong arity + "not a", // needs parens + "(ite a x)", // wrong arity + "(a b)", // using non-function as function + ".5", // rational constants must have integer prefix + "1." // rational constants must have fractional suffix +}; + +const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); + +class ParserBlack : public CxxTest::TestSuite { + ExprManager *d_exprManager; + + /* Set up declaration context for expr inputs */ + + void setupContext(Parser& parser) { + /* a, b, c: BOOLEAN */ + parser.mkVar("a",d_exprManager->booleanType()); + parser.mkVar("b",d_exprManager->booleanType()); + parser.mkVar("c",d_exprManager->booleanType()); + /* t, u, v: TYPE */ + Type t = parser.mkSort("t"); + Type u = parser.mkSort("u"); + Type v = parser.mkSort("v"); + /* f : t->u; g: u->v; h: v->t; */ + parser.mkVar("f", d_exprManager->mkFunctionType(t,u)); + parser.mkVar("g", d_exprManager->mkFunctionType(u,v)); + parser.mkVar("h", d_exprManager->mkFunctionType(v,t)); + /* x:t; y:u; z:v; */ + parser.mkVar("x",t); + parser.mkVar("y",u); + parser.mkVar("z",v); + } + + void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) { + for(int i = 0; i < numInputs; ++i) { + try { +// Debug.on("parser"); +// Debug.on("parser-extra"); + Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n"; +// istringstream stream(goodInputs[i]); + Input* input = Input::newStringInput(d_lang, goodInputs[i], "test"); + Parser parser(d_exprManager, input); + TS_ASSERT( !parser.done() ); + Command* cmd; + while((cmd = parser.nextCommand()) != NULL) { + // cout << "Parsed command: " << (*cmd) << endl; + } + TS_ASSERT( parser.nextCommand() == NULL ); + TS_ASSERT( parser.done() ); + delete input; +// Debug.off("parser"); +// Debug.off("parser-extra"); + } catch (Exception& e) { + cout << "\nGood input failed:\n" << goodInputs[i] << endl + << e << endl; +// Debug.off("parser-extra"); + throw; + } + } + } + + void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) { + for(int i = 0; i < numInputs; ++i) { +// cout << "Testing bad input: '" << badInputs[i] << "'\n"; +// Debug.on("parser"); + Input* input = Input::newStringInput(d_lang, badInputs[i], "test"); + Parser parser(d_exprManager, input); + TS_ASSERT_THROWS + ( while(parser.nextCommand()); + cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, + ParserException ); +// Debug.off("parser"); + delete input; + } + } + + void tryGoodExprs(InputLanguage d_lang, const string goodBooleanExprs[], int numExprs) { + // cout << "Using context: " << context << endl; +// Debug.on("parser"); +// Debug.on("parser-extra"); + for(int i = 0; i < numExprs; ++i) { + try { + // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n"; + // Debug.on("parser"); +// istringstream stream(context + goodBooleanExprs[i]); + Input* input = Input::newStringInput(d_lang, + goodBooleanExprs[i], "test"); + Parser parser(d_exprManager, input); + TS_ASSERT( !parser.done() ); + setupContext(parser); + TS_ASSERT( !parser.done() ); + Expr e = parser.nextExpression(); + TS_ASSERT( !e.isNull() ); + e = parser.nextExpression(); + TS_ASSERT( parser.done() ); + TS_ASSERT( e.isNull() ); + delete input; + } catch (Exception& e) { + cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl; + cout << e; + throw; + } + } + } + + void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) { + //Debug.on("parser"); + for(int i = 0; i < numExprs; ++i) { + // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n"; +// istringstream stream(context + badBooleanExprs[i]); + Input* input = Input::newStringInput(d_lang, + badBooleanExprs[i], "test"); + Parser parser(d_exprManager, input); + + setupContext(parser); + TS_ASSERT( !parser.done() ); + TS_ASSERT_THROWS + ( parser.nextExpression(); + cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, + ParserException ); + delete input; + } + //Debug.off("parser"); + } + +public: + void setUp() { + d_exprManager = new ExprManager(); + } + + void tearDown() { + delete d_exprManager; + } + + void testBs() { + DeclarationScope declScope; + declScope.bind("foo", d_exprManager->mkVar("foo",d_exprManager->booleanType())); + + } + + void testGoodCvc4Inputs() { + tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); + } + + void testBadCvc4Inputs() { + tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs); + } + + void testGoodCvc4Exprs() { + tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs); + } + + void testBadCvc4Exprs() { + tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs); + } + + void testGoodSmtInputs() { + tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs); + } + + void testBadSmtInputs() { + tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs); + } + + void testGoodSmtExprs() { + tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs); + } + + void testBadSmtExprs() { + tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs); + } +}; diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h deleted file mode 100644 index 1d19525d6..000000000 --- a/test/unit/parser/parser_white.h +++ /dev/null @@ -1,306 +0,0 @@ -/********************* */ -/** parser_white.h - ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** White box testing of CVC4::parser::SmtParser. - **/ - -#include -//#include -#include - -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "parser/input.h" -#include "parser/parser_state.h" -#include "expr/command.h" -#include "util/output.h" - -using namespace CVC4; -using namespace CVC4::parser; -using namespace std; - - -/************************** CVC test inputs ********************************/ - -const string goodCvc4Inputs[] = { - "", // empty string is OK - "ASSERT TRUE;", - "QUERY TRUE;", - "CHECKSAT FALSE;", - "a, b : BOOLEAN;", - "a, b : BOOLEAN; QUERY (a => b) AND a => b;", - "T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;", - "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;", - "%% nothing but a comment", - "% a comment\nASSERT TRUE; %a command\n% another comment", - }; - -const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string); - - -/* The following expressions are valid after setupContext. */ -const string goodCvc4Exprs[] = { - "a AND b", - "a AND b OR c", - "(a => b) AND a => b", - "(a <=> b) AND (NOT a)", - "(a XOR b) <=> (a OR b) AND (NOT (a AND b))" -}; - -const int numGoodCvc4Exprs = sizeof(goodCvc4Exprs) / sizeof(string); - -const string badCvc4Inputs[] = { - ";", // no command - "ASSERT;", // no args - "QUERY", - "CHECKSAT", - "a, b : boolean;", // lowercase boolean isn't a type - "0x : INT;", // 0x isn't an identifier - "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl - "a : BOOLEAN; a: BOOLEAN;" // double decl - "a, b: BOOLEAN; QUERY a(b);" // non-function used as function - }; - -const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string); - -/* The following expressions are invalid even after setupContext. */ -const string badCvc4Exprs[] = { - "a AND", // wrong arity - "AND(a,b)", // not infix - "(OR (AND a b) c)", // not infix - "a IMPLIES b", // should be => - "a NOT b", // wrong arity, not infix - "a and b" // wrong case -}; - -const int numBadCvc4Exprs = sizeof(badCvc4Exprs) / sizeof(string); - -/************************** SMT test inputs ********************************/ - -const string goodSmtInputs[] = { - "", // empty string is OK - "(benchmark foo :assumption true)", - "(benchmark bar :formula true)", - "(benchmark qux :formula false)", - "(benchmark baz :extrapreds ( (a) (b) ) )", - "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))", - "(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) ) :formula (= (f x) x))", - "(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))", - ";; nothing but a comment", - "; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)" - }; - -const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string); - -/* The following expressions are valid after setupContext. */ -const string goodSmtExprs[] = { - "(and a b)", - "(or (and a b) c)", - "(implies (and (implies a b) a) b)", - "(and (iff a b) (not a))", - "(iff (xor a b) (and (or a b) (not (and a b))))", - "(ite a (f x) y)", - "(if_then_else a (f x) y)", - "1", - "0"// , -// "1.5" -}; - -const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); - -const string badSmtInputs[] = { - "(benchmark foo)", // empty benchmark is not OK - "(benchmark bar :assumption)", // no args - "(benchmark bar :formula)", - "(benchmark baz :extrapreds ( (a) (a) ) )", // double decl - "(benchmark zub :extrasorts (a) :extrapreds (p a))" // (p a) needs parens - }; - -const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string); - -/* The following expressions are invalid even after setupContext. */ -const string badSmtExprs[] = { - "(and)", // wrong arity - "(and a b", // no closing paren - "(a and b)", // infix - "(OR (AND a b) c)", // wrong case - "(a IMPLIES b)", // infix AND wrong case - "(not a b)", // wrong arity - "not a", // needs parens - "(ite a x)", // wrong arity - "(a b)", // using non-function as function - ".5", // rational constants must have integer prefix - "1." // rational constants must have fractional suffix -}; - -const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); - -class ParserWhite : public CxxTest::TestSuite { - ExprManager *d_exprManager; - - /* Set up declaration context for expr inputs */ - - void setupContext(ParserState* parserState) { - /* a, b, c: BOOLEAN */ - parserState->mkVar("a",d_exprManager->booleanType()); - parserState->mkVar("b",d_exprManager->booleanType()); - parserState->mkVar("c",d_exprManager->booleanType()); - /* t, u, v: TYPE */ - Type t = parserState->mkSort("t"); - Type u = parserState->mkSort("u"); - Type v = parserState->mkSort("v"); - /* f : t->u; g: u->v; h: v->t; */ - parserState->mkVar("f", d_exprManager->mkFunctionType(t,u)); - parserState->mkVar("g", d_exprManager->mkFunctionType(u,v)); - parserState->mkVar("h", d_exprManager->mkFunctionType(v,t)); - /* x:t; y:u; z:v; */ - parserState->mkVar("x",t); - parserState->mkVar("y",u); - parserState->mkVar("z",v); - } - - void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) { - for(int i = 0; i < numInputs; ++i) { - try { -// Debug.on("parser"); -// Debug.on("parser-extra"); - Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n"; -// istringstream stream(goodInputs[i]); - Input* parser = Input::newStringInput(d_exprManager, d_lang, goodInputs[i], "test"); - TS_ASSERT( !parser->done() ); - Command* cmd; - while((cmd = parser->parseNextCommand())) { - // cout << "Parsed command: " << (*cmd) << endl; - } - TS_ASSERT( parser->parseNextCommand() == NULL ); - TS_ASSERT( parser->done() ); - delete parser; -// Debug.off("parser"); -// Debug.off("parser-extra"); - } catch (Exception& e) { - cout << "\nGood input failed:\n" << goodInputs[i] << endl - << e << endl; -// Debug.off("parser-extra"); - throw; - } - } - } - - void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) { - for(int i = 0; i < numInputs; ++i) { -// cout << "Testing bad input: '" << badInputs[i] << "'\n"; -// Debug.on("parser"); - Input* parser = Input::newStringInput(d_exprManager, d_lang, badInputs[i], "test"); - TS_ASSERT_THROWS - ( while(parser->parseNextCommand()); - cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, - ParserException ); -// Debug.off("parser"); - delete parser; - } - } - - void tryGoodExprs(InputLanguage d_lang, const string goodBooleanExprs[], int numExprs) { - // cout << "Using context: " << context << endl; -// Debug.on("parser"); -// Debug.on("parser-extra"); - for(int i = 0; i < numExprs; ++i) { - try { - // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n"; - // Debug.on("parser"); -// istringstream stream(context + goodBooleanExprs[i]); - Input* input = Input::newStringInput(d_exprManager, d_lang, - goodBooleanExprs[i], "test"); - TS_ASSERT( !input->done() ); - setupContext(input->getParserState()); - TS_ASSERT( !input->done() ); - Expr e = input->parseNextExpression(); - TS_ASSERT( !e.isNull() ); - e = input->parseNextExpression(); - TS_ASSERT( input->done() ); - TS_ASSERT( e.isNull() ); - delete input; - } catch (Exception& e) { - cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl; - cout << e; - throw; - } - } - } - - void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) { - //Debug.on("parser"); - for(int i = 0; i < numExprs; ++i) { - // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n"; -// istringstream stream(context + badBooleanExprs[i]); - Input* input = Input::newStringInput(d_exprManager, d_lang, - badBooleanExprs[i], "test"); - - TS_ASSERT( !input->done() ); - setupContext(input->getParserState()); - TS_ASSERT( !input->done() ); - TS_ASSERT_THROWS - ( input->parseNextExpression(); - cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, - ParserException ); - delete input; - } - //Debug.off("parser"); - } - -public: - void setUp() { - d_exprManager = new ExprManager(); - } - - void tearDown() { - delete d_exprManager; - } - - void testBs() { - DeclarationScope declScope; - declScope.bind("foo", d_exprManager->mkVar("foo",d_exprManager->booleanType())); - - } - - void testGoodCvc4Inputs() { - tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); - } - - void testBadCvc4Inputs() { - tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs); - } - - void testGoodCvc4Exprs() { - tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs); - } - - void testBadCvc4Exprs() { - tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs); - } - - void testGoodSmtInputs() { - tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs); - } - - void testBadSmtInputs() { - tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs); - } - - void testGoodSmtExprs() { - tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs); - } - - void testBadSmtExprs() { - tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs); - } -};