diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-03 14:59:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-03 14:59:30 +0000 |
commit | 7fb54afe126e5045fc6c5553c1aff3c3f73509aa (patch) | |
tree | 37f4f23af0eccd6c9615a5af9b2d219e305d1f78 /src/parser/parser.h | |
parent | bde1a14afc211c8f0f0521bb91feb562eaa9f9ea (diff) |
parsing/expr/command/result/various other fixes
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 107 |
1 files changed, 54 insertions, 53 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 765fb0553..411e7760c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -16,83 +16,84 @@ #include <string> #include <iostream> -namespace CVC4 -{ -namespace parser -{ +#include "parser/language.h" +#include "parser/parser_state.h" + +namespace CVC4 { // Forward declarations class Expr; class Command; class ExprManager; -class ParserState; +class SmtEngine; +class Options; + +namespace parser { /** - * The parser. + * The global pointer to ParserTemp. Each instance of class Parser sets this pointer + * before any calls to the lexer. We do it this way because flex and bison use global + * vars, and we want each Parser object to appear independent. */ -class Parser -{ - private: +extern ParserState CVC4_PUBLIC *_global_parser_state; - /** Internal parser state we are keeping */ - ParserState* d_data; +/** + * The parser. + */ +class CVC4_PUBLIC Parser { + private: - /** Initialize the parser */ - void initParser(); + /** Internal parser state we are keeping */ + //ParserState* d_data; - /** Remove the parser components */ - void deleteParser(); + /** Initialize the parser */ + void initParser(); - public: + /** Remove the parser components */ + void deleteParser(); - /** The supported input languages */ - enum InputLanguage { - /** SMT-LIB language */ - INPUT_SMTLIB, - /** CVC language */ - INPUT_CVC - }; + Language d_lang; + std::istream &d_in; + Options *d_opts; - /** - * Constructor for parsing out of a file. - * @param em the expression manager to use - * @param lang the language syntax to use - * @param file_name the file to parse - */ - Parser(ExprManager* em, InputLanguage lang, const std::string& file_name); + public: - /** - * Destructor. - */ - ~Parser(); + /** + * Constructor for parsing out of a file. + * @param em the expression manager to use + * @param lang the language syntax to use + * @param file_name the file to parse + */ + Parser(SmtEngine* smt, ExprManager* em, Language lang, std::istream& in, Options* opts) : + d_lang(lang), d_in(in), d_opts(opts) { + _global_parser_state = new ParserState(smt, em); + _global_parser_state->setInputStream(in); + } - /** Parse a command */ - Command parseNextCommand(); + /** + * Destructor. + */ + ~Parser(); - /** Parse an expression of the stream */ - Expr parseNextExpression(); + /** Parse a command */ + Command* parseNextCommand(bool verbose = false); - // Check if we are done (end of input has been reached) - bool done() const; + /** Parse an expression of the stream */ + Expr parseNextExpression(); - // The same check can be done by using the class Parser's value as a Boolean - operator bool() const { return done(); } + // Check if we are done (end of input has been reached) + bool done() const; - /** Prints the location to the output stream */ - void printLocation(std::ostream& out) const; + // The same check can be done by using the class Parser's value as a Boolean + operator bool() const { return done(); } - /** Reset any local data */ - void reset(); + /** Prints the location to the output stream */ + void printLocation(std::ostream& out) const; + /** Reset any local data */ + void reset(); }; // end of class Parser -/** - * The global pointer to ParserTemp. Each instance of class Parser sets this pointer - * before any calls to the lexer. We do it this way because flex and bison use global - * vars, and we want each Parser object to appear independent. - */ -extern ParserState* _global_parser_state; - }/* CVC4::parser namespace */ }/* CVC4 namespace */ |