#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"
// if(inputFromStdin) {
// parser = Parser::getNewParser(&exprMgr, options.lang, cin, "<stdin>");
// } 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);
}
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
+++ /dev/null
-/********************* */
-/** 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 <limits.h>
-#include <antlr3.h>
-
-#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 */
+++ /dev/null
-/********************* */
-/** 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 <vector>
-#include <string>
-#include <iostream>
-#include <antlr3.h>
-
-#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
- * <code>K</code> for an LL(k) grammar. */
- unsigned int d_lookahead;
-
- /** The ANTLR3 lexer associated with this input. This will be <code>NULL</code> initially. It
- * must be set by a call to <code>setLexer</code>, preferably in the subclass constructor. */
- pANTLR3_LEXER d_lexer;
-
- /** The ANTLR3 parser associated with this input. This will be <code>NULL</code> initially. It
- * must be set by a call to <code>setParser</code>, preferably in the subclass constructor.
- * The <code>super</code> field of <code>d_parser</code> will be set to <code>this</code> and
- * <code>reportError</code> will be set to <code>AntlrInput::reportError</code>. */
- 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 <code>setLexer</code>.
- * NOTE: We assume that we <em>can</em> 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 <em>can</em> free it on exit. No sharing! */
- pANTLR3_INPUT_STREAM d_input;
-
- /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
- static void reportError(pANTLR3_BASE_RECOGNIZER recognizer);
-
- /** Builds a message for a lexer error and calls <code>parseError</code>. */
- 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 <code>true</code> 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 <code>ParserException</code> 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
- * <code>setLexer()</code>. */
- 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 */
+++ /dev/null
-/*
- * 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 <antlr3.h>
-#include <sstream>
-
-#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
@parser::includes {
#include "expr/command.h"
-#include "parser/parser_state.h"
+#include "parser/parser.h"
namespace CVC4 {
class Expr;
#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 <vector>
/* 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
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); }
@init {
std::vector<std::string> 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
/** Match the right-hand side of a declaration. Returns the type. */
declType[CVC4::Type& t, std::vector<std::string>& 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
@init {
Type t2;
std::vector<Type> 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]
CVC4::parser::DeclarationCheck check,
CVC4::parser::SymbolType type]
: IDENTIFIER
- { id = AntlrInput::tokenText($IDENTIFIER);
+ { id = Input::tokenText($IDENTIFIER);
PARSER_STATE->checkDeclaration(id, check, type); }
;
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]
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); }
*/
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]
;
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
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]
orFormula[CVC4::Expr& f]
@init {
std::vector<Expr> 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); }
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]
andFormula[CVC4::Expr& f]
@init {
std::vector<Expr> 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); }
*/
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]
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]
@init {
std::string name;
std::vector<Expr> 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
iteTerm[CVC4::Expr& f]
@init {
std::vector<Expr> 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); }
iteElseTerm[CVC4::Expr& f]
@init {
std::vector<Expr> 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); }
*/
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]
#include <antlr3.h>
#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"
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);
throw ParserException("Failed to create CVC lexer.");
}
- setLexer( d_pCvcLexer->pLexer );
+ setAntlr3Lexer( d_pCvcLexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
AlwaysAssert( tokenStream != NULL );
throw ParserException("Failed to create CVC parser.");
}
- setParser(d_pCvcParser->pParser);
+ setAntlr3Parser(d_pCvcParser->pParser);
}
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);
}
#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"
namespace parser {
-class CvcInput : public AntlrInput {
+class CvcInput : public Input {
/** The ANTLR3 CVC lexer for the input. */
pCvcLexer d_pCvcLexer;
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 <code>true</code> 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.
*
* @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();
*
* @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 <code>Expr</code>
* 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:
/********************* */
/** 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)
** 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 <stdint.h>
+#include <limits.h>
+#include <antlr3.h>
#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:
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 */
/** 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
** 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 <antlr3.h>
+#include <iostream>
#include <string>
+#include <vector>
#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 <code>true</code> 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 <code>parseNextCommand</code> and <code>parseNextExpression</code> to
- * extract a stream of <code>Command</code>'s and <code>Expr</code>'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., <code>newFileParser</code> and <code>newStringInput</code>, and
- * should be deleted when done.
+ * An input to be parsed. The static factory methods in this class (e.g.,
+ * <code>newFileInput</code>, <code>newStringInput</code>) 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
+ * <code>K</code> for an LL(k) grammar. */
+ unsigned int d_lookahead;
-public:
+ /** The ANTLR3 lexer associated with this input. This will be <code>NULL</code> initially. It
+ * must be set by a call to <code>setLexer</code>, 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 <code>NULL</code> initially. It
+ * must be set by a call to <code>setParser</code>, preferably in the subclass constructor.
+ * The <code>super</code> field of <code>d_parser</code> will be set to <code>this</code> and
+ * <code>reportError</code> will be set to <code>Input::reportError</code>. */
+ 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 <code>setLexer</code>.
+ * NOTE: We assume that we <em>can</em> 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 <em>can</em> free it on exit. No sharing! */
+ AntlrInputStream *d_inputStream;
+
+ /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
+ static void reportError(pANTLR3_BASE_RECOGNIZER recognizer);
+
+ /** Builds a message for a lexer error and calls <code>parseError</code>. */
+ 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
+ * <code>setLexer()</code>. */
+ pANTLR3_COMMON_TOKEN_STREAM getTokenStream();
- /** Called by <code>parseNextCommand</code> to actually parse a command from
+ /** Parse a command from
* the input by invoking the implementation-specific parsing method. Returns
* <code>NULL</code> 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 <code>ParserException</code> with the given message.
+ */
+ void parseError(const std::string& msg) throw (ParserException);
- /** Called by <code>parseNextExpression</code> to actually parse an
+ /** Parse an
* expression from the input by invoking the implementation-specific
* parsing method. Returns a null <code>Expr</code> 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 <code>ParserException</code> with the given error message.
- * Implementations should fill in the <code>ParserException</code> 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 */
--- /dev/null
+/*
+ * 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 <antlr3.h>
+#include <sstream>
+
+#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
--- /dev/null
+/********************* */
+/** 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 <iostream>
+#include <fstream>
+#include <stdint.h>
+
+#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<Expr>
+Parser::mkVars(const std::vector<std::string> names,
+ const Type& type) {
+ std::vector<Expr> 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<Type>
+Parser::mkSorts(const std::vector<std::string>& names) {
+ std::vector<Type> 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 */
--- /dev/null
+/********************* */
+/** 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 <string>
+
+#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 <code>ExprManager</code>. */
+ 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 <em>only</me> 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 <code>kind</code> can accept <code>numArgs</code> 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 <code>kind</code> cannot be
+ * applied to <code>numArgs</code> 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<Expr>
+ mkVars(const std::vector<std::string> 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<Type>
+ mkSorts(const std::vector<std::string>& 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 */
+++ /dev/null
-/********************* */
-/** 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 <iostream>
-#include <fstream>
-#include <stdint.h>
-
-#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<Expr>
-ParserState::mkVars(const std::vector<std::string> names,
- const Type& type) {
- std::vector<Expr> 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<Type>
-ParserState::mkSorts(const std::vector<std::string>& names) {
- std::vector<Type> 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 */
+++ /dev/null
-/********************* */
-/** 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 <string>
-
-#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 <code>ExprManager</code>. */
- 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 <em>only</me> 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 <code>kind</code> can accept <code>numArgs</code> 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 <code>kind</code> cannot be
- * applied to <code>numArgs</code> 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<Expr>
- mkVars(const std::vector<std::string> 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<Type>
- mkSorts(const std::vector<std::string>& 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 */
@parser::includes {
#include "expr/command.h"
-#include "parser/parser_state.h"
+#include "parser/parser.h"
namespace CVC4 {
class Expr;
#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"
/* 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
/**
* 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"){
*/
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<Expr> args; /* = getExprVector(); */
| 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 */
*/
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; }
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;
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); }
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); }
#include <antlr3.h>
+#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"
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);
throw ParserException("Failed to create SMT lexer.");
}
- setLexer( d_pSmtLexer->pLexer );
+ setAntlr3Lexer( d_pSmtLexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
AlwaysAssert( tokenStream != NULL );
throw ParserException("Failed to create SMT parser.");
}
- setParser(d_pSmtParser->pParser);
+ setAntlr3Parser(d_pSmtParser->pParser);
}
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);
}
#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"
namespace parser {
-class SmtInput : public AntlrInput {
+class SmtInput : public Input {
/** The ANTLR3 SMT lexer for the input. */
pSmtLexer d_pSmtLexer;
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 <code>true</code> 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.
* @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();
*
* @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
*
* @throws ParserException if an error is encountered during parsing.
*/
- Expr doParseExpr() throw(ParserException);
+ Expr parseExpr() throw(ParserException);
private:
+++ /dev/null
-/********************* */
-/** 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 <string>
-#include <stack>
-
-#include <ext/hash_map>
-
-#include "util/Assert.h"
-
-namespace CVC4 {
-namespace parser {
-
-struct StringHashFunction {
- size_t operator()(const std::string& str) const {
- return __gnu_cxx::hash<const char*>()(str.c_str());
- }
-};
-
-/**
- * Generic symbol table for looking up variables by name.
- */
-template <class ObjectType>
-class SymbolTable {
-
-private:
-
- /** The name to expression bindings */
- typedef __gnu_cxx::hash_map<std::string, ObjectType, StringHashFunction>
- 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 */
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 \
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)
--- /dev/null
+/********************* */
+/** 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 <cxxtest/TestSuite.h>
+//#include <string>
+#include <sstream>
+
+#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);
+ }
+};
+++ /dev/null
-/********************* */
-/** 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 <cxxtest/TestSuite.h>
-//#include <string>
-#include <sstream>
-
-#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);
- }
-};
projects / cvc5.git / commitdiff