about summary refs log tree commit diff homepage
path: root/lib/SMT
diff options
context:
space:
mode:
Diffstat (limited to 'lib/SMT')
-rw-r--r--lib/SMT/parser.h71
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