CVC3  2.4.1
parser.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file parser.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Wed Feb 5 11:46:57 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  * The top-level API to the parser. At this level, it is simply a
19  * stream of commands (Expr's) terminated by an infinite sequence of
20  * Null Expr. It has a support to parse several different input
21  * languages (as many as we care to implement), and may take a file
22  * name, or an istream to read from (default: std::cin, or stdin).
23  * Using iostream means no more worries about whether to close files
24  * or not.
25  */
26 /*****************************************************************************/
27 
28 #ifndef _cvc3__parser_h_
29 #define _cvc3__parser_h_
30 
31 #include "exception.h"
32 #include "lang.h"
33 
34 namespace CVC3 {
35 
36  class ValidityChecker;
37  class Translator;
38  class Expr;
39 
40  // Internal parser state and other data
41  class ParserData;
42 
43  class Parser {
44  private:
45  ParserData* d_data;
46  // Internal methods for constructing and destroying the actual parser
47  void initParser();
48  void deleteParser();
49  public:
50  // Constructors
51  Parser(ValidityChecker* vc, Translator* translator, InputLanguage lang,
52  // The 'interactive' flag is ignored when fileName != ""
53  bool interactive = true,
54  const std::string& fileName = "");
55  Parser(ValidityChecker* vc, Translator* translator, InputLanguage lang, std::istream& is,
56  bool interactive = false);
57  // Destructor
58  ~Parser();
59  // Read the next command.
60  Expr next();
61  // Check if we are done (end of input has been reached)
62  bool done() const;
63  // The same check can be done by using the class Parser's value as
64  // a Boolean
65  operator bool() const { return done(); }
66  void printLocation(std::ostream & out) const;
67  // Reset any local data that depends on validity checker
68  void reset();
69  }; // end of class Parser
70 
71  // The global pointer to ParserTemp. Each instance of class Parser
72  // sets this pointer before any calls to the lexer. We do it this
73  // way because flex and bison use global vars, and we want each
74  // Parser object to appear independent.
75  class ParserTemp;
76  extern ParserTemp* parserTemp;
77 
78 } // end of namespace CVC3
79 
80 #endif