1 /********************* */
4 ** Top contributors (to current version):
5 ** Tim King, Morgan Deters, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Simple representation of S-expressions
14 ** Simple representation of S-expressions.
16 ** SExprs have their own language specific printing procedures. The reason for
17 ** this being implemented on SExpr and not on the Printer class is that the
18 ** Printer class lives in libcvc4. It has to currently as it prints fairly
19 ** complicated objects, like Model, which in turn uses SmtEngine pointers.
20 ** However, SExprs need to be printed by Statistics. To get the output
21 ** consistent with the previous version, the printing of SExprs in different
22 ** languages is handled in the SExpr class and the libexpr library.
25 #include "util/sexpr.h"
31 #include "base/check.h"
32 #include "options/set_language.h"
33 #include "util/ostream_util.h"
34 #include "util/smt2_quote_string.h"
38 const int PrettySExprs::s_iosIndex
= std::ios_base::xalloc();
40 std::ostream
& operator<<(std::ostream
& out
, PrettySExprs ps
) {
41 ps
.applyPrettySExprs(out
);
46 if (d_children
!= NULL
) {
50 Assert(d_children
== NULL
);
53 SExpr
& SExpr::operator=(const SExpr
& other
) {
54 d_sexprType
= other
.d_sexprType
;
55 d_integerValue
= other
.d_integerValue
;
56 d_rationalValue
= other
.d_rationalValue
;
57 d_stringValue
= other
.d_stringValue
;
59 if (d_children
== NULL
&& other
.d_children
== NULL
) {
61 } else if (d_children
== NULL
) {
62 d_children
= new SExprVector(*other
.d_children
);
63 } else if (other
.d_children
== NULL
) {
67 (*d_children
) = other
.getChildren();
69 Assert(isAtom() == other
.isAtom());
70 Assert((d_children
== NULL
) == isAtom());
75 : d_sexprType(SEXPR_STRING
),
81 SExpr::SExpr(const SExpr
& other
)
82 : d_sexprType(other
.d_sexprType
),
83 d_integerValue(other
.d_integerValue
),
84 d_rationalValue(other
.d_rationalValue
),
85 d_stringValue(other
.d_stringValue
),
88 (other
.d_children
== NULL
) ? NULL
: new SExprVector(*other
.d_children
);
89 // d_children being NULL is equivalent to the node being an atom.
90 Assert((d_children
== NULL
) == isAtom());
93 SExpr::SExpr(const CVC4::Integer
& value
)
94 : d_sexprType(SEXPR_INTEGER
),
95 d_integerValue(value
),
100 SExpr::SExpr(int value
)
101 : d_sexprType(SEXPR_INTEGER
),
102 d_integerValue(value
),
107 SExpr::SExpr(long int value
)
108 : d_sexprType(SEXPR_INTEGER
),
109 d_integerValue(value
),
114 SExpr::SExpr(unsigned int value
)
115 : d_sexprType(SEXPR_INTEGER
),
116 d_integerValue(value
),
121 SExpr::SExpr(unsigned long int value
)
122 : d_sexprType(SEXPR_INTEGER
),
123 d_integerValue(value
),
128 SExpr::SExpr(const CVC4::Rational
& value
)
129 : d_sexprType(SEXPR_RATIONAL
),
131 d_rationalValue(value
),
135 SExpr::SExpr(const std::string
& value
)
136 : d_sexprType(SEXPR_STRING
),
139 d_stringValue(value
),
143 * This constructs a string expression from a const char* value.
144 * This cannot be removed in order to support SExpr("foo").
145 * Given the other constructors this SExpr("foo") converts to bool.
146 * instead of SExpr(string("foo")).
148 SExpr::SExpr(const char* value
)
149 : d_sexprType(SEXPR_STRING
),
152 d_stringValue(value
),
155 SExpr::SExpr(bool value
)
156 : d_sexprType(SEXPR_KEYWORD
),
159 d_stringValue(value
? "true" : "false"),
162 SExpr::SExpr(const Keyword
& value
)
163 : d_sexprType(SEXPR_KEYWORD
),
166 d_stringValue(value
.getString()),
169 SExpr::SExpr(const std::vector
<SExpr
>& children
)
170 : d_sexprType(SEXPR_NOT_ATOM
),
174 d_children(new SExprVector(children
)) {}
176 std::string
SExpr::toString() const {
177 std::stringstream ss
;
182 /** Is this S-expression an atom? */
183 bool SExpr::isAtom() const { return d_sexprType
!= SEXPR_NOT_ATOM
; }
185 /** Is this S-expression an integer? */
186 bool SExpr::isInteger() const { return d_sexprType
== SEXPR_INTEGER
; }
188 /** Is this S-expression a rational? */
189 bool SExpr::isRational() const { return d_sexprType
== SEXPR_RATIONAL
; }
191 /** Is this S-expression a string? */
192 bool SExpr::isString() const { return d_sexprType
== SEXPR_STRING
; }
194 /** Is this S-expression a keyword? */
195 bool SExpr::isKeyword() const { return d_sexprType
== SEXPR_KEYWORD
; }
197 std::ostream
& operator<<(std::ostream
& out
, const SExpr
& sexpr
) {
198 SExpr::toStream(out
, sexpr
);
202 void SExpr::toStream(std::ostream
& out
, const SExpr
& sexpr
) {
203 toStream(out
, sexpr
, language::SetLanguage::getLanguage(out
));
206 void SExpr::toStream(std::ostream
& out
, const SExpr
& sexpr
,
207 OutputLanguage language
) {
208 const int indent
= PrettySExprs::getPrettySExprs(out
) ? 2 : 0;
209 toStream(out
, sexpr
, language
, indent
);
212 void SExpr::toStream(std::ostream
& out
, const SExpr
& sexpr
,
213 OutputLanguage language
, int indent
) {
214 if (sexpr
.isKeyword() && languageQuotesKeywords(language
)) {
215 out
<< quoteSymbol(sexpr
.getValue());
217 toStreamRec(out
, sexpr
, language
, indent
);
221 void SExpr::toStreamRec(std::ostream
& out
, const SExpr
& sexpr
,
222 OutputLanguage language
, int indent
) {
223 StreamFormatScope
scope(out
);
225 if (sexpr
.isInteger()) {
226 out
<< sexpr
.getIntegerValue();
227 } else if (sexpr
.isRational()) {
228 const double approximation
= sexpr
.getRationalValue().getDouble();
229 out
<< std::fixed
<< approximation
;
230 } else if (sexpr
.isKeyword()) {
231 out
<< sexpr
.getValue();
232 } else if (sexpr
.isString()) {
233 std::string s
= sexpr
.getValue();
234 // escape backslash and quote
235 for (size_t i
= 0; i
< s
.length(); ++i
) {
237 s
.replace(i
, 1, "\\\"");
239 } else if (s
[i
] == '\\') {
240 s
.replace(i
, 1, "\\\\");
244 out
<< "\"" << s
<< "\"";
246 const std::vector
<SExpr
>& kids
= sexpr
.getChildren();
247 out
<< (indent
> 0 && kids
.size() > 1 ? "( " : "(");
249 for (std::vector
<SExpr
>::const_iterator i
= kids
.begin(); i
!= kids
.end();
255 out
<< "\n" << std::string(indent
, ' ');
260 toStreamRec(out
, *i
, language
,
261 indent
<= 0 || indent
> 2 ? 0 : indent
+ 2);
263 if (indent
> 0 && kids
.size() > 1) {
266 out
<< std::string(indent
- 2, ' ');
271 } /* toStreamRec() */
273 bool SExpr::languageQuotesKeywords(OutputLanguage language
) {
275 case language::output::LANG_TPTP
:
277 case language::output::LANG_AST
:
278 case language::output::LANG_CVC3
:
279 case language::output::LANG_CVC4
:
280 default: return language::isOutputLang_smt2(language
);
284 std::string
SExpr::getValue() const {
285 PrettyCheckArgument(isAtom(), this);
286 switch (d_sexprType
) {
288 return d_integerValue
.toString();
289 case SEXPR_RATIONAL
: {
290 // We choose to represent rationals as decimal strings rather than
291 // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL
292 // could be added if we need both styles, even if it's backed by
293 // the same Rational object.
294 std::stringstream ss
;
295 ss
<< std::fixed
<< d_rationalValue
.getDouble();
300 return d_stringValue
;
302 return std::string();
304 return std::string();
307 const CVC4::Integer
& SExpr::getIntegerValue() const {
308 PrettyCheckArgument(isInteger(), this);
309 return d_integerValue
;
312 const CVC4::Rational
& SExpr::getRationalValue() const {
313 PrettyCheckArgument(isRational(), this);
314 return d_rationalValue
;
317 const std::vector
<SExpr
>& SExpr::getChildren() const {
318 PrettyCheckArgument(!isAtom(), this);
319 Assert(d_children
!= NULL
);
323 bool SExpr::operator==(const SExpr
& s
) const {
324 if (d_sexprType
== s
.d_sexprType
&& d_integerValue
== s
.d_integerValue
&&
325 d_rationalValue
== s
.d_rationalValue
&&
326 d_stringValue
== s
.d_stringValue
) {
327 if (d_children
== NULL
&& s
.d_children
== NULL
) {
329 } else if (d_children
!= NULL
&& s
.d_children
!= NULL
) {
330 return getChildren() == s
.getChildren();
336 bool SExpr::operator!=(const SExpr
& s
) const { return !(*this == s
); }
338 SExpr
SExpr::parseAtom(const std::string
& atom
) {
339 if (atom
== "true") {
341 } else if (atom
== "false") {
347 } catch (std::invalid_argument
&) {
348 // Fall through to the next case
353 } catch (std::invalid_argument
&) {
354 // Fall through to the next case
360 SExpr
SExpr::parseListOfAtoms(const std::vector
<std::string
>& atoms
) {
361 std::vector
<SExpr
> parsedAtoms
;
362 typedef std::vector
<std::string
>::const_iterator const_iterator
;
363 for (const_iterator i
= atoms
.begin(), i_end
= atoms
.end(); i
!= i_end
; ++i
) {
364 parsedAtoms
.push_back(parseAtom(*i
));
366 return SExpr(parsedAtoms
);
369 SExpr
SExpr::parseListOfListOfAtoms(
370 const std::vector
<std::vector
<std::string
> >& atoms_lists
) {
371 std::vector
<SExpr
> parsedListsOfAtoms
;
372 typedef std::vector
<std::vector
<std::string
> >::const_iterator const_iterator
;
373 for (const_iterator i
= atoms_lists
.begin(), i_end
= atoms_lists
.end();
375 parsedListsOfAtoms
.push_back(parseListOfAtoms(*i
));
377 return SExpr(parsedListsOfAtoms
);
380 } /* CVC4 namespace */