blob: 411e7760c55f1f73ed0ed9568251eb17a4f87382 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
/********************* -*- C++ -*- */
/** parser.h
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.
**
** Parser abstraction.
**/
#ifndef __CVC4__PARSER__PARSER_H
#define __CVC4__PARSER__PARSER_H
#include <string>
#include <iostream>
#include "parser/language.h"
#include "parser/parser_state.h"
namespace CVC4 {
// Forward declarations
class Expr;
class Command;
class ExprManager;
class SmtEngine;
class Options;
namespace 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 CVC4_PUBLIC *_global_parser_state;
/**
* The parser.
*/
class CVC4_PUBLIC Parser {
private:
/** Internal parser state we are keeping */
//ParserState* d_data;
/** Initialize the parser */
void initParser();
/** Remove the parser components */
void deleteParser();
Language d_lang;
std::istream &d_in;
Options *d_opts;
public:
/**
* 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);
}
/**
* Destructor.
*/
~Parser();
/** Parse a command */
Command* parseNextCommand(bool verbose = false);
/** Parse an expression of the stream */
Expr parseNextExpression();
// 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(); }
/** Prints the location to the output stream */
void printLocation(std::ostream& out) const;
/** Reset any local data */
void reset();
}; // end of class Parser
}/* CVC4::parser namespace */
}/* CVC4 namespace */
#endif /* __CVC4__PARSER__PARSER_H */
|
