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
|
/********************* */
/*! \file sexpr.cpp
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Simple representation of S-expressions
**
** Simple representation of S-expressions.
**
** SExprs have their own language specific printing procedures. The reason for
** this being implemented on SExpr and not on the Printer class is that the
** Printer class lives in libcvc4. It has to currently as it prints fairly
** complicated objects, like Model, which in turn uses SmtEngine pointers.
** However, SExprs need to be printed by Statistics. To get the output consistent
** with the previous version, the printing of SExprs in different languages is
** handled in the SExpr class and the libexpr library.
**/
#include "expr/sexpr.h"
#include <iostream>
#include <sstream>
#include <vector>
#include "base/cvc4_assert.h"
#include "expr/expr.h"
#include "util/smt2_quote_string.h"
namespace CVC4 {
const int PrettySExprs::s_iosIndex = std::ios_base::xalloc();
std::ostream& operator<<(std::ostream& out, PrettySExprs ps) {
ps.applyPrettySExprs(out);
return out;
}
std::string SExpr::toString() const {
std::stringstream ss;
ss << (*this);
return ss.str();
}
std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
SExpr::toStream(out, sexpr);
return out;
}
void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() {
toStream(out, sexpr, Expr::setlanguage::getLanguage(out));
}
void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() {
toStream(out, sexpr, language, PrettySExprs::getPrettySExprs(out) ? 2 : 0);
}
void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() {
if( sexpr.isKeyword() && languageQuotesKeywords(language) ){
out << quoteSymbol(sexpr.getValue());
} else {
toStreamRec(out, sexpr, language, indent);
}
}
void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() {
if(sexpr.isInteger()) {
out << sexpr.getIntegerValue();
} else if(sexpr.isRational()) {
out << std::fixed << sexpr.getRationalValue().getDouble();
} else if(sexpr.isKeyword()) {
out << sexpr.getValue();
} else if(sexpr.isString()) {
std::string s = sexpr.getValue();
// escape backslash and quote
for(size_t i = 0; i < s.length(); ++i) {
if(s[i] == '"') {
s.replace(i, 1, "\\\"");
++i;
} else if(s[i] == '\\') {
s.replace(i, 1, "\\\\");
++i;
}
}
out << "\"" << s << "\"";
} else {
const std::vector<SExpr>& kids = sexpr.getChildren();
out << (indent > 0 && kids.size() > 1 ? "( " : "(");
bool first = true;
for(std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
if(first) {
first = false;
} else {
if(indent > 0) {
out << "\n" << std::string(indent, ' ');
} else {
out << ' ';
}
}
toStreamRec(out, *i, language, indent <= 0 || indent > 2 ? 0 : indent + 2);
}
if(indent > 0 && kids.size() > 1) {
out << '\n';
if(indent > 2) {
out << std::string(indent - 2, ' ');
}
}
out << ')';
}
}/* toStreamRec() */
bool SExpr::languageQuotesKeywords(OutputLanguage language) {
switch(language) {
case language::output::LANG_SMTLIB_V1:
case language::output::LANG_SMTLIB_V2_0:
case language::output::LANG_SMTLIB_V2_5:
case language::output::LANG_SYGUS:
case language::output::LANG_TPTP:
case language::output::LANG_Z3STR:
return true;
case language::output::LANG_AST:
case language::output::LANG_CVC3:
case language::output::LANG_CVC4:
default:
return false;
};
}
std::string SExpr::getValue() const {
CheckArgument( isAtom(), this );
switch(d_sexprType) {
case SEXPR_INTEGER:
return d_integerValue.toString();
case SEXPR_RATIONAL: {
// We choose to represent rationals as decimal strings rather than
// "numerator/denominator." Perhaps an additional SEXPR_DECIMAL
// could be added if we need both styles, even if it's backed by
// the same Rational object.
std::stringstream ss;
ss << std::fixed << d_rationalValue.getDouble();
return ss.str();
}
case SEXPR_STRING:
case SEXPR_KEYWORD:
return d_stringValue;
case SEXPR_NOT_ATOM:
return std::string();
}
return std::string();
}
const CVC4::Integer& SExpr::getIntegerValue() const {
CheckArgument( isInteger(), this );
return d_integerValue;
}
const CVC4::Rational& SExpr::getRationalValue() const {
CheckArgument( isRational(), this );
return d_rationalValue;
}
const std::vector<SExpr>& SExpr::getChildren() const {
CheckArgument( !isAtom(), this );
return d_children;
}
bool SExpr::operator==(const SExpr& s) const {
return d_sexprType == s.d_sexprType &&
d_integerValue == s.d_integerValue &&
d_rationalValue == s.d_rationalValue &&
d_stringValue == s.d_stringValue &&
d_children == s.d_children;
}
bool SExpr::operator!=(const SExpr& s) const {
return !(*this == s);
}
SExpr SExpr::parseAtom(const std::string& atom) {
if(atom == "true"){
return SExpr(true);
} else if(atom == "false"){
return SExpr(false);
} else {
try {
Integer z(atom);
return SExpr(z);
}catch(std::invalid_argument&){
// Fall through to the next case
}
try {
Rational q(atom);
return SExpr(q);
}catch(std::invalid_argument&){
// Fall through to the next case
}
return SExpr(atom);
}
}
SExpr SExpr::parseListOfAtoms(const std::vector<std::string>& atoms) {
std::vector<SExpr> parsedAtoms;
typedef std::vector<std::string>::const_iterator const_iterator;
for(const_iterator i = atoms.begin(), i_end=atoms.end(); i != i_end; ++i){
parsedAtoms.push_back(parseAtom(*i));
}
return SExpr(parsedAtoms);
}
SExpr SExpr::parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists) {
std::vector<SExpr> parsedListsOfAtoms;
typedef std::vector< std::vector<std::string> >::const_iterator const_iterator;
for(const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); i != i_end; ++i){
parsedListsOfAtoms.push_back(parseListOfAtoms(*i));
}
return SExpr(parsedListsOfAtoms);
}
}/* CVC4 namespace */
|
