diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-07 05:51:09 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-07 05:51:09 +0000 |
commit | b3bcafc179201e33c4f41ccf028c12eacc110d69 (patch) | |
tree | 6b35f7e654ac3b2278b9201db331fab980b32cd9 /src/parser/parser.cpp | |
parent | c16be5841e613818d5764e4de99e4694a0703685 (diff) |
antlr parser for the cvc4 language (boolean only)
yet to be finalized, it should work as expected
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 76 |
1 files changed, 67 insertions, 9 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index b9091668e..65a5d11c1 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -20,6 +20,8 @@ #include "parser/antlr_parser.h" #include "parser/smt/AntlrSmtParser.hpp" #include "parser/smt/AntlrSmtLexer.hpp" +#include "parser/cvc/AntlrCvcParser.hpp" +#include "parser/cvc/AntlrCvcLexer.hpp" using namespace std; @@ -27,21 +29,25 @@ namespace CVC4 { namespace parser { Parser::Parser(ExprManager* em) : - d_expr_manager(em) { + d_expr_manager(em), d_done(false) { } -bool SmtParser::done() const { +void Parser::setDone(bool done) { + d_done = done; +} + +bool Parser::done() const { return d_done; } Command* SmtParser::parseNextCommand() throw (ParserException) { Command* cmd = 0; - if(!d_done) { + if(!done()) { try { cmd = d_antlr_parser->benchmark(); - d_done = true; + setDone(); } catch(antlr::ANTLRException& e) { - d_done = true; + setDone(); throw ParserException(e.toString()); } } @@ -50,11 +56,11 @@ Command* SmtParser::parseNextCommand() throw (ParserException) { Expr SmtParser::parseNextExpression() throw (ParserException) { Expr result; - if (!d_done) { + if (!done()) { try { result = d_antlr_parser->an_formula(); } catch(antlr::ANTLRException& e) { - d_done = true; + setDone(); throw ParserException(e.toString()); } } @@ -67,14 +73,14 @@ SmtParser::~SmtParser() { } SmtParser::SmtParser(ExprManager* em, istream& input) : - Parser(em), d_done(false) { + Parser(em) { d_antlr_lexer = new AntlrSmtLexer(input); d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer); d_antlr_parser->setExpressionManager(d_expr_manager); } SmtParser::SmtParser(ExprManager*em, const char* file_name) : - Parser(em), d_done(false), d_input(file_name) { + Parser(em), d_input(file_name) { d_antlr_lexer = new AntlrSmtLexer(d_input); d_antlr_lexer->setFilename(file_name); d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer); @@ -82,6 +88,58 @@ SmtParser::SmtParser(ExprManager*em, const char* file_name) : d_antlr_parser->setFilename(file_name); } +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) : + Parser(em) { + d_antlr_lexer = new AntlrCvcLexer(input); + d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer); + d_antlr_parser->setExpressionManager(d_expr_manager); +} + +CvcParser::CvcParser(ExprManager*em, const char* file_name) : + Parser(em), d_input(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 */ |