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
|
/*****************************************************************************/
/*!
* \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 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(InputLanguage lang, bool interactive,
const std::string& fileName)
: d_data(new ParserData) {
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(InputLanguage lang, std::istream& is, bool interactive)
: d_data(new ParserData) {
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 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 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 NULL;//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 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 NULL;//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 = NULL;//Expr();
}
} // end of namespace CVC3
|
