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
|
// small unit test for parsing SMT 2 files
#include <cstdlib>
#include <iostream>
#include <solvers/smt2/smt2_parser.h>
/*******************************************************************\
Function: smt2_parser_test
Inputs:
Outputs:
Purpose:
\*******************************************************************/
class smt2_parser_testt:public smt2_parsert
{
public:
smt2_parser_testt(std::istream &_in, std::ostream &_out):
smt2_parsert(_in), out(_out), first(true)
{
}
protected:
std::ostream &out;
bool first;
// overload from smt2_parsert
virtual void symbol()
{
if(first)
first=false;
else
out << ' ';
// possibly need to quote
out << buffer;
}
virtual void keyword()
{
if(first)
first=false;
else
out << ' ';
out << ':' << buffer;
}
virtual void string_literal()
{
if(first)
first=false;
else
out << ' ';
out << '"';
for(unsigned i=0; i<buffer.size(); i++)
{
char ch=buffer[i];
if(ch=='"') out << '"';
out << ch;
}
out << '"';
}
virtual void numeral()
{
if(first)
first=false;
else
out << ' ';
out << buffer;
}
virtual void open_expression() // '('
{
if(!first)
out << ' ';
out << '(';
first=true;
}
virtual void close_expression() // ')'
{
out << ')';
first=false;
}
virtual void error(const std::string &message)
{
std::cerr << "error: " << message << '\n';
exit(0);
}
};
int main()
{
while(std::cin)
{
smt2_parser_testt(std::cin, std::cout)();
std::cout << '\n';
}
}
|
