diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-25 00:42:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-25 00:42:52 +0000 |
commit | 2a1ac62e56d43893c59c4c2d91bcaca0dd7ce417 (patch) | |
tree | 5d2e6b493d8d366ab75163effaf13191dbf0bd71 /src/parser/parser.h | |
parent | 06b391f721c8e9de4835e5a5bf2c60383ea7f8e9 (diff) |
additional work on parser hookup, configuration + build
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 66 |
1 files changed, 32 insertions, 34 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 73565b8c4..8103238b3 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -13,47 +13,45 @@ #ifndef __CVC4__PARSER__PARSER_H #define __CVC4__PARSER__PARSER_H +#include <iostream> + #include "util/exception.h" #include "parser/language.h" +#include "parser/parser_state.h" #include "util/command.h" +#include "util/options.h" +#include "expr/expr.h" +#include "smt/smt_engine.h" +#include "util/assert.h" namespace CVC4 { namespace parser { - class Expr; - - // Internal parser state and other data - class ParserData; - - class Parser { - private: - ParserData* d_data; - // Internal methods for constructing and destroying the actual parser - void initParser(); - void deleteParser(); - public: - // Constructors - Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, Options* opts, bool interactive = false); - // Destructor - ~Parser(); - // Read the next command. - CVC4::Command* next(); - // Check if we are done (end of input has been reached) - bool done() const; - // The same check can be done by using the class Parser's value as - // a Boolean - operator bool() const { return done(); } - void printLocation(std::ostream & out) const; - // Reset any local data that depends on validity checker - 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. - class ParserTemp; - extern ParserTemp* parserTemp; +class Parser { + + CVC4::SmtEngine *d_smt; + std::istream &d_is; + CVC4::Options *d_opts; + Language d_lang; + bool d_interactive; + void *d_buffer; + +public: + // Constructors + Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive = false) throw(); + // Destructor + ~Parser() throw(); + // Read the next command. + CVC4::Command* next() throw(); + // Check if we are done (end of input has been reached) + bool done() const throw(); + // The same check can be done by using the class Parser's value as + // a Boolean + operator bool() const throw() { return done(); } + void printLocation(std::ostream & out) const throw(); + // Reset any local data that depends on SmtEngine + void reset() throw(); +}; // end of class Parser }/* CVC4::parser namespace */ }/* CVC4 namespace */ |