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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
|
/*****************************************************************************/
/*!
* \file parser.cpp
* \brief The top-level API to the parser. See parser.h for details.
*
* 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>
*
*/
/*****************************************************************************/
#include <fstream>
#include <iomanip>
#include "parser_temp.h"
#include "parser.h"
#include "parser_exception.h"
using namespace std;
// The communication entry points of the actual parsers
// for presentation language (PL.y and PL.lex)
extern int PLparse();
extern void *PL_createBuffer(int);
extern void PL_deleteBuffer(void *);
extern void PL_switchToBuffer(void *);
extern int PL_bufSize();
extern void *PL_bufState();
void PL_setInteractive(bool);
// for Lisp language (Lisp.y and Lisp.lex)
extern int Lispparse();
extern void *Lisp_createBuffer(int);
extern void Lisp_deleteBuffer(void *);
extern void Lisp_switchToBuffer(void *);
extern int Lisp_bufSize();
extern void *LispBufState();
void Lisp_setInteractive(bool);
// for Lisp language (Lisp.y and Lisp.lex)
extern int Lispparse();
extern void *Lisp_createBuffer(int);
extern void Lisp_deleteBuffer(void *);
extern void Lisp_switchToBuffer(void *);
extern int Lisp_bufSize();
extern void *LispBufState();
void Lisp_setInteractive(bool);
// for smtlib language (smtlib.y and smtlib.lex)
extern int smtlibparse();
extern void *smtlib_createBuffer(int);
extern void smtlib_deleteBuffer(void *);
extern void smtlib_switchToBuffer(void *);
extern int smtlib_bufSize();
extern void *smtlibBufState();
void smtlib_setInteractive(bool);
namespace CVC3 {
// 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.
// FIXME: This should probably go away eventually, when I figure out
// flex++ -- Sergey.
ParserTemp* parserTemp;
int ParserTemp::error(const string& s) {
throw ParserException(s);
return 0;
}
// Internal storage class; I'll use member names without 'd_'s here
class ParserData {
public:
// Which language to use
InputLanguage lang;
// Is the input given by the file name or as istream?
bool useName;
ParserTemp temp;
// Internal buffer used by the parser
void* buffer;
};
// Constructors
Parser::Parser(ValidityChecker* vc, InputLanguage lang,
bool interactive,
const std::string& fileName)
: d_data(new ParserData) {
d_data->temp.vc = vc;
d_data->lang = lang;
if(fileName == "") {
// Use std::cin
d_data->useName = false;
d_data->temp.is = &cin;
d_data->temp.fileName = "stdin";
d_data->temp.interactive = interactive;
} else {
// Open the file by name
d_data->useName = true;
d_data->temp.fileName = fileName;
d_data->temp.is = new ifstream(fileName.c_str());
if (!(*d_data->temp.is)) {
throw ParserException("File not found: "+fileName);
}
d_data->temp.interactive = false;
}
initParser();
}
Parser::Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is,
bool interactive)
: d_data(new ParserData) {
d_data->temp.vc = vc;
d_data->lang = lang;
d_data->useName = false;
d_data->temp.is = &is;
d_data->temp.fileName = "stdin";
d_data->temp.interactive = interactive;
initParser();
}
// Destructor
Parser::~Parser() {
if(d_data->useName) // Stream is ours; delete it
delete d_data->temp.is;
deleteParser();
delete d_data;
}
// Initialize the actual parser
void Parser::initParser() {
switch(d_data->lang) {
case PRESENTATION_LANG:
d_data->buffer = PL_createBuffer(PL_bufSize());
d_data->temp.lineNum = 1;
break;
case LISP_LANG:
d_data->buffer = Lisp_createBuffer(Lisp_bufSize());
d_data->temp.lineNum = 1;
break;
case SMTLIB_LANG:
d_data->buffer = smtlib_createBuffer(smtlib_bufSize());
d_data->temp.lineNum = 1;
break;
default: FatalAssert(false, "Bad input language specified"); exit(1);
}
}
// Clean up the parser's internal data structures
void Parser::deleteParser() {
switch(d_data->lang) {
case PRESENTATION_LANG:
PL_deleteBuffer(d_data->buffer);
break;
case LISP_LANG:
Lisp_deleteBuffer(d_data->buffer);
break;
case SMTLIB_LANG:
smtlib_deleteBuffer(d_data->buffer);
break;
default: FatalAssert(false, "Bad input language specified");
}
}
Expr Parser::next() {
// If no more commands are available, return a Null Expr
if(d_data->temp.done) return Expr();
// Set the global var so the parser uses the right stream and EM
parserTemp = &(d_data->temp);
// Switch to our buffer, in case there are multiple instances of
// the parser running
try {
switch(d_data->lang) {
case PRESENTATION_LANG:
PL_switchToBuffer(d_data->buffer);
PL_setInteractive(d_data->temp.interactive);
PLparse();
// Reset the prompt to the main one
d_data->temp.setPrompt1();
break;
case LISP_LANG:
Lisp_switchToBuffer(d_data->buffer);
Lisp_setInteractive(d_data->temp.interactive);
Lispparse();
// Reset the prompt to the main one
d_data->temp.setPrompt1();
break;
case SMTLIB_LANG:
smtlib_switchToBuffer(d_data->buffer);
smtlib_setInteractive(d_data->temp.interactive);
smtlibparse();
// Reset the prompt to the main one
d_data->temp.setPrompt1();
break;
default: {
ostringstream ss;
ss << "Bad input language specified: " << d_data->lang;
DebugAssert(false, ss.str().c_str()); exit(1);
}
}
} catch(Exception* e) {
cerr << d_data->temp.fileName << ":" << d_data->temp.lineNum
<< ": " << e << endl;
return Expr();
}
return d_data->temp.expr;
}
bool Parser::done() const { return d_data->temp.done; }
void Parser::printLocation(ostream & out) const
{
out << d_data->temp.fileName << ":" << d_data->temp.lineNum;
}
void Parser::reset()
{
d_data->temp.expr = Expr();
}
} // end of namespace CVC3
|
