diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-06 02:21:46 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-06 02:21:46 +0000 |
commit | c16be5841e613818d5764e4de99e4694a0703685 (patch) | |
tree | 5bf7c07a8f7200c2830d50f5dd83ecbb4f02444d /src/parser/parser.cpp | |
parent | 200f36785acf7aac3e7e230795ea7ffdb6b1ed64 (diff) |
Big chunk of changes:
* Fixed bugs in option parsing
* Simplified the main.cpp significantly (more c++ like)
* Added the null kind, expr value, and expression, with the default constructor public
* Simplified commands, we need to discuss this in the meeting (what to do with command results?)
* Removed all the lex/yacc files
* Symbol table is now a templated class, as we will have tables for variables, predicates and functions
* The ANTLR parsing infrastructure/makefiles is all in. SMT lib Boolean benchmarks should parse + giving nice error such as
Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test4.smt:3:16: Undeclared variable p
Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test2.smt:2:11: unexpected token: sa
Didn't add any unit tests as the unit testing doesn't work with the updated build system -- it doesn't know how to create directories in the corresponding build directory.
TODO:
* add the PL grammar and unit test when the testing becomes available
* with this build setup my eclipse debugger doesn't work. Might have something to do with the visibility of symbols?
* i'm getting g++ depracated warnings regarding the hash_map from the symbol table, need to figure out how to use it in a standard manner. the new <unordered_map> header is for C++0x, and the <ext/hash_map> is getting deprecation warningns... weird.
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 82 |
1 files changed, 54 insertions, 28 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index cd03f21f2..b9091668e 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -11,49 +11,75 @@ **/ #include <iostream> +#include <fstream> -#include "cvc4_config.h" -#include "parser/parser.h" +#include "parser.h" #include "util/command.h" #include "util/assert.h" -#include "parser/parser_state.h" -#include "parser/parser_exception.h" - -int CVC4_PUBLIC smtlibparse(); -int CVC4_PUBLIC PLparse(); -extern "C" int smtlibdebug, PLdebug; +#include "parser_exception.h" +#include "parser/antlr_parser.h" +#include "parser/smt/AntlrSmtParser.hpp" +#include "parser/smt/AntlrSmtLexer.hpp" using namespace std; -using namespace CVC4; namespace CVC4 { namespace parser { -ParserState CVC4_PUBLIC *_global_parser_state = 0; +Parser::Parser(ExprManager* em) : + d_expr_manager(em) { +} -bool Parser::done() const { - return _global_parser_state->done(); +bool SmtParser::done() const { + return d_done; +} + +Command* SmtParser::parseNextCommand() throw (ParserException) { + Command* cmd = 0; + if(!d_done) { + try { + cmd = d_antlr_parser->benchmark(); + d_done = true; + } catch(antlr::ANTLRException& e) { + d_done = true; + throw ParserException(e.toString()); + } + } + return cmd; } -Command* Parser::parseNextCommand(bool verbose) { - switch(d_lang) { - case PL: - PLdebug = verbose; - PLparse(); - cout << "getting command" << endl; - return _global_parser_state->getCommand(); - case SMTLIB: - smtlibdebug = verbose; - smtlibparse(); - return _global_parser_state->getCommand(); - default: - Unhandled(); +Expr SmtParser::parseNextExpression() throw (ParserException) { + Expr result; + if (!d_done) { + try { + result = d_antlr_parser->an_formula(); + } catch(antlr::ANTLRException& e) { + d_done = true; + throw ParserException(e.toString()); + } } - return new EmptyCommand; + return result; +} + +SmtParser::~SmtParser() { + delete d_antlr_parser; + delete d_antlr_lexer; +} + +SmtParser::SmtParser(ExprManager* em, istream& input) : + Parser(em), d_done(false) { + d_antlr_lexer = new AntlrSmtLexer(input); + d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer); + d_antlr_parser->setExpressionManager(d_expr_manager); } -Parser::~Parser() { - //delete d_data; +SmtParser::SmtParser(ExprManager*em, const char* file_name) : + Parser(em), d_done(false), 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); + d_antlr_parser->setExpressionManager(d_expr_manager); + d_antlr_parser->setFilename(file_name); } }/* CVC4::parser namespace */ |