diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-16 18:07:41 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-16 18:07:41 +0000 |
commit | 48142c912d7571ee204b373eadf835c5b676af2c (patch) | |
tree | 5caf584809cf5b28882edfbcbc73e86efe7a0ae9 /src/parser | |
parent | 69248e7ee22494ccefe0ce21fe4b834eb60df2e1 (diff) |
Converting semantic predicates in parser to AlwaysAssertions
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_parser.cpp | 4 | ||||
-rw-r--r-- | src/parser/antlr_parser.h | 5 | ||||
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 28 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.g | 39 |
4 files changed, 44 insertions, 32 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index bd263f72d..24d0ac3d7 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -288,9 +288,9 @@ bool AntlrParser::isDeclared(string name, SymbolType type) { } } -void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) +void AntlrParser::parseError(string message) throw (antlr::SemanticException) { - throw antlr::SemanticException(new_message, getFilename(), + throw antlr::SemanticException(message, getFilename(), LT(1).get()->getLine(), LT(1).get()->getColumn()); } diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 76200368c..eec444af9 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -101,10 +101,9 @@ protected: AntlrParser(antlr::TokenStream& lexer, int k); /** - * Renames the antlr semantic expression to a given message. + * Throws an ANTLR semantic exception with the given message. */ - void rethrow(antlr::SemanticException& e, std::string msg) - throw (antlr::SemanticException); + void parseError(std::string msg) throw (antlr::SemanticException); /** * Returns a variable, given a name and a type. diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 794f4706a..926430a5c 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -157,8 +157,8 @@ returns [std::string id] { checkDeclaration(id, check, type) }? exception catch [antlr::SemanticException& ex] { switch (check) { - case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared"); - case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared"); + case CHECK_DECLARED: parseError("Symbol " + id + " not declared"); + case CHECK_UNDECLARED: parseError("Symbol " + id + " already declared"); default: throw ex; } } @@ -322,12 +322,12 @@ term returns [CVC4::Expr t] Debug("parser") << "term: " << LT(1)->getText() << endl; } : /* function application */ - { isFunction(LT(1)->getText()) }? - name = functionSymbol[CHECK_DECLARED] - { - std::vector<CVC4::Expr> args; - args.push_back( getFunction(name) ); - } + // { isFunction(LT(1)->getText()) }? + { Expr f; + std::vector<CVC4::Expr> args; } + f = functionSymbol[CHECK_DECLARED] + { args.push_back( f ); } + LPAREN formulaList[args] RPAREN // TODO: check arity { t = mkExpr(CVC4::APPLY, args); } @@ -382,9 +382,15 @@ iteElseTerm returns [CVC4::Expr t] * @param what kind of check to perform on the id * @return the predicate symol */ -functionSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string symbol] +functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f] { Debug("parser") << "function symbol: " << LT(1)->getText() << endl; - -} : symbol = identifier[check,SYM_FUNCTION] + std::string name; +} + : name = identifier[check,SYM_FUNCTION] + { AlwaysAssert( isFunction(name) ); + f = getFunction(name); } + exception catch [CVC4::AssertionException& ex] { + parseError("Expected function symbol, found: " + name); + } ; diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 4ecac0418..fc38871b0 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -16,6 +16,7 @@ header "post_include_hpp" { #include "parser/antlr_parser.h" #include "expr/command.h" +#include "util/Assert.h" } header "post_include_cpp" { @@ -42,7 +43,7 @@ class AntlrSmtParser extends Parser("AntlrParser"); options { genHashLines = true; // Include line number information importVocab = SmtVocabulary; // Import the common vocabulary - defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions + defaultErrorHandler = false; // Skip the default error handling, just break with exceptions k = 2; } @@ -122,10 +123,10 @@ annotatedFormula returns [CVC4::Expr formula] } : /* a built-in operator application */ LPAREN kind = builtinOp annotatedFormulas[args] RPAREN - { args.size() >= minArity(kind) - && args.size() <= maxArity(kind) }? - { formula = mkExpr(kind,args); } - exception catch [antlr::SemanticException& ex] { + { AlwaysAssert( args.size() >= minArity(kind) + && args.size() <= maxArity(kind) ); + formula = mkExpr(kind,args); } + exception catch [CVC4::AssertionException& ex] { stringstream ss; ss << "Expected "; if( args.size() < minArity(kind) ) { @@ -135,11 +136,15 @@ annotatedFormula returns [CVC4::Expr formula] } ss << "arguments for operator '" << kind << "'. "; ss << "Found: " << args.size(); - rethrow(ex, ss.str()); + parseError(ss.str()); } | /* A non-built-in function application */ - { isFunction(LT(2)->getText()) }? + + // Semantic predicate not necessary if parenthesized subexpressions + // are disallowed + // { isFunction(LT(2)->getText()) }? + { Expr f; } LPAREN f = functionSymbol { args.push_back(f); } @@ -156,9 +161,6 @@ annotatedFormula returns [CVC4::Expr formula] RPAREN { formula = mkExpr(CVC4::ITE, test, trueExpr, falseExpr); } - | /* a parenthesized sub-formula */ - LPAREN formula = annotatedFormula RPAREN - | /* a variable */ { std::string name; } name = identifier[CHECK_DECLARED] @@ -224,7 +226,12 @@ functionSymbol returns [CVC4::Expr fun] string name; } : name = functionName[CHECK_DECLARED] - { fun = getFunction(name); } + { AlwaysAssert( isFunction(name) ); + fun = getFunction(name); } + exception catch [CVC4::AssertionException& ex] { + parseError("Expected function symbol, found: " + name); + } + ; /** @@ -325,12 +332,12 @@ returns [std::string id] << " type? " << toString(type) << endl; } : x:IDENTIFIER - { id = x->getText(); } - { checkDeclaration(id, check,type) }? - exception catch [antlr::SemanticException& ex] { + { id = x->getText(); + AlwaysAssert( checkDeclaration(id, check,type) ); } + exception catch [CVC4::AssertionException& ex] { switch (check) { - case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared"); - case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared"); + case CHECK_DECLARED: parseError("Symbol " + id + " not declared"); + case CHECK_UNDECLARED: parseError("Symbol " + id + " already declared"); default: throw ex; } } |