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/smt | |
parent | 093492af43fae12d7f1d4607e63b1da686044ea6 (diff) |
Lots of parser changes to make Chris happy. Yet more to come later.
Diffstat (limited to 'src/parser/smt')
-rw-r--r-- | src/parser/smt/Makefile.am | 2 | ||||
-rw-r--r-- | src/parser/smt/Makefile.in | 5 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.cpp | 79 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.g | 185 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.h | 79 |
5 files changed, 115 insertions, 235 deletions
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 6f5f1bfd4..96ad9c27f 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -24,8 +24,6 @@ ANTLR_STUFF = \ libparsersmt_la_SOURCES = \ smt_lexer.g \ smt_parser.g \ - smt_parser.h \ - smt_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in index 721ff0e2b..6145b4c4e 100644 --- a/src/parser/smt/Makefile.in +++ b/src/parser/smt/Makefile.in @@ -56,7 +56,7 @@ am__objects_1 = am__objects_2 = AntlrSmtLexer.lo $(am__objects_1) am__objects_3 = AntlrSmtParser.lo am__objects_4 = $(am__objects_2) $(am__objects_3) -am_libparsersmt_la_OBJECTS = smt_parser.lo $(am__objects_4) +am_libparsersmt_la_OBJECTS = $(am__objects_4) libparsersmt_la_OBJECTS = $(am_libparsersmt_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -249,8 +249,6 @@ ANTLR_STUFF = \ libparsersmt_la_SOURCES = \ smt_lexer.g \ smt_parser.g \ - smt_parser.h \ - smt_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) @@ -310,7 +308,6 @@ distclean-compile: @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtLexer.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtParser.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/smt_parser.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp deleted file mode 100644 index 8c5773e32..000000000 --- a/src/parser/smt/smt_parser.cpp +++ /dev/null @@ -1,79 +0,0 @@ -/********************* -*- C++ -*- */ -/** smt_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. - ** - ** SMT-LIB 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/smt/smt_parser.h" -#include "parser/smt/generated/AntlrSmtParser.hpp" -#include "parser/smt/generated/AntlrSmtLexer.hpp" - -using namespace std; - -namespace CVC4 { -namespace parser { - -Command* SmtParser::parseNextCommand() throw(ParserException) { - Command* cmd = 0; - if(!done()) { - try { - cmd = d_antlr_parser->benchmark(); - setDone(); - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return cmd; -} - -Expr SmtParser::parseNextExpression() throw(ParserException) { - Expr result; - if(!done()) { - try { - result = d_antlr_parser->an_formula(); - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return result; -} - -SmtParser::~SmtParser() { - delete d_antlr_parser; - delete d_antlr_lexer; -} - -SmtParser::SmtParser(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 AntlrSmtLexer(input); - d_antlr_lexer->setFilename(file_name); - d_antlr_parser = new AntlrSmtParser(*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/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 6e0051821..f7045fa7e 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -27,6 +27,108 @@ options { defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions k = 2; } + +/** + * Parses an expression. + * @return the parsed expression + */ +parseExpr returns [CVC4::Expr expr] + : expr = annotatedFormula + ; + +/** + * Parses a command (the whole benchmark) + * @return the command of the benchmark + */ +parseCommand returns [CVC4::Command* cmd] + : cmd = benchmark + ; + +/** + * Matches the whole SMT-LIB benchmark. + * @return the sequence command containing the whole problem + */ +benchmark returns [Command* cmd] + : LPAREN BENCHMARK IDENTIFIER cmd = benchAttributes RPAREN + | EOF { cmd = 0; } + ; + +/** + * Matchecs sequence of benchmark attributes and returns a pointer to a command + * sequence command. + * @return the command sequence + */ +benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()] +{ + Command* cmd; +} + : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+ + ; + +/** + * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns + * a corresponding command + * @retrurn a command corresponding to the attribute + */ +benchAttribute returns [ Command* smt_command = 0] +{ + Expr formula; + string logic; + SetBenchmarkStatusCommand::BenchmarkStatus b_status = SetBenchmarkStatusCommand::SMT_UNKNOWN; +} + : C_LOGIC logic = identifier { smt_command = new SetBenchmarkLogicCommand(logic); } + | C_ASSUMPTION formula = annotatedFormula { smt_command = new AssertCommand(formula); } + | C_FORMULA formula = annotatedFormula { smt_command = new CheckSatCommand(formula); } + | C_STATUS b_status = status { smt_command = new SetBenchmarkStatusCommand(b_status); } + | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN + | C_NOTES STRING_LITERAL + | annotation + ; + +/** + * Matches an identifier and returns a string. + * @param check what kinds of check to do on the symbol + * @return the id 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 an annotated formula. + * @return the expression representing the formula + */ +annotatedFormula returns [CVC4::Expr formula] +{ + Kind kind; + vector<Expr> children; +} + : formula = annotatedAtom + | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children); } + ; + +/** + * Matches an annotated proposition atom, which is either a propositional atom + * or built of other atoms using a predicate symbol. + */ +annotatedAtom returns [CVC4::Expr atom] + : atom = propositionalAtom + ; + + + + + /** * Matches an attribute name from the input (:attribute_name). @@ -34,7 +136,7 @@ options { attribute : C_IDENTIFIER ; - + /** * Matches the sort symbol, which can be an arbitrary identifier. */ @@ -60,7 +162,7 @@ pred_symb returns [std::string p] /** * Matches a propositional atom. */ -prop_atom returns [CVC4::Expr atom] +propositionalAtom returns [CVC4::Expr atom] { std::string p; } @@ -71,22 +173,11 @@ prop_atom returns [CVC4::Expr atom] | TRUE { atom = getTrueExpr(); } | FALSE { atom = getFalseExpr(); } ; - -/** - * Matches an annotated proposition atom, which is either a propositional atom - * or built of other atoms using a predicate symbol. Annotation can be added if - * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined - * here in order to get rid of the ugly antlr non-determinism warnings. - */ - // [chris 12/15/2009] FIXME: Where is the annotation? -an_atom returns [CVC4::Expr atom] - : atom = prop_atom - ; - + /** * Matches on of the unary Boolean connectives. */ -bool_connective returns [CVC4::Kind kind] +boolConnective returns [CVC4::Kind kind] : NOT { kind = CVC4::NOT; } | IMPLIES { kind = CVC4::IMPLIES; } | AND { kind = CVC4::AND; } @@ -94,24 +185,12 @@ bool_connective returns [CVC4::Kind kind] | XOR { kind = CVC4::XOR; } | IFF { kind = CVC4::IFF; } ; - -/** - * Matches an annotated formula. - */ -an_formula returns [CVC4::Expr formula] -{ - Kind kind; - vector<Expr> children; -} - : formula = an_atom - | LPAREN kind = bool_connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } - ; - -an_formulas[std::vector<Expr>& formulas] + +annotatedFormulas[std::vector<Expr>& formulas] { Expr f; } - : ( f = an_formula { formulas.push_back(f); } )+ + : ( f = annotatedFormula { formulas.push_back(f); } )+ ; /** @@ -138,44 +217,8 @@ sort_symbs[std::vector<std::string>& sorts] /** * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. */ -status returns [ AntlrParser::BenchmarkStatus status ] - : SAT { status = SMT_SATISFIABLE; } - | UNSAT { status = SMT_UNSATISFIABLE; } - | UNKNOWN { status = SMT_UNKNOWN; } - ; - -/** - * Matches a benchmark attribute, sucha as ':logic', ':formula', etc. - */ -bench_attribute returns [ Command* smt_command = 0] -{ - BenchmarkStatus b_status = SMT_UNKNOWN; - Expr formula; - vector<string> sorts; -} - : C_LOGIC IDENTIFIER - | C_ASSUMPTION formula = an_formula { smt_command = new AssertCommand(formula); } - | C_FORMULA formula = an_formula { smt_command = new CheckSatCommand(formula); } - | C_STATUS b_status = status { setBenchmarkStatus(b_status); } - | C_EXTRASORTS LPAREN sort_symbs[sorts] RPAREN { addExtraSorts(sorts); } - | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN - | C_NOTES STRING_LITERAL - | annotation - ; - -/** - * Returns a pointer to a command sequence command. - */ -bench_attributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()] -{ - Command* cmd; -} - : (cmd = bench_attribute { if (cmd) cmd_seq->addCommand(cmd); } )+ - ; - -/** - * Matches the whole SMT-LIB benchmark. - */ -benchmark returns [Command* cmd] - : LPAREN BENCHMARK IDENTIFIER cmd = bench_attributes RPAREN - ; +status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ] + : SAT { status = SetBenchmarkStatusCommand::SMT_SATISFIABLE; } + | UNSAT { status = SetBenchmarkStatusCommand::SMT_UNSATISFIABLE; } + | UNKNOWN { status = SetBenchmarkStatusCommand::SMT_UNKNOWN; } + ;
\ No newline at end of file diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h deleted file mode 100644 index 21c278a37..000000000 --- a/src/parser/smt/smt_parser.h +++ /dev/null @@ -1,79 +0,0 @@ -/********************* -*- C++ -*- */ -/** smt_parser.h - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): cconway, 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. - ** - ** SMT-LIB language parser abstraction. - **/ - -#ifndef __CVC4__PARSER__SMT_PARSER_H -#define __CVC4__PARSER__SMT_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 SMT parser. - */ -class CVC4_PUBLIC SmtParser : public Parser { - -public: - - /** - * Construct the parser that uses the given expression manager and 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) - */ - SmtParser(ExprManager* em, std::istream& input, const char* file_name = ""); - - /** - * Destructor. - */ - ~SmtParser(); - - /** - * Parses the next command. By default, the SMT-LIB 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 */ - AntlrSmtLexer* d_antlr_lexer; - - /** The ANTLR smt parser */ - AntlrSmtParser* d_antlr_parser; - - /** The file stream we might be using */ - std::istream& d_input; -}; - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__SMT_PARSER_H */ |