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.h | |
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.h')
-rw-r--r-- | src/parser/parser.h | 70 |
1 files changed, 60 insertions, 10 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index d0ef3776a..dbdca4af8 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -30,6 +30,8 @@ namespace parser { class AntlrSmtLexer; class AntlrSmtParser; +class AntlrCvcLexer; +class AntlrCvcParser; /** * The parser. @@ -49,7 +51,6 @@ public: */ virtual ~Parser() { } - ; /** * Parse the next command of the input @@ -64,13 +65,19 @@ public: /** * Check if we are done -- either the end of input has been reached. */ - virtual bool done() const = 0; + bool done() const; protected: + /** Sets the done flag */ + void setDone(bool done = true); + /** Expression manager the parser will be using */ ExprManager* d_expr_manager; + /** Are we done */ + bool d_done; + }; // end of class Parser class CVC4_PUBLIC SmtParser : public Parser { @@ -112,12 +119,6 @@ public: */ Expr parseNextExpression() throw (ParserException); - /** - * Check if we are done with the stream, i.e. EOF has been reached, or the - * whole SMT benchmark has been parsed. - */ - bool done() const; - protected: /** The ANTLR smt lexer */ @@ -126,13 +127,62 @@ protected: /** The ANTLR smt parser */ AntlrSmtParser* d_antlr_parser; - /** Are we done */ - bool d_done; + /** The file stream we might be using */ + std::ifstream d_input; +}; + +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 + */ + CvcParser(ExprManager* em, std::istream& input); + + /** + * Construct the parser that uses the given expression manager and parses + * from the file. + * @param em the expression manager to use + * @param file_name the file to parse + */ + CvcParser(ExprManager* em, const char* file_name); + + /** + * Destructor. + */ + ~CvcParser(); + + /** + * Parses the next command. By default, the SMTLIB 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::ifstream d_input; }; + }/* CVC4::parser namespace */ }/* CVC4 namespace */ |