1 /********************* -*- C++ -*- */
3 ** This file is part of the CVC4 prototype.
4 ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
5 ** Courant Institute of Mathematical Sciences
7 ** See the file COPYING in the top-level source directory for licensing
10 ** Parser implementation.
17 #include "util/command.h"
18 #include "util/Assert.h"
19 #include "parser_exception.h"
20 #include "parser/antlr_parser.h"
21 #include "parser/smt/generated/AntlrSmtParser.hpp"
22 #include "parser/smt/generated/AntlrSmtLexer.hpp"
23 #include "parser/cvc/generated/AntlrCvcParser.hpp"
24 #include "parser/cvc/generated/AntlrCvcLexer.hpp"
31 Parser::Parser(ExprManager
* em
) :
32 d_expr_manager(em
), d_done(false) {
35 void Parser::setDone(bool done
) {
39 bool Parser::done() const {
43 Command
* SmtParser::parseNextCommand() throw (ParserException
) {
47 cmd
= d_antlr_parser
->benchmark();
49 } catch(antlr::ANTLRException
& e
) {
51 throw ParserException(e
.toString());
57 Expr
SmtParser::parseNextExpression() throw (ParserException
) {
61 result
= d_antlr_parser
->an_formula();
62 } catch(antlr::ANTLRException
& e
) {
64 throw ParserException(e
.toString());
70 SmtParser::~SmtParser() {
71 delete d_antlr_parser
;
75 SmtParser::SmtParser(ExprManager
* em
, istream
& input
) :
77 d_antlr_lexer
= new AntlrSmtLexer(input
);
78 d_antlr_parser
= new AntlrSmtParser(*d_antlr_lexer
);
79 d_antlr_parser
->setExpressionManager(d_expr_manager
);
82 SmtParser::SmtParser(ExprManager
*em
, const char* file_name
) :
83 Parser(em
), d_input(file_name
) {
85 throw ParserException(string("File not found or inaccessible: ") + file_name
);
87 d_antlr_lexer
= new AntlrSmtLexer(d_input
);
88 d_antlr_lexer
->setFilename(file_name
);
89 d_antlr_parser
= new AntlrSmtParser(*d_antlr_lexer
);
90 d_antlr_parser
->setExpressionManager(d_expr_manager
);
91 d_antlr_parser
->setFilename(file_name
);
94 Command
* CvcParser::parseNextCommand() throw (ParserException
) {
98 cmd
= d_antlr_parser
->command();
101 cmd
= new EmptyCommand("EOF");
103 } catch(antlr::ANTLRException
& e
) {
105 throw ParserException(e
.toString());
111 Expr
CvcParser::parseNextExpression() throw (ParserException
) {
115 result
= d_antlr_parser
->formula();
116 } catch(antlr::ANTLRException
& e
) {
118 throw ParserException(e
.toString());
124 CvcParser::~CvcParser() {
125 delete d_antlr_parser
;
126 delete d_antlr_lexer
;
129 CvcParser::CvcParser(ExprManager
* em
, istream
& input
) :
131 d_antlr_lexer
= new AntlrCvcLexer(input
);
132 d_antlr_parser
= new AntlrCvcParser(*d_antlr_lexer
);
133 d_antlr_parser
->setExpressionManager(d_expr_manager
);
136 CvcParser::CvcParser(ExprManager
*em
, const char* file_name
) :
137 Parser(em
), d_input(file_name
) {
139 throw ParserException(string("File not found or inaccessible: ") + file_name
);
141 d_antlr_lexer
= new AntlrCvcLexer(d_input
);
142 d_antlr_lexer
->setFilename(file_name
);
143 d_antlr_parser
= new AntlrCvcParser(*d_antlr_lexer
);
144 d_antlr_parser
->setExpressionManager(d_expr_manager
);
145 d_antlr_parser
->setFilename(file_name
);
149 }/* CVC4::parser namespace */
150 }/* CVC4 namespace */