diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_input.cpp | 9 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 9 | ||||
-rw-r--r-- | src/parser/bounded_token_buffer.cpp | 2 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 6 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.cpp | 6 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.h | 6 | ||||
-rw-r--r-- | src/parser/input.h | 6 | ||||
-rw-r--r-- | src/parser/memory_mapped_input_buffer.cpp | 17 | ||||
-rw-r--r-- | src/parser/parser.cpp | 16 | ||||
-rw-r--r-- | src/parser/smt1/Smt1.g | 107 | ||||
-rw-r--r-- | src/parser/smt1/smt1_input.cpp | 6 | ||||
-rw-r--r-- | src/parser/smt1/smt1_input.h | 6 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 6 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 6 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.h | 8 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 6 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 2 | ||||
-rw-r--r-- | src/parser/tptp/tptp_input.cpp | 6 | ||||
-rw-r--r-- | src/parser/tptp/tptp_input.h | 6 |
19 files changed, 138 insertions, 98 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 8987a7572..fbf2b8650 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -63,8 +63,13 @@ AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) throw (InputStreamException) { +#ifdef _WIN32 + if(useMmap) { + useMmap = false; + } +#endif pANTLR3_INPUT_STREAM input = NULL; - if( useMmap ) { + if(useMmap) { input = MemoryMappedInputBufferNew(name); } else { // libantlr3c v3.2 isn't source-compatible with v3.4 @@ -74,7 +79,7 @@ AntlrInputStream::newFileInputStream(const std::string& name, input = antlr3FileStreamNew((pANTLR3_UINT8) name.c_str(), ANTLR3_ENC_8BIT); #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */ } - if( input == NULL ) { + if(input == NULL) { throw InputStreamException("Couldn't open file: " + name); } return new AntlrInputStream( name, input ); diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 68a62274d..a2fe99f52 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -285,7 +285,14 @@ inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) { inline BitVector AntlrInput::tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size) { std::string number_str = tokenTextSubstr(number, 2); - return BitVector(tokenToUnsigned(size), Integer(number_str)); + unsigned sz = tokenToUnsigned(size); + Integer val(number_str); + if(val.modByPow2(sz) != val) { + std::stringstream ss; + ss << "Overflow in bitvector construction (specified bitvector size " << sz << " too small to hold value " << tokenText(number) << ")"; + throw std::invalid_argument(ss.str()); + } + return BitVector(sz, val); } }/* CVC4::parser namespace */ diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index 904f9a7fa..6a6ae8609 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -512,7 +512,7 @@ static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) { } -/// Return a string that represents the name assoicated with the input source +/// Return a string that represents the name associated with the input source /// /// /param[in] is The ANTLR3_INT_STREAM interface that is representing this token stream. /// diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 1af4799be..b8ec160e8 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -416,10 +416,8 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { @header { /** - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information. **/ diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 52fadae66..8328306be 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -56,13 +56,11 @@ CvcInput::~CvcInput() { d_pCvcParser->free(d_pCvcParser); } -Command* CvcInput::parseCommand() - throw (ParserException, TypeCheckingException) { +Command* CvcInput::parseCommand() { return d_pCvcParser->parseCommand(d_pCvcParser); } -Expr CvcInput::parseExpr() - throw (ParserException, TypeCheckingException) { +Expr CvcInput::parseExpr() { return d_pCvcParser->parseExpr(d_pCvcParser); } diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 398ac4bd0..973e1c173 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -63,16 +63,14 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() - throw(ParserException, TypeCheckingException); + Command* parseCommand(); /** Parse an expression from the input. Returns a null <code>Expr</code> * if there is no expression there to parse. * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() - throw(ParserException, TypeCheckingException); + Expr parseExpr(); private: diff --git a/src/parser/input.h b/src/parser/input.h index 0203ed806..f4b36469b 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -168,8 +168,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - virtual Command* parseCommand() - throw (ParserException, TypeCheckingException) = 0; + virtual Command* parseCommand() = 0; /** * Issue a warning to the user, with source file, line, and column info. @@ -188,8 +187,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - virtual Expr parseExpr() - throw (ParserException, TypeCheckingException) = 0; + virtual Expr parseExpr() = 0; /** Set the Parser object for this input. */ virtual void setParser(Parser& parser) = 0; diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index 9f72ac51c..f110b1145 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -18,10 +18,15 @@ #include <stdio.h> #include <stdint.h> +#include <antlr3input.h> + +#ifndef _WIN32 + #include <cerrno> #include <sys/mman.h> #include <sys/stat.h> -#include <antlr3input.h> + +#endif /* _WIN32 */ #include "parser/memory_mapped_input_buffer.h" #include "util/exception.h" @@ -31,6 +36,14 @@ namespace parser { extern "C" { +#ifdef _WIN32 + +pANTLR3_INPUT_STREAM MemoryMappedInputBufferNew(const std::string& filename) { + return 0; +} + +#else /* ! _WIN32 */ + static ANTLR3_UINT32 MemoryMapFile(pANTLR3_INPUT_STREAM input, const std::string& filename); @@ -112,6 +125,8 @@ void UnmapFile(pANTLR3_INPUT_STREAM input) { input->close(input); } +#endif /* _WIN32 */ + }/* extern "C" */ }/* CVC4::parser namespace */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 65d46220b..8b77362b2 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -462,15 +462,9 @@ Command* Parser::nextCommand() throw(ParserException) { } catch(ParserException& e) { setDone(); throw; - } catch(Exception& e) { + } catch(exception& e) { setDone(); - stringstream ss; - // set the language of the stream, otherwise if it contains - // Exprs or Types it prints in the AST language - OutputLanguage outlang = - language::toOutputLanguage(d_input->getLanguage()); - ss << Expr::setlanguage(outlang) << e; - parseError( ss.str() ); + parseError(e.what()); } } } @@ -490,11 +484,9 @@ Expr Parser::nextExpression() throw(ParserException) { } catch(ParserException& e) { setDone(); throw; - } catch(Exception& e) { + } catch(exception& e) { setDone(); - stringstream ss; - ss << e; - parseError( ss.str() ); + parseError(e.what()); } } Debug("parser") << "nextExpression() => " << result << std::endl; diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index 6dade9530..f8331c899 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -31,10 +31,8 @@ options { @header { /** - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information. **/ @@ -235,10 +233,10 @@ annotatedFormula[CVC4::Expr& expr] Expr op; /* Operator expression FIXME: move away kill it */ } : /* a built-in operator application */ - LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK + LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { /* Unary AND/OR can be replaced with the argument. - It just so happens expr should already by the only argument. */ + * It just so happens expr should already be the only argument. */ assert( expr == args[0] ); } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { @@ -253,6 +251,7 @@ annotatedFormula[CVC4::Expr& expr] expr = MK_EXPR(kind, args); } } + termAnnotation[expr]* RPAREN_TOK | /* A quantifier */ LPAREN_TOK @@ -261,12 +260,13 @@ annotatedFormula[CVC4::Expr& expr] ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK { args.push_back(PARSER_STATE->mkBoundVar(name, t)); } )+ - annotatedFormula[expr] RPAREN_TOK + annotatedFormula[expr] { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) ); args2.push_back(expr); expr = MK_EXPR(kind, args2); - PARSER_STATE->popScope(); } + termAnnotation[expr]* RPAREN_TOK + { PARSER_STATE->popScope(); } | /* A non-built-in function application */ @@ -275,9 +275,10 @@ annotatedFormula[CVC4::Expr& expr] // { isFunction(LT(2)->getText()) }? LPAREN_TOK parameterizedOperator[op] - annotatedFormulas[args,expr] RPAREN_TOK + annotatedFormulas[args,expr] // TODO: check arity { expr = MK_EXPR(op,args); } + termAnnotation[expr]* RPAREN_TOK | /* An ite expression */ LPAREN_TOK ITE_TOK @@ -286,9 +287,9 @@ annotatedFormula[CVC4::Expr& expr] annotatedFormula[expr] { args.push_back(expr); } annotatedFormula[expr] - { args.push_back(expr); } - RPAREN_TOK - { expr = MK_EXPR(CVC4::kind::ITE, args); } + { args.push_back(expr); + expr = MK_EXPR(CVC4::kind::ITE, args); } + termAnnotation[expr]* RPAREN_TOK | /* a let/flet binding */ LPAREN_TOK @@ -298,7 +299,7 @@ annotatedFormula[CVC4::Expr& expr] { PARSER_STATE->pushScope(); PARSER_STATE->defineVar(name,expr); } annotatedFormula[expr] - RPAREN_TOK + termAnnotation[expr]* RPAREN_TOK { PARSER_STATE->popScope(); } /* constants */ @@ -310,7 +311,7 @@ annotatedFormula[CVC4::Expr& expr] { // FIXME: This doesn't work because an SMT rational is not a // valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } - | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']' + | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']' { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); } // NOTE: Theory constants go here /* TODO: quantifiers, arithmetic constants */ @@ -320,7 +321,6 @@ annotatedFormula[CVC4::Expr& expr] | let_identifier[name,CHECK_DECLARED] | flet_identifier[name,CHECK_DECLARED] ) { expr = PARSER_STATE->getVariable(name); } - ; /** @@ -458,7 +458,7 @@ functionSymbol[CVC4::Expr& fun] * Matches an attribute name from the input (:attribute_name). */ attribute[std::string& s] - : ATTR_IDENTIFIER + : ATTR_IDENTIFIER { s = AntlrInput::tokenText($ATTR_IDENTIFIER); } ; @@ -555,28 +555,56 @@ status[ CVC4::BenchmarkStatus& status ] /** * Matches an annotation, which is an attribute name, with an optional user + * value. */ annotation[CVC4::Command*& smt_command] @init { - std::string key; + std::string key, value; smt_command = NULL; + std::vector<Expr> pats; + Expr pat; } - : attribute[key] - ( USER_VALUE - { std::string value = AntlrInput::tokenText($USER_VALUE); - assert(*value.begin() == '{'); - assert(*value.rbegin() == '}'); - // trim whitespace - value.erase(value.begin(), value.begin() + 1); - value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace)))); - value.erase(value.end() - 1); - value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), value.end()); - smt_command = new SetInfoCommand(key.c_str() + 1, value); } - )? - { if(smt_command == NULL) { - smt_command = new EmptyCommand(std::string("annotation: ") + key); + : PATTERN_ANNOTATION_BEGIN + { PARSER_STATE->warning(":pat not supported here; ignored"); } + annotatedFormulas[pats,pat] '}' + | attribute[key] + ( userValue[value] + { smt_command = new SetInfoCommand(key.c_str() + 1, value); } + | { smt_command = new EmptyCommand(std::string("annotation: ") + key); } + ) + ; + +/** + * Matches an annotation, which is an attribute name, with an optional user + * value. + */ +termAnnotation[CVC4::Expr& expr] +@init { + std::string key, value; + std::vector<Expr> pats; + Expr pat; +} + : PATTERN_ANNOTATION_BEGIN annotatedFormulas[pats,pat] '}' + { if(expr.getKind() == kind::FORALL || expr.getKind() == kind::EXISTS) { + pat = MK_EXPR(kind::INST_PATTERN, pats); + if(expr.getNumChildren() == 3) { + // we have other user patterns attached to the quantifier + // already; add this one to the existing list + pats = expr[2].getChildren(); + pats.push_back(pat); + expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pats)); + } else { + // this is the only user pattern for the quantifier + expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pat)); + } + } else { + PARSER_STATE->warning(":pat only supported on quantifiers"); } } + | ':pat' + { PARSER_STATE->warning("expected an instantiation pattern after :pat"); } + | attribute[key] userValue[value]? + { PARSER_STATE->attributeNotSupported(key); } ; /** @@ -752,6 +780,23 @@ FLET_IDENTIFIER * only constraint imposed on a user-defined value is that it start * with an open brace and end with closed brace. */ +userValue[std::string& s] + : USER_VALUE + { s = AntlrInput::tokenText($USER_VALUE); + assert(*s.begin() == '{'); + assert(*s.rbegin() == '}'); + // trim whitespace + s.erase(s.begin(), s.begin() + 1); + s.erase(s.begin(), std::find_if(s.begin(), s.end(), std::not1(std::ptr_fun<int, int>(std::isspace)))); + s.erase(s.end() - 1); + s.erase(std::find_if(s.rbegin(), s.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), s.end()); + } + ; + +PATTERN_ANNOTATION_BEGIN + : ':pat' (' ' | '\t' | '\f' | '\r' | '\n')* '{' + ; + USER_VALUE : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}' ; diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp index 156ca083f..2dae4ef66 100644 --- a/src/parser/smt1/smt1_input.cpp +++ b/src/parser/smt1/smt1_input.cpp @@ -57,13 +57,11 @@ Smt1Input::~Smt1Input() { d_pSmt1Parser->free(d_pSmt1Parser); } -Command* Smt1Input::parseCommand() - throw (ParserException, TypeCheckingException) { +Command* Smt1Input::parseCommand() { return d_pSmt1Parser->parseCommand(d_pSmt1Parser); } -Expr Smt1Input::parseExpr() - throw (ParserException, TypeCheckingException) { +Expr Smt1Input::parseExpr() { return d_pSmt1Parser->parseExpr(d_pSmt1Parser); } diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h index ce5c8284c..11110e78a 100644 --- a/src/parser/smt1/smt1_input.h +++ b/src/parser/smt1/smt1_input.h @@ -66,8 +66,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() - throw(ParserException, TypeCheckingException); + Command* parseCommand(); /** * Parse an expression from the input. Returns a null @@ -75,8 +74,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() - throw(ParserException, TypeCheckingException); + Expr parseExpr(); private: diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 648666091..1ee288aa4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -31,10 +31,8 @@ options { @header { /** - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information. **/ diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 2ed8d6966..9b423dcad 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -58,13 +58,11 @@ Smt2Input::~Smt2Input() { d_pSmt2Parser->free(d_pSmt2Parser); } -Command* Smt2Input::parseCommand() - throw (ParserException, TypeCheckingException) { +Command* Smt2Input::parseCommand() { return d_pSmt2Parser->parseCommand(d_pSmt2Parser); } -Expr Smt2Input::parseExpr() - throw (ParserException, TypeCheckingException) { +Expr Smt2Input::parseExpr() { return d_pSmt2Parser->parseExpr(d_pSmt2Parser); } diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 62ed33632..9b271a2c0 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -41,7 +41,7 @@ class Smt2Input : public AntlrInput { /** The ANTLR3 SMT2 lexer for the input. */ pSmt2Lexer d_pSmt2Lexer; - /** The ANTLR3 CVC parser for the input. */ + /** The ANTLR3 SMT2 parser for the input. */ pSmt2Parser d_pSmt2Parser; /** @@ -75,8 +75,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() - throw(ParserException, TypeCheckingException); + Command* parseCommand(); /** * Parse an expression from the input. Returns a null @@ -84,8 +83,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() - throw(ParserException, TypeCheckingException); + Expr parseExpr(); };/* class Smt2Input */ diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 2180255ca..ec6868c5b 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -32,10 +32,8 @@ options { @header { /** - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** This file is part of CVC4. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information. **/ diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 1e40ea63f..59b1d205b 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -151,7 +151,7 @@ void Tptp::includeFile(std::string fileName){ if( d_tptpDir.empty() ){ parseError("Couldn't open included file: " + fileName - + " at " + currentDirFileName + " and the TPTP directory is not specified (environnement variable TPTP)"); + + " at " + currentDirFileName + " and the TPTP directory is not specified (environment variable TPTP)"); }; std::string tptpDirFileName = d_tptpDir + fileName; diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index 40231853f..d52c7f597 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -58,13 +58,11 @@ TptpInput::~TptpInput() { d_pTptpParser->free(d_pTptpParser); } -Command* TptpInput::parseCommand() - throw (ParserException, TypeCheckingException) { +Command* TptpInput::parseCommand() { return d_pTptpParser->parseCommand(d_pTptpParser); } -Expr TptpInput::parseExpr() - throw (ParserException, TypeCheckingException) { +Expr TptpInput::parseExpr() { return d_pTptpParser->parseExpr(d_pTptpParser); } diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h index da9c67e31..13aa358cd 100644 --- a/src/parser/tptp/tptp_input.h +++ b/src/parser/tptp/tptp_input.h @@ -75,8 +75,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() - throw(ParserException, TypeCheckingException); + Command* parseCommand(); /** * Parse an expression from the input. Returns a null @@ -84,8 +83,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() - throw(ParserException, TypeCheckingException); + Expr parseExpr(); };/* class TptpInput */ |