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-2021 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 cvc5::Integer
& value
)
94 : d_sexprType(SEXPR_INTEGER
),
95 d_integerValue(value
),
102 SExpr::SExpr(int value
)
103 : d_sexprType(SEXPR_INTEGER
),
104 d_integerValue(value
),
109 SExpr::SExpr(long int value
)
110 : d_sexprType(SEXPR_INTEGER
),
111 d_integerValue(value
),
116 SExpr::SExpr(unsigned int value
)
117 : d_sexprType(SEXPR_INTEGER
),
118 d_integerValue(value
),
123 SExpr::SExpr(unsigned long int value
)
124 : d_sexprType(SEXPR_INTEGER
),
125 d_integerValue(value
),
130 SExpr::SExpr(const cvc5::Rational
& value
)
131 : d_sexprType(SEXPR_RATIONAL
),
133 d_rationalValue(value
),
139 SExpr::SExpr(const std::string
& value
)
140 : d_sexprType(SEXPR_STRING
),
143 d_stringValue(value
),
147 * This constructs a string expression from a const char* value.
148 * This cannot be removed in order to support SExpr("foo").
149 * Given the other constructors this SExpr("foo") converts to bool.
150 * instead of SExpr(string("foo")).
152 SExpr::SExpr(const char* value
)
153 : d_sexprType(SEXPR_STRING
),
156 d_stringValue(value
),
159 SExpr::SExpr(bool value
)
160 : d_sexprType(SEXPR_KEYWORD
),
163 d_stringValue(value
? "true" : "false"),
166 SExpr::SExpr(const Keyword
& value
)
167 : d_sexprType(SEXPR_KEYWORD
),
170 d_stringValue(value
.getString()),
173 SExpr::SExpr(const std::vector
<SExpr
>& children
)
174 : d_sexprType(SEXPR_NOT_ATOM
),
178 d_children(new SExprVector(children
)) {}
180 std::string
SExpr::toString() const {
181 std::stringstream ss
;
186 /** Is this S-expression an atom? */
187 bool SExpr::isAtom() const { return d_sexprType
!= SEXPR_NOT_ATOM
; }
189 /** Is this S-expression an integer? */
190 bool SExpr::isInteger() const { return d_sexprType
== SEXPR_INTEGER
; }
192 /** Is this S-expression a rational? */
193 bool SExpr::isRational() const { return d_sexprType
== SEXPR_RATIONAL
; }
195 /** Is this S-expression a string? */
196 bool SExpr::isString() const { return d_sexprType
== SEXPR_STRING
; }
198 /** Is this S-expression a keyword? */
199 bool SExpr::isKeyword() const { return d_sexprType
== SEXPR_KEYWORD
; }
201 std::ostream
& operator<<(std::ostream
& out
, const SExpr
& sexpr
) {
202 SExpr::toStream(out
, sexpr
);
206 void SExpr::toStream(std::ostream
& out
, const SExpr
& sexpr
) {
207 toStream(out
, sexpr
, language::SetLanguage::getLanguage(out
));
210 void SExpr::toStream(std::ostream
& out
, const SExpr
& sexpr
,
211 OutputLanguage language
) {
212 const int indent
= PrettySExprs::getPrettySExprs(out
) ? 2 : 0;
213 toStream(out
, sexpr
, language
, indent
);
216 void SExpr::toStream(std::ostream
& out
, const SExpr
& sexpr
,
217 OutputLanguage language
, int indent
) {
218 if (sexpr
.isKeyword() && languageQuotesKeywords(language
)) {
219 out
<< quoteSymbol(sexpr
.getValue());
221 toStreamRec(out
, sexpr
, language
, indent
);
225 void SExpr::toStreamRec(std::ostream
& out
, const SExpr
& sexpr
,
226 OutputLanguage language
, int indent
) {
227 StreamFormatScope
scope(out
);
229 if (sexpr
.isInteger()) {
230 out
<< sexpr
.getIntegerValue();
231 } else if (sexpr
.isRational()) {
232 const double approximation
= sexpr
.getRationalValue().getDouble();
233 out
<< std::fixed
<< approximation
;
234 } else if (sexpr
.isKeyword()) {
235 out
<< sexpr
.getValue();
236 } else if (sexpr
.isString()) {
237 std::string s
= sexpr
.getValue();
238 // escape backslash and quote
239 for (size_t i
= 0; i
< s
.length(); ++i
) {
241 s
.replace(i
, 1, "\\\"");
243 } else if (s
[i
] == '\\') {
244 s
.replace(i
, 1, "\\\\");
248 out
<< "\"" << s
<< "\"";
250 const std::vector
<SExpr
>& kids
= sexpr
.getChildren();
251 out
<< (indent
> 0 && kids
.size() > 1 ? "( " : "(");
253 for (std::vector
<SExpr
>::const_iterator i
= kids
.begin(); i
!= kids
.end();
259 out
<< "\n" << std::string(indent
, ' ');
264 toStreamRec(out
, *i
, language
,
265 indent
<= 0 || indent
> 2 ? 0 : indent
+ 2);
267 if (indent
> 0 && kids
.size() > 1) {
270 out
<< std::string(indent
- 2, ' ');
275 } /* toStreamRec() */
277 bool SExpr::languageQuotesKeywords(OutputLanguage language
) {
279 case language::output::LANG_TPTP
:
281 case language::output::LANG_AST
:
282 case language::output::LANG_CVC3
:
283 case language::output::LANG_CVC4
:
284 default: return language::isOutputLang_smt2(language
);
288 std::string
SExpr::getValue() const {
289 PrettyCheckArgument(isAtom(), this);
290 switch (d_sexprType
) {
292 return d_integerValue
.toString();
293 case SEXPR_RATIONAL
: {
294 // We choose to represent rationals as decimal strings rather than
295 // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL
296 // could be added if we need both styles, even if it's backed by
297 // the same Rational object.
298 std::stringstream ss
;
299 ss
<< std::fixed
<< d_rationalValue
.getDouble();
304 return d_stringValue
;
306 return std::string();
308 return std::string();
311 const cvc5::Integer
& SExpr::getIntegerValue() const
313 PrettyCheckArgument(isInteger(), this);
314 return d_integerValue
;
317 const cvc5::Rational
& SExpr::getRationalValue() const
319 PrettyCheckArgument(isRational(), this);
320 return d_rationalValue
;
323 const std::vector
<SExpr
>& SExpr::getChildren() const {
324 PrettyCheckArgument(!isAtom(), this);
325 Assert(d_children
!= NULL
);
329 bool SExpr::operator==(const SExpr
& s
) const {
330 if (d_sexprType
== s
.d_sexprType
&& d_integerValue
== s
.d_integerValue
&&
331 d_rationalValue
== s
.d_rationalValue
&&
332 d_stringValue
== s
.d_stringValue
) {
333 if (d_children
== NULL
&& s
.d_children
== NULL
) {
335 } else if (d_children
!= NULL
&& s
.d_children
!= NULL
) {
336 return getChildren() == s
.getChildren();
342 bool SExpr::operator!=(const SExpr
& s
) const { return !(*this == s
); }
344 SExpr
SExpr::parseAtom(const std::string
& atom
) {
345 if (atom
== "true") {
347 } else if (atom
== "false") {
353 } catch (std::invalid_argument
&) {
354 // Fall through to the next case
359 } catch (std::invalid_argument
&) {
360 // Fall through to the next case
366 SExpr
SExpr::parseListOfAtoms(const std::vector
<std::string
>& atoms
) {
367 std::vector
<SExpr
> parsedAtoms
;
368 typedef std::vector
<std::string
>::const_iterator const_iterator
;
369 for (const_iterator i
= atoms
.begin(), i_end
= atoms
.end(); i
!= i_end
; ++i
) {
370 parsedAtoms
.push_back(parseAtom(*i
));
372 return SExpr(parsedAtoms
);
375 SExpr
SExpr::parseListOfListOfAtoms(
376 const std::vector
<std::vector
<std::string
> >& atoms_lists
) {
377 std::vector
<SExpr
> parsedListsOfAtoms
;
378 typedef std::vector
<std::vector
<std::string
> >::const_iterator const_iterator
;
379 for (const_iterator i
= atoms_lists
.begin(), i_end
= atoms_lists
.end();
381 parsedListsOfAtoms
.push_back(parseListOfAtoms(*i
));
383 return SExpr(parsedListsOfAtoms
);