diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-18 05:07:19 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-18 05:07:19 +0000 |
commit | 2eef69eb63f3a5637f8711944e3d056672872f20 (patch) | |
tree | ab534fd3345dfb307267b991994a54e860d79064 /src/parser/cvc | |
parent | 093492af43fae12d7f1d4607e63b1da686044ea6 (diff) |
Lots of parser changes to make Chris happy. Yet more to come later.
Diffstat (limited to 'src/parser/cvc')
-rw-r--r-- | src/parser/cvc/Makefile.am | 2 | ||||
-rw-r--r-- | src/parser/cvc/Makefile.in | 5 | ||||
-rw-r--r-- | src/parser/cvc/cvc_parser.cpp | 82 | ||||
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 120 | ||||
-rw-r--r-- | src/parser/cvc/cvc_parser.h | 80 |
5 files changed, 99 insertions, 190 deletions
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index 666c408cf..ad0eb70d8 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -24,8 +24,6 @@ ANTLR_STUFF = \ libparsercvc_la_SOURCES = \ cvc_lexer.g \ cvc_parser.g \ - cvc_parser.h \ - cvc_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in index 3fd1701c8..28b80800e 100644 --- a/src/parser/cvc/Makefile.in +++ b/src/parser/cvc/Makefile.in @@ -56,7 +56,7 @@ am__objects_1 = am__objects_2 = AntlrCvcLexer.lo $(am__objects_1) am__objects_3 = AntlrCvcParser.lo am__objects_4 = $(am__objects_2) $(am__objects_3) -am_libparsercvc_la_OBJECTS = cvc_parser.lo $(am__objects_4) +am_libparsercvc_la_OBJECTS = $(am__objects_4) libparsercvc_la_OBJECTS = $(am_libparsercvc_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -249,8 +249,6 @@ ANTLR_STUFF = \ libparsercvc_la_SOURCES = \ cvc_lexer.g \ cvc_parser.g \ - cvc_parser.h \ - cvc_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) @@ -310,7 +308,6 @@ distclean-compile: @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcLexer.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcParser.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cvc_parser.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp deleted file mode 100644 index 57d5e6c96..000000000 --- a/src/parser/cvc/cvc_parser.cpp +++ /dev/null @@ -1,82 +0,0 @@ -/********************* -*- C++ -*- */ -/** cvc_parser.cpp - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 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. - ** - ** CVC presentation language parser implementation. - **/ - -#include <iostream> -#include <fstream> - -#include "parser/parser.h" -#include "util/command.h" -#include "util/Assert.h" -#include "parser/parser_exception.h" -#include "parser/antlr_parser.h" -#include "parser/cvc/cvc_parser.h" -#include "parser/cvc/generated/AntlrCvcParser.hpp" -#include "parser/cvc/generated/AntlrCvcLexer.hpp" - -using namespace std; - -namespace CVC4 { -namespace parser { - -Command* CvcParser::parseNextCommand() throw(ParserException) { - Command* cmd = 0; - if(!done()) { - try { - cmd = d_antlr_parser->command(); - if(cmd == 0) { - setDone(); - cmd = new EmptyCommand("EOF"); - } - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return cmd; -} - -Expr CvcParser::parseNextExpression() throw(ParserException) { - Expr result; - if(!done()) { - try { - result = d_antlr_parser->formula(); - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return result; -} - -CvcParser::~CvcParser() { - delete d_antlr_parser; - delete d_antlr_lexer; -} - -CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) : - Parser(em), d_input(input) { - if(!d_input) { - throw ParserException(string("Read error") + - ((file_name != NULL) ? (string(" on ") + file_name) : "")); - } - d_antlr_lexer = new AntlrCvcLexer(d_input); - d_antlr_lexer->setFilename(file_name); - d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer); - d_antlr_parser->setExpressionManager(d_expr_manager); - d_antlr_parser->setFilename(file_name); -} - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 864719cfa..c7f932a0c 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -29,6 +29,23 @@ options { } /** + * Parses the next command. + * @return command or 0 if EOF + */ +parseCommand returns [CVC4::Command* cmd] + : cmd = command + ; + +/** + * Parses the next expression. + * @return the parsed expression (null expression if EOF) + */ +parseExpr returns [CVC4::Expr expr] + : expr = formula + | EOF + ; + +/** * Matches a command of the input. If a declaration, it will return an empty * command. */ @@ -41,64 +58,118 @@ command returns [CVC4::Command* cmd = 0] | QUERY f = formula { cmd = new QueryCommand(f); } | CHECKSAT f = formula { cmd = new CheckSatCommand(f); } | CHECKSAT { cmd = new CheckSatCommand(); } - | identifierList[ids] COLON type { + | identifierList[ids, CHECK_UNDECLARED] COLON type { // [chris 12/15/2009] FIXME: decls may not be BOOLEAN newPredicates(ids); - cmd = new EmptyCommand("Declaration"); + cmd = new DeclarationCommand(ids); } | EOF ; -identifierList[std::vector<std::string>& id_list] - : id1:IDENTIFIER { id_list.push_back(id1->getText()); } - ( - COMMA - id2:IDENTIFIER { id_list.push_back(id2->getText()); } - )* +/** + * Mathches a list of identifiers separated by a comma and puts them in the + * given list. + * @param idList the list to fill with identifiers. + * @param check what kinds of check to perform on the symbols + */ +identifierList[std::vector<std::string>& idList, DeclarationCheck check = CHECK_NONE] +{ + string id; +} + : id = identifier { idList.push_back(id); } + (COMMA id = identifier { idList.push_back(id); })* ; + +/** + * Matches an identifier and returns a string. + */ +identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id] + : x:IDENTIFIER { checkDeclation(x->getText(), check) }? + { + id = x->getText(); + } + 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"); + default: throw ex; + } + } + ; + +/** + * Matches a type. + * TODO: parse more types + */ type : BOOLEAN ; +/** + * Matches a CVC4 formula. + * @return the expression representing the formula + */ formula returns [CVC4::Expr formula] - : formula = bool_formula + : formula = boolFormula ; -bool_formula returns [CVC4::Expr formula] +/** + * Matches a CVC4 basic Boolean formula (AND, OR, NOT...). It parses the list of + * operands (primaryBoolFormulas) and operators (Kinds) and then calls the + * createPrecedenceExpr method to build the expression using the precedence + * and associativity of the operators. + * @return the expression representing the formula + */ +boolFormula returns [CVC4::Expr formula] { vector<Expr> formulas; vector<Kind> kinds; Expr f1, f2; Kind k; } - : f1 = primary_bool_formula { formulas.push_back(f1); } - ( k = bool_operator { kinds.push_back(k); } f2 = primary_bool_formula { formulas.push_back(f2); } )* + : f1 = primaryBoolFormula { formulas.push_back(f1); } + ( k = boolOperator { kinds.push_back(k); } f2 = primaryBoolFormula { formulas.push_back(f2); } )* { // Create the expression based on precedences formula = createPrecedenceExpr(formulas, kinds); } ; -primary_bool_formula returns [CVC4::Expr formula] - : formula = bool_atom - | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); } - | LPAREN formula = bool_formula RPAREN +/** + * Parses a primary Boolean formula. A primary Boolean formula is either a + * Boolean atom (variables and predicates) a negation of a primary Boolean + * formula or a formula enclosed in parenthesis. + * @return the expression representing the formula + */ +primaryBoolFormula returns [CVC4::Expr formula] + : formula = boolAtom + | NOT formula = primaryBoolFormula { formula = mkExpr(CVC4::NOT, formula); } + | LPAREN formula = boolFormula RPAREN ; -bool_operator returns [CVC4::Kind kind] +/** + * Parses the Boolean operators and returns the corresponding CVC4 expression + * kind. + * @param the kind of the Boolean operator + */ +boolOperator returns [CVC4::Kind kind] : IMPLIES { kind = CVC4::IMPLIES; } | AND { kind = CVC4::AND; } | OR { kind = CVC4::OR; } | XOR { kind = CVC4::XOR; } | IFF { kind = CVC4::IFF; } ; - -bool_atom returns [CVC4::Expr atom] + +/** + * Parses the Boolean atoms (variables and predicates). + * @return the expression representing the atom. + */ +boolAtom returns [CVC4::Expr atom] { string p; } - : p = predicate_sym {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); } + : p = predicateSymbol[CHECK_DECLARED] { atom = getVariable(p); } exception catch [antlr::SemanticException ex] { rethrow(ex, "Undeclared variable " + p); } @@ -106,7 +177,12 @@ bool_atom returns [CVC4::Expr atom] | FALSE { atom = getFalseExpr(); } ; -predicate_sym returns [std::string p] - : id:IDENTIFIER { p = id->getText(); } +/** + * Parses a predicate symbol (an identifier). + * @param what kind of check to perform on the id + * @return the predicate symol + */ +predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol] + : pSymbol = identifier[check] ;
\ No newline at end of file diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h deleted file mode 100644 index 82d659566..000000000 --- a/src/parser/cvc/cvc_parser.h +++ /dev/null @@ -1,80 +0,0 @@ -/********************* -*- C++ -*- */ -/** cvc_parser.h - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 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. - ** - ** CVC presentation language parser abstraction. - **/ - -#ifndef __CVC4__PARSER__CVC_PARSER_H -#define __CVC4__PARSER__CVC_PARSER_H - -#include <string> -#include <iostream> -#include <fstream> -#include "cvc4_config.h" -#include "parser/parser_exception.h" -#include "parser/parser.h" - -namespace CVC4 { -namespace parser { - -/** - * The CVC parser. - */ -class CVC4_PUBLIC CvcParser : public Parser { - -public: - - /** - * Construct the parser that uses the given expression manager and parses - * from the given input stream. - * @param em the expression manager to use - * @param input the input stream to parse - * @param file_name the name of the file (for diagnostic output) - */ - CvcParser(ExprManager* em, std::istream& input, const char* file_name = ""); - - /** - * Destructor. - */ - ~CvcParser(); - - /** - * Parses the next command. By default, the CVC parser produces one - * CommandSequence command. If parsing is successful, we should be - * done after the first call to this command. - * @return the CommandSequence command that includes the whole - * benchmark - */ - Command* parseNextCommand() throw(ParserException); - - /** - * Parses the next complete expression of the stream. - * @return the expression parsed - */ - Expr parseNextExpression() throw(ParserException); - -protected: - - /** The ANTLR smt lexer */ - AntlrCvcLexer* d_antlr_lexer; - - /** The ANTLR smt parser */ - AntlrCvcParser* d_antlr_parser; - - /** The file stream we might be using */ - std::istream& d_input; -}; - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__CVC_PARSER_H */ |