diff options
Diffstat (limited to 'src/parser')
27 files changed, 166 insertions, 153 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index ea593e7da..0dc833ee5 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -36,7 +36,6 @@ #include "parser/smt2/smt2_input.h" #include "parser/tptp/tptp_input.h" #include "util/output.h" -#include "util/Assert.h" using namespace std; using namespace CVC4; @@ -51,7 +50,7 @@ AntlrInputStream::AntlrInputStream(std::string name, bool fileIsTemporary) : InputStream(name,fileIsTemporary), d_input(input) { - AlwaysAssert( input != NULL ); + assert( input != NULL ); } AntlrInputStream::~AntlrInputStream() { @@ -65,7 +64,7 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { pANTLR3_INPUT_STREAM input = NULL; if( useMmap ) { input = MemoryMappedInputBufferNew(name); @@ -87,7 +86,7 @@ AntlrInputStream* AntlrInputStream::newStreamInputStream(std::istream& input, const std::string& name, bool lineBuffered) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { pANTLR3_INPUT_STREAM inputStream = NULL; @@ -162,10 +161,10 @@ AntlrInputStream::newStreamInputStream(std::istream& input, AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { char* inputStr = strdup(input.c_str()); char* nameStr = strdup(name.c_str()); - AlwaysAssert( inputStr!=NULL && nameStr!=NULL ); + assert( inputStr!=NULL && nameStr!=NULL ); #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM pANTLR3_INPUT_STREAM inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) inputStr, @@ -207,7 +206,9 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre break; default: - Unhandled(lang); + std::stringstream ss; + ss << "internal error: unhandled language " << lang << " in AntlrInput::newInput"; + throw ParserException(ss.str()); } return input; @@ -261,11 +262,11 @@ pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() { void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super); - AlwaysAssert(lexer!=NULL); + assert(lexer!=NULL); Parser *parser = (Parser*)(lexer->super); - AlwaysAssert(parser!=NULL); + assert(parser!=NULL); AntlrInput *input = (AntlrInput*) parser->getInput(); - AlwaysAssert(input!=NULL); + assert(input!=NULL); /* Call the error display routine *if* there's not already a * parse error pending. If a parser error is pending, this @@ -280,7 +281,7 @@ void AntlrInput::warning(const std::string& message) { } void AntlrInput::parseError(const std::string& message) - throw (ParserException, AssertionException) { + throw (ParserException) { Debug("parser") << "Throwing exception: " << getInputStream()->getName() << ":" << d_lexer->getLine(d_lexer) << "." diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 2d468a7d6..613390ca1 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -27,12 +27,12 @@ #include <stdexcept> #include <string> #include <vector> +#include <cassert> #include "parser/bounded_token_buffer.h" #include "parser/parser_exception.h" #include "parser/input.h" -#include "util/Assert.h" #include "util/bitvector.h" #include "util/integer.h" #include "util/rational.h" @@ -73,13 +73,13 @@ public: */ static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Create an input from an istream. */ static AntlrInputStream* newStreamInputStream(std::istream& input, const std::string& name, bool lineBuffered = false) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Create a string input. * @@ -88,7 +88,7 @@ public: */ static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name) - throw (InputStreamException, AssertionException); + throw (InputStreamException); };/* class AntlrInputStream */ class Parser; @@ -212,7 +212,7 @@ protected: * Throws a <code>ParserException</code> with the given message. */ void parseError(const std::string& msg) - throw (ParserException, AssertionException); + throw (ParserException); /** Set the ANTLR3 lexer for this input. */ void setAntlr3Lexer(pANTLR3_LEXER pLexer); @@ -255,7 +255,7 @@ inline std::string AntlrInput::tokenTextSubstr(pANTLR3_COMMON_TOKEN token, ANTLR3_MARKER start = token->getStartIndex(token); // Its the last character of the token (not the one just after) ANTLR3_MARKER end = token->getStopIndex(token); - Assert( start < end ); + assert( start < end ); if( index > (size_t) end - start ) { std::stringstream ss; ss << "Out-of-bounds substring index: " << index; diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index d714c4975..9c92846bb 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -57,7 +57,6 @@ #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/parser_exception.h" -#include "util/Assert.h" using namespace std; @@ -92,11 +91,11 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { // Dig the CVC4 objects out of the ANTLR3 mess pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); - AlwaysAssert(antlr3Parser!=NULL); + assert(antlr3Parser!=NULL); Parser *parser = (Parser*)(antlr3Parser->super); - AlwaysAssert(parser!=NULL); + assert(parser!=NULL); AntlrInput *input = (AntlrInput*) parser->getInput() ; - AlwaysAssert(input!=NULL); + assert(input!=NULL); // Signal we are in error recovery now recognizer->state->errorRecovery = ANTLR3_TRUE; @@ -235,7 +234,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { } } } else { - Unreachable("Parse error with empty set of expected tokens."); + assert(false);//("Parse error with empty set of expected tokens."); } } break; @@ -257,7 +256,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { // then we are just going to report what we know about the // token. // - Unhandled("Unexpected exception in parser."); + assert(false);//("Unexpected exception in parser."); break; } diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp index b42562f72..0facbddaf 100644 --- a/src/parser/antlr_line_buffered_input.cpp +++ b/src/parser/antlr_line_buffered_input.cpp @@ -20,9 +20,9 @@ #include <antlr3.h> #include <iostream> #include <string> +#include <cassert> #include "util/output.h" -#include "util/Assert.h" namespace CVC4 { namespace parser { @@ -242,7 +242,7 @@ myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) { in.getline((((char*)input->data) + input->sizeBuf), 1024); } input->sizeBuf += strlen(((char*)input->data) + input->sizeBuf); - Assert(*(((char*)input->data) + input->sizeBuf) == '\0'); + assert(*(((char*)input->data) + input->sizeBuf) == '\0'); Debug("pipe") << "SIZEBUF now " << input->sizeBuf << std::endl; *(((char*)input->data) + input->sizeBuf) = '\n'; ++input->sizeBuf; diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index d63d3afe0..7edbf7b7f 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -56,7 +56,7 @@ #include <antlr3tokenstream.h> #include "parser/bounded_token_buffer.h" -#include "util/Assert.h" +#include <cassert> namespace CVC4 { namespace parser { @@ -142,7 +142,7 @@ BoundedTokenBufferSourceNew(ANTLR3_UINT32 k, pANTLR3_TOKEN_SOURCE source) pANTLR3_COMMON_TOKEN_STREAM stream; - AlwaysAssert( k > 0 ); + assert( k > 0 ); /* Memory for the interface structure */ @@ -235,7 +235,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) { buffer = (pBOUNDED_TOKEN_BUFFER) cts->super; /* k must be in the range [-buffer->k..buffer->k] */ - AlwaysAssert( k <= (ANTLR3_INT32)buffer->k + assert( k <= (ANTLR3_INT32)buffer->k && -k <= (ANTLR3_INT32)buffer->k ); if(k == 0) { @@ -244,7 +244,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) { /* Initialize the buffer on our first call. */ if( EXPECT_FALSE(buffer->empty == ANTLR3_TRUE) ) { - AlwaysAssert( buffer->tokenBuffer != NULL ); + assert( buffer->tokenBuffer != NULL ); buffer->tokenBuffer[ 0 ] = nextToken(buffer); buffer->maxIndex = 0; buffer->currentIndex = 0; @@ -257,7 +257,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) { kIndex = buffer->currentIndex + k - 1; } else { /* Can't look behind more tokens than we've consumed. */ - AlwaysAssert( -k <= (ANTLR3_INT32)buffer->currentIndex ); + assert( -k <= (ANTLR3_INT32)buffer->currentIndex ); /* look-behind token k is at offset -k */ kIndex = buffer->currentIndex + k; } @@ -289,7 +289,8 @@ dbgTokLT (pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) static pANTLR3_COMMON_TOKEN get (pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 i) { - Unreachable(); + assert(false);// unimplemented + return NULL; } static pANTLR3_TOKEN_SOURCE @@ -308,19 +309,22 @@ setTokenSource ( pANTLR3_TOKEN_STREAM ts, static pANTLR3_STRING toString (pANTLR3_TOKEN_STREAM ts) { - Unimplemented("toString(ts)"); + assert(false);// unimplemented + return NULL; } static pANTLR3_STRING toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop) { - Unimplemented("toStringSS(ts, %u, %u)", start, stop); + assert(false);// unimplemented + return NULL; } static pANTLR3_STRING toStringTT (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop) { - Unimplemented("toStringTT(ts, %u, %u)", start, stop); + assert(false);// unimplemented + return NULL; } /** Move the input pointer to the next incoming token. The stream @@ -379,7 +383,8 @@ _LA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i) static ANTLR3_UINT32 dbgLA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i) { - Unreachable(); + assert(false); + return 0; } static ANTLR3_MARKER @@ -394,7 +399,8 @@ mark (pANTLR3_INT_STREAM is) static ANTLR3_MARKER dbgMark (pANTLR3_INT_STREAM is) { - Unreachable(); + assert(false); + return 0; } static void @@ -406,7 +412,8 @@ release (pANTLR3_INT_STREAM is, ANTLR3_MARKER mark) static ANTLR3_UINT32 size (pANTLR3_INT_STREAM is) { - Unreachable(); + assert(false); + return 0; } static ANTLR3_MARKER @@ -426,12 +433,12 @@ tindex (pANTLR3_INT_STREAM is) static void dbgRewindLast (pANTLR3_INT_STREAM is) { - Unreachable(); + assert(false); } static void rewindLast (pANTLR3_INT_STREAM is) { - Unreachable(); + assert(false); } static void rewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) @@ -441,7 +448,7 @@ rewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) static void dbgRewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) { - Unreachable(); + assert(false); } static void @@ -458,7 +465,7 @@ seek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index) static void dbgSeek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index) { - Unreachable(); + assert(false); } static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) { diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 4577b504c..b496aa91c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -288,7 +288,9 @@ int getOperatorPrecedence(int type) { case IN_TOK: return 33; default: - Unhandled(CvcParserTokenNames[type]); + std::stringstream ss; + ss << "internal error: no entry in precedence table for operator " << CvcParserTokenNames[type]; + throw ParserException(ss.str()); } }/* getOperatorPrecedence() */ @@ -318,16 +320,18 @@ Kind getOperatorKind(int type, bool& negate) { case INTDIV_TOK: return kind::INTS_DIVISION; case MOD_TOK: return kind::INTS_MODULUS; case DIV_TOK: return kind::DIVISION; - case EXP_TOK: Unhandled(CvcParserTokenNames[type]); + case EXP_TOK: break; // bvBinop case CONCAT_TOK: return kind::BITVECTOR_CONCAT; case BAR: return kind::BITVECTOR_OR; case BVAND_TOK: return kind::BITVECTOR_AND; - - default: - Unhandled(CvcParserTokenNames[type]); } + + std::stringstream ss; + ss << "internal error: no entry in operator-kind table for operator " << CvcParserTokenNames[type]; + throw ParserException(ss.str()); + }/* getOperatorKind() */ unsigned findPivot(const std::vector<unsigned>& operators, @@ -355,10 +359,10 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em, const std::vector<CVC4::Expr>& expressions, const std::vector<unsigned>& operators, unsigned startIndex, unsigned stopIndex) { - Assert(expressions.size() == operators.size() + 1); - Assert(startIndex < expressions.size()); - Assert(stopIndex < expressions.size()); - Assert(startIndex <= stopIndex); + assert(expressions.size() == operators.size() + 1); + assert(startIndex < expressions.size()); + assert(stopIndex < expressions.size()); + assert(startIndex <= stopIndex); if(stopIndex == startIndex) { return expressions[startIndex]; @@ -450,6 +454,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { @parser::includes { #include <stdint.h> +#include <cassert> #include "expr/command.h" #include "parser/parser.h" #include "util/subrange_bound.h" @@ -1016,7 +1021,7 @@ type[CVC4::Type& t, /* a type, possibly a function */ : restrictedTypePossiblyFunctionLHS[t,check,lhs] { if(lhs) { - Assert(t.isTuple()); + assert(t.isTuple()); args = TupleType(t).getTypes(); } else { args.push_back(t); @@ -1430,7 +1435,7 @@ arrayStore[CVC4::Expr& f] } : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+ ASSIGN_TOK uminusTerm[f3] - { Assert(dims.size() >= 1); + { assert(dims.size() >= 1); // these loops are a bit complicated; they're only used for the // multidimensional ...WITH [a][b] :=... syntax for(unsigned i = 0; i < dims.size() - 1; ++i) { @@ -1630,7 +1635,7 @@ postfixTerm[CVC4::Expr& f] } else if(t.isTester()) { f = MK_EXPR(CVC4::kind::APPLY_TESTER, args); } else { - Unhandled(t); + PARSER_STATE->parseError("internal error: unhandled function application kind"); } } @@ -1864,18 +1869,18 @@ simpleTerm[CVC4::Expr& f] | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } /* bitvector literals */ | HEX_LITERAL - { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); + { assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4); f = MK_CONST( BitVector(hexString, 16) ); } | BINARY_LITERAL - { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); + { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); f = MK_CONST( BitVector(binString, 2) ); } /* record literals */ | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); } ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN { std::vector< std::pair<std::string, Type> > typeIds; - Assert(names.size() == args.size()); + assert(names.size() == args.size()); for(unsigned i = 0; i < names.size(); ++i) { typeIds.push_back(std::make_pair(names[i], args[i].getType())); } diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index d91a13bee..26ee4a693 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -32,7 +32,7 @@ namespace parser { CvcInput::CvcInput(AntlrInputStream& inputStream) : AntlrInput(inputStream,6) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); + assert( input != NULL ); d_pCvcLexer = CvcLexerNew(input); if( d_pCvcLexer == NULL ) { @@ -42,7 +42,7 @@ CvcInput::CvcInput(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pCvcLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); + assert( tokenStream != NULL ); d_pCvcParser = CvcParserNew(tokenStream); if( d_pCvcParser == NULL ) { @@ -59,12 +59,12 @@ CvcInput::~CvcInput() { } Command* CvcInput::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pCvcParser->parseCommand(d_pCvcParser); } Expr CvcInput::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pCvcParser->parseExpr(d_pCvcParser); } diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 9a1f24fde..94e1bfc60 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -66,7 +66,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); /** Parse an expression from the input. Returns a null <code>Expr</code> * if there is no expression there to parse. @@ -74,7 +74,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); private: diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 76aa47812..12c674a61 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -24,7 +24,6 @@ #include "expr/type.h" #include "parser/antlr_input.h" #include "util/output.h" -#include "util/Assert.h" using namespace std; using namespace CVC4; @@ -57,7 +56,7 @@ InputStream *Input::getInputStream() { Input* Input::newFileInput(InputLanguage lang, const std::string& filename, bool useMmap) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename, useMmap); return AntlrInput::newInput(lang, *inputStream); @@ -67,7 +66,7 @@ Input* Input::newStreamInput(InputLanguage lang, std::istream& input, const std::string& name, bool lineBuffered) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { AntlrInputStream *inputStream = AntlrInputStream::newStreamInputStream(input, name, lineBuffered); return AntlrInput::newInput(lang, *inputStream); @@ -76,7 +75,7 @@ Input* Input::newStreamInput(InputLanguage lang, Input* Input::newStringInput(InputLanguage lang, const std::string& str, const std::string& name) - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str, name); return AntlrInput::newInput(lang, *inputStream); } diff --git a/src/parser/input.h b/src/parser/input.h index d47ca4d12..6f30724d1 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -29,7 +29,6 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "parser/parser_exception.h" -#include "util/Assert.h" #include "util/language.h" namespace CVC4 { @@ -111,7 +110,7 @@ public: static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap = false) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Create an input for the given stream. * @@ -126,7 +125,7 @@ public: std::istream& input, const std::string& name, bool lineBuffered = false) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Create an input for the given string * @@ -137,7 +136,7 @@ public: static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Destructor. Frees the input stream and closes the input. */ @@ -172,7 +171,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ virtual Command* parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) = 0; + throw (ParserException, TypeCheckingException) = 0; /** * Issue a warning to the user, with source file, line, and column info. @@ -183,7 +182,7 @@ protected: * Throws a <code>ParserException</code> with the given message. */ virtual void parseError(const std::string& msg) - throw (ParserException, AssertionException) = 0; + throw (ParserException) = 0; /** Parse an expression from the input by invoking the * implementation-specific parsing method. Returns a null @@ -192,7 +191,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ virtual Expr parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) = 0; + throw (ParserException, TypeCheckingException) = 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 f0b7a9d2c..8f8f07099 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -26,7 +26,6 @@ #include <antlr3input.h> #include "parser/memory_mapped_input_buffer.h" -#include "util/Assert.h" #include "util/exception.h" namespace CVC4 { diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 2a64d122d..7b58ba4f9 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -20,6 +20,7 @@ #include <fstream> #include <iterator> #include <stdint.h> +#include <cassert> #include "parser/input.h" #include "parser/parser.h" @@ -30,7 +31,6 @@ #include "expr/type.h" #include "util/output.h" #include "options/options.h" -#include "util/Assert.h" using namespace std; using namespace CVC4::kind; @@ -53,16 +53,15 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par Expr Parser::getSymbol(const std::string& name, SymbolType type) { checkDeclaration(name, CHECK_DECLARED, type); - Assert( isDeclared(name, type) ); + assert( isDeclared(name, type) ); - switch( type ) { - - case SYM_VARIABLE: // Functions share var namespace + if(type == SYM_VARIABLE) { + // Functions share var namespace return d_symtab->lookup(name); - - default: - Unhandled(type); } + + assert(false);//Unhandled(type); + return Expr(); } @@ -77,14 +76,14 @@ Expr Parser::getFunction(const std::string& name) { Type Parser::getType(const std::string& var_name, SymbolType type) { checkDeclaration(var_name, CHECK_DECLARED, type); - Assert( isDeclared(var_name, type) ); + assert( isDeclared(var_name, type) ); Type t = getSymbol(var_name, type).getType(); return t; } Type Parser::getSort(const std::string& name) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); - Assert( isDeclared(name, SYM_SORT) ); + assert( isDeclared(name, SYM_SORT) ); Type t = d_symtab->lookupType(name); return t; } @@ -92,14 +91,14 @@ Type Parser::getSort(const std::string& name) { Type Parser::getSort(const std::string& name, const std::vector<Type>& params) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); - Assert( isDeclared(name, SYM_SORT) ); + assert( isDeclared(name, SYM_SORT) ); Type t = d_symtab->lookupType(name, params); return t; } size_t Parser::getArity(const std::string& sort_name){ checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT); - Assert( isDeclared(sort_name, SYM_SORT) ); + assert( isDeclared(sort_name, SYM_SORT) ); return d_symtab->lookupArity(sort_name); } @@ -187,20 +186,20 @@ Parser::defineVar(const std::string& name, const Expr& val, bool levelZero) { Debug("parser") << "defineVar( " << name << " := " << val << " , " << levelZero << ")" << std::endl;; d_symtab->bind(name, val, levelZero); - Assert( isDeclared(name) ); + assert( isDeclared(name) ); } void Parser::defineFunction(const std::string& name, const Expr& val, bool levelZero) { d_symtab->bindDefinedFunction(name, val, levelZero); - Assert( isDeclared(name) ); + assert( isDeclared(name) ); } void Parser::defineType(const std::string& name, const Type& type) { d_symtab->bindType(name, type); - Assert( isDeclared(name, SYM_SORT) ); + assert( isDeclared(name, SYM_SORT) ); } void @@ -208,7 +207,7 @@ Parser::defineType(const std::string& name, const std::vector<Type>& params, const Type& type) { d_symtab->bindType(name, params, type); - Assert( isDeclared(name, SYM_SORT) ); + assert( isDeclared(name, SYM_SORT) ); } void @@ -283,7 +282,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { std::vector<DatatypeType> types = d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); - Assert(datatypes.size() == types.size()); + assert(datatypes.size() == types.size()); for(unsigned i = 0; i < datatypes.size(); ++i) { DatatypeType t = types[i]; @@ -379,9 +378,9 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) { return d_symtab->isBound(name); case SYM_SORT: return d_symtab->isBoundType(name); - default: - Unhandled(type); } + assert(false);//Unhandled(type); + return false; } void Parser::checkDeclaration(const std::string& varName, @@ -411,7 +410,7 @@ void Parser::checkDeclaration(const std::string& varName, break; default: - Unhandled(check); + assert(false);//Unhandled(check); } } diff --git a/src/parser/parser.h b/src/parser/parser.h index 7efc4d78c..deeff5a62 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -24,6 +24,7 @@ #include <string> #include <set> #include <list> +#include <cassert> #include "parser/input.h" #include "parser/parser_exception.h" diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 73c31f578..f48d1e309 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -61,29 +61,27 @@ void ParserBuilder::init(ExprManager* exprManager, } Parser* ParserBuilder::build() - throw (InputStreamException, AssertionException) { + throw (InputStreamException) { Input* input = NULL; switch( d_inputType ) { case FILE_INPUT: input = Input::newFileInput(d_lang, d_filename, d_mmap); break; case LINE_BUFFERED_STREAM_INPUT: - AlwaysAssert( d_streamInput != NULL, - "Uninitialized stream input in ParserBuilder::build()" ); + assert( d_streamInput != NULL ); input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true); break; case STREAM_INPUT: - AlwaysAssert( d_streamInput != NULL, - "Uninitialized stream input in ParserBuilder::build()" ); + assert( d_streamInput != NULL ); input = Input::newStreamInput(d_lang, *d_streamInput, d_filename); break; case STRING_INPUT: input = Input::newStringInput(d_lang, d_stringInput, d_filename); break; - default: - Unreachable(); } + assert(input != NULL); + Parser* parser = NULL; switch(d_lang) { case language::input::LANG_SMTLIB_V1: diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 095769ab5..4952f310d 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -91,7 +91,7 @@ public: const Options& options); /** Build the parser, using the current settings. */ - Parser *build() throw (InputStreamException, AssertionException); + Parser *build() throw (InputStreamException); /** Should semantic checks be enabled in the parser? (Default: yes) */ ParserBuilder& withChecks(bool flag = true); diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index b228fb9ec..e093037eb 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -241,7 +241,7 @@ annotatedFormula[CVC4::Expr& 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. */ - Assert( expr == args[0] ); + assert( expr == args[0] ); } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ @@ -474,7 +474,7 @@ functionDeclaration[CVC4::Command*& smt_command] { sorts.push_back(t); } sortList[sorts] RPAREN_TOK { if( sorts.size() == 1 ) { - Assert( t == sorts[0] ); + assert( t == sorts[0] ); } else { t = EXPR_MANAGER->mkFunctionType(sorts); } @@ -566,8 +566,8 @@ annotation[CVC4::Command*& smt_command] : attribute[key] ( USER_VALUE { std::string value = AntlrInput::tokenText($USER_VALUE); - Assert(*value.begin() == '{'); - Assert(*value.rbegin() == '}'); + 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)))); diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index c91743226..9074cc20a 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -117,9 +117,10 @@ void Smt1::addTheory(Theory theory) { } case THEORY_BITVECTOR_ARRAYS_EX: { - Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)"); - //addOperator(kind::SELECT); - //addOperator(kind::STORE); + // We don't define the "Array" symbol in this case; + // the parser creates the Array[m:n] types on the fly. + addOperator(kind::SELECT); + addOperator(kind::STORE); break; } @@ -134,7 +135,6 @@ void Smt1::addTheory(Theory theory) { case THEORY_INT_ARRAYS: case THEORY_INT_ARRAYS_EX: { defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType())); - addOperator(kind::SELECT); addOperator(kind::STORE); break; @@ -167,7 +167,9 @@ void Smt1::addTheory(Theory theory) { break; default: - Unhandled(theory); + std::stringstream ss; + ss << "internal error: unsupported theory " << theory; + throw ParserException(ss.str()); } } @@ -229,8 +231,8 @@ void Smt1::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; - case QF_ABV: - addTheory(THEORY_ARRAYS_EX); + case QF_ABV:// nonstandard logic + addTheory(THEORY_BITVECTOR_ARRAYS_EX); addTheory(THEORY_BITVECTORS); break; @@ -241,18 +243,18 @@ void Smt1::setLogic(const std::string& name) { case QF_AUFBV: addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTOR_ARRAYS_EX); addTheory(THEORY_BITVECTORS); break; - case QF_AUFBVLIA: + case QF_AUFBVLIA:// nonstandard logic addOperator(kind::APPLY_UF); addTheory(THEORY_ARRAYS_EX); addTheory(THEORY_BITVECTORS); addTheory(THEORY_INTS); break; - case QF_AUFBVLRA: + case QF_AUFBVLRA:// nonstandard logic addOperator(kind::APPLY_UF); addTheory(THEORY_ARRAYS_EX); addTheory(THEORY_BITVECTORS); @@ -260,22 +262,22 @@ void Smt1::setLogic(const std::string& name) { break; case QF_AUFLIA: - addTheory(THEORY_INT_ARRAYS_EX); + addTheory(THEORY_INT_ARRAYS_EX);// nonstandard logic addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); break; - case QF_AUFLIRA: + case QF_AUFLIRA:// nonstandard logic addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); addTheory(THEORY_REALS); break; - case ALL_SUPPORTED: + case ALL_SUPPORTED:// nonstandard logic addTheory(THEORY_QUANTIFIERS); /* fall through */ - case QF_ALL_SUPPORTED: + case QF_ALL_SUPPORTED:// nonstandard logic addTheory(THEORY_ARRAYS_EX); addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp index 4987cd793..aae990311 100644 --- a/src/parser/smt1/smt1_input.cpp +++ b/src/parser/smt1/smt1_input.cpp @@ -33,7 +33,7 @@ namespace parser { Smt1Input::Smt1Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); + assert( input != NULL ); d_pSmt1Lexer = Smt1LexerNew(input); if( d_pSmt1Lexer == NULL ) { @@ -43,7 +43,7 @@ Smt1Input::Smt1Input(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pSmt1Lexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); + assert( tokenStream != NULL ); d_pSmt1Parser = Smt1ParserNew(tokenStream); if( d_pSmt1Parser == NULL ) { @@ -60,12 +60,12 @@ Smt1Input::~Smt1Input() { } Command* Smt1Input::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pSmt1Parser->parseCommand(d_pSmt1Parser); } Expr Smt1Input::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pSmt1Parser->parseExpr(d_pSmt1Parser); } diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h index 77d6f4b50..0f8a962ba 100644 --- a/src/parser/smt1/smt1_input.h +++ b/src/parser/smt1/smt1_input.h @@ -69,7 +69,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); /** * Parse an expression from the input. Returns a null @@ -78,7 +78,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); private: diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index fb97d5d1e..1b778f87a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -587,7 +587,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] args.size() == 1) { /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ - Assert( expr == args[0] ); + assert( expr == args[0] ); } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ @@ -778,12 +778,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } | HEX_LITERAL - { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); + { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); expr = MK_CONST( BitVector(hexString, 16) ); } | BINARY_LITERAL - { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); + { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); expr = MK_CONST( BitVector(binString, 2) ); } @@ -1055,7 +1055,9 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] } t = EXPR_MANAGER->mkBitVectorType(numerals.front()); } else { - Unhandled(name); + std::stringstream ss; + ss << "unknown indexed symbol `" << name << "'"; + PARSER_STATE->parseError(ss.str()); } } | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ca7697810..45caf94a8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -88,7 +88,9 @@ void Smt2::addTheory(Theory theory) { break; default: - Unhandled(theory); + std::stringstream ss; + ss << "internal error: unsupported theory " << theory; + throw ParserException(ss.str()); } } diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 8f43b0acf..dd90598bb 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -34,7 +34,7 @@ namespace parser { Smt2Input::Smt2Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); + assert( input != NULL ); d_pSmt2Lexer = Smt2LexerNew(input); if( d_pSmt2Lexer == NULL ) { @@ -44,7 +44,7 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pSmt2Lexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); + assert( tokenStream != NULL ); d_pSmt2Parser = Smt2ParserNew(tokenStream); if( d_pSmt2Parser == NULL ) { @@ -61,12 +61,12 @@ Smt2Input::~Smt2Input() { } Command* Smt2Input::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pSmt2Parser->parseCommand(d_pSmt2Parser); } Expr Smt2Input::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pSmt2Parser->parseExpr(d_pSmt2Parser); } diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 05a62c30d..2e36b218e 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -78,7 +78,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); /** * Parse an expression from the input. Returns a null @@ -87,7 +87,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); };/* class Smt2Input */ diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 134498eea..7df2b0210 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -83,7 +83,9 @@ void Tptp::addTheory(Theory theory) { break; default: - Unhandled(theory); + std::stringstream ss; + ss << "internal error: Tptp::addTheory(): unhandled theory " << theory; + throw ParserException(ss.str()); } } diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 9d75a1d37..6d35cac61 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -24,6 +24,7 @@ #include "parser/parser.h" #include "expr/command.h" #include <ext/hash_set> +#include <cassert> namespace CVC4 { @@ -52,9 +53,9 @@ class Tptp : public Parser { public: bool cnf; //in a cnf formula - void addFreeVar(Expr var){Assert(cnf); d_freeVar.push_back(var); }; + void addFreeVar(Expr var){assert(cnf); d_freeVar.push_back(var); }; std::vector< Expr > getFreeVar(){ - Assert(cnf); + assert(cnf); std::vector< Expr > r; r.swap(d_freeVar); return r; @@ -212,22 +213,19 @@ inline Command* Tptp::makeCommand(FormulaRole fr, Expr & expr){ case FR_PLAIN: // it's a usual assert return new AssertCommand(expr); - break; case FR_CONJECTURE: // something to prove return new AssertCommand(getExprManager()->mkExpr(kind::NOT,expr)); - break; case FR_UNKNOWN: case FR_FI_DOMAIN: case FR_FI_FUNCTORS: case FR_FI_PREDICATES: case FR_TYPE: return new EmptyCommand("Untreated role"); - break; - default: - Unreachable("fr",fr); - }; -}; + } + assert(false);// unreachable + return NULL; +} namespace tptp { /** diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index 689f13a8b..8d41a5b68 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -34,7 +34,7 @@ namespace parser { TptpInput::TptpInput(AntlrInputStream& inputStream) : AntlrInput(inputStream, 1) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); + assert( input != NULL ); d_pTptpLexer = TptpLexerNew(input); if( d_pTptpLexer == NULL ) { @@ -44,7 +44,7 @@ TptpInput::TptpInput(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pTptpLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); + assert( tokenStream != NULL ); d_pTptpParser = TptpParserNew(tokenStream); if( d_pTptpParser == NULL ) { @@ -61,12 +61,12 @@ TptpInput::~TptpInput() { } Command* TptpInput::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pTptpParser->parseCommand(d_pTptpParser); } Expr TptpInput::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pTptpParser->parseExpr(d_pTptpParser); } diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h index 7977117d0..32d3efad1 100644 --- a/src/parser/tptp/tptp_input.h +++ b/src/parser/tptp/tptp_input.h @@ -78,7 +78,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); /** * Parse an expression from the input. Returns a null @@ -87,7 +87,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); };/* class TptpInput */ |