diff options
Diffstat (limited to 'lib/SMT')
-rw-r--r-- | lib/SMT/parser.h | 71 |
1 files changed, 0 insertions, 71 deletions
diff --git a/lib/SMT/parser.h b/lib/SMT/parser.h deleted file mode 100644 index 30a01ac2..00000000 --- a/lib/SMT/parser.h +++ /dev/null @@ -1,71 +0,0 @@ -/*****************************************************************************/ -/*! - * \file parser.h - * - * Author: Sergey Berezin - * - * Created: Wed Feb 5 11:46:57 2003 - * - * <hr> - * - * License to use, copy, modify, sell and/or distribute this software - * and its documentation for any purpose is hereby granted without - * royalty, subject to the terms and conditions defined in the \ref - * LICENSE file provided with this distribution. - * - * <hr> - * - * The top-level API to the parser. At this level, it is simply a - * stream of commands (Expr's) terminated by an infinite sequence of - * Null Expr. It has a support to parse several different input - * languages (as many as we care to implement), and may take a file - * name, or an istream to read from (default: std::cin, or stdin). - * Using iostream means no more worries about whether to close files - * or not. - */ -/*****************************************************************************/ - -#ifndef _cvc3__parser_h_ -#define _cvc3__parser_h_ - -namespace CVC3 { - - // 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(// The 'interactive' flag is ignored when fileName != "" - bool interactive = true, - const std::string& fileName = ""); - Parser(std::istream& is, bool interactive = false); - // Destructor - ~Parser(); - // Read the next command. - klee::expr::ExprHandle 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; - -} // end of namespace CVC3 - -#endif |