GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/sexpr.cpp Lines: 97 181 53.6 %
Date: 2021-03-23 Branches: 91 363 25.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sexpr.cpp
3
 ** \verbatim
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
11
 **
12
 ** \brief Simple representation of S-expressions
13
 **
14
 ** Simple representation of S-expressions.
15
 **
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.
23
 **/
24
25
#include "util/sexpr.h"
26
27
#include <iostream>
28
#include <sstream>
29
#include <vector>
30
31
#include "base/check.h"
32
#include "options/set_language.h"
33
#include "util/ostream_util.h"
34
#include "util/smt2_quote_string.h"
35
36
namespace CVC4 {
37
38
8895
const int PrettySExprs::s_iosIndex = std::ios_base::xalloc();
39
40
std::ostream& operator<<(std::ostream& out, PrettySExprs ps) {
41
  ps.applyPrettySExprs(out);
42
  return out;
43
}
44
45
1698
SExpr::~SExpr() {
46
849
  if (d_children != NULL) {
47
178
    delete d_children;
48
178
    d_children = NULL;
49
  }
50
849
  Assert(d_children == NULL);
51
849
}
52
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;
58
59
  if (d_children == NULL && other.d_children == NULL) {
60
    // Do nothing.
61
  } else if (d_children == NULL) {
62
    d_children = new SExprVector(*other.d_children);
63
  } else if (other.d_children == NULL) {
64
    delete d_children;
65
    d_children = NULL;
66
  } else {
67
    (*d_children) = other.getChildren();
68
  }
69
  Assert(isAtom() == other.isAtom());
70
  Assert((d_children == NULL) == isAtom());
71
  return *this;
72
}
73
74
SExpr::SExpr()
75
    : d_sexprType(SEXPR_STRING),
76
      d_integerValue(0),
77
      d_rationalValue(0),
78
      d_stringValue(""),
79
      d_children(NULL) {}
80
81
683
SExpr::SExpr(const SExpr& other)
82
683
    : d_sexprType(other.d_sexprType),
83
      d_integerValue(other.d_integerValue),
84
      d_rationalValue(other.d_rationalValue),
85
      d_stringValue(other.d_stringValue),
86
683
      d_children(NULL) {
87
683
  d_children =
88
683
      (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children);
89
  // d_children being NULL is equivalent to the node being an atom.
90
683
  Assert((d_children == NULL) == isAtom());
91
683
}
92
93
48
SExpr::SExpr(const CVC4::Integer& value)
94
    : d_sexprType(SEXPR_INTEGER),
95
      d_integerValue(value),
96
      d_rationalValue(0),
97
      d_stringValue(""),
98
48
      d_children(NULL) {}
99
100
SExpr::SExpr(int value)
101
    : d_sexprType(SEXPR_INTEGER),
102
      d_integerValue(value),
103
      d_rationalValue(0),
104
      d_stringValue(""),
105
      d_children(NULL) {}
106
107
SExpr::SExpr(long int value)
108
    : d_sexprType(SEXPR_INTEGER),
109
      d_integerValue(value),
110
      d_rationalValue(0),
111
      d_stringValue(""),
112
      d_children(NULL) {}
113
114
SExpr::SExpr(unsigned int value)
115
    : d_sexprType(SEXPR_INTEGER),
116
      d_integerValue(value),
117
      d_rationalValue(0),
118
      d_stringValue(""),
119
      d_children(NULL) {}
120
121
SExpr::SExpr(unsigned long int value)
122
    : d_sexprType(SEXPR_INTEGER),
123
      d_integerValue(value),
124
      d_rationalValue(0),
125
      d_stringValue(""),
126
      d_children(NULL) {}
127
128
14
SExpr::SExpr(const CVC4::Rational& value)
129
    : d_sexprType(SEXPR_RATIONAL),
130
      d_integerValue(0),
131
      d_rationalValue(value),
132
      d_stringValue(""),
133
14
      d_children(NULL) {}
134
135
57
SExpr::SExpr(const std::string& value)
136
    : d_sexprType(SEXPR_STRING),
137
      d_integerValue(0),
138
      d_rationalValue(0),
139
      d_stringValue(value),
140
57
      d_children(NULL) {}
141
142
/**
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")).
147
 */
148
SExpr::SExpr(const char* value)
149
    : d_sexprType(SEXPR_STRING),
150
      d_integerValue(0),
151
      d_rationalValue(0),
152
      d_stringValue(value),
153
      d_children(NULL) {}
154
155
SExpr::SExpr(bool value)
156
    : d_sexprType(SEXPR_KEYWORD),
157
      d_integerValue(0),
158
      d_rationalValue(0),
159
      d_stringValue(value ? "true" : "false"),
160
      d_children(NULL) {}
161
162
8
SExpr::SExpr(const Keyword& value)
163
    : d_sexprType(SEXPR_KEYWORD),
164
      d_integerValue(0),
165
      d_rationalValue(0),
166
8
      d_stringValue(value.getString()),
167
16
      d_children(NULL) {}
168
169
39
SExpr::SExpr(const std::vector<SExpr>& children)
170
    : d_sexprType(SEXPR_NOT_ATOM),
171
      d_integerValue(0),
172
      d_rationalValue(0),
173
      d_stringValue(""),
174
39
      d_children(new SExprVector(children)) {}
175
176
14
std::string SExpr::toString() const {
177
28
  std::stringstream ss;
178
14
  ss << (*this);
179
28
  return ss.str();
180
}
181
182
/** Is this S-expression an atom? */
183
780
bool SExpr::isAtom() const { return d_sexprType != SEXPR_NOT_ATOM; }
184
185
/** Is this S-expression an integer? */
186
144
bool SExpr::isInteger() const { return d_sexprType == SEXPR_INTEGER; }
187
188
/** Is this S-expression a rational? */
189
103
bool SExpr::isRational() const { return d_sexprType == SEXPR_RATIONAL; }
190
191
/** Is this S-expression a string? */
192
89
bool SExpr::isString() const { return d_sexprType == SEXPR_STRING; }
193
194
/** Is this S-expression a keyword? */
195
103
bool SExpr::isKeyword() const { return d_sexprType == SEXPR_KEYWORD; }
196
197
14
std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
198
14
  SExpr::toStream(out, sexpr);
199
14
  return out;
200
}
201
202
14
void SExpr::toStream(std::ostream& out, const SExpr& sexpr) {
203
14
  toStream(out, sexpr, language::SetLanguage::getLanguage(out));
204
14
}
205
206
14
void SExpr::toStream(std::ostream& out, const SExpr& sexpr,
207
                     OutputLanguage language) {
208
14
  const int indent = PrettySExprs::getPrettySExprs(out) ? 2 : 0;
209
14
  toStream(out, sexpr, language, indent);
210
14
}
211
212
14
void SExpr::toStream(std::ostream& out, const SExpr& sexpr,
213
                     OutputLanguage language, int indent) {
214
14
  if (sexpr.isKeyword() && languageQuotesKeywords(language)) {
215
8
    out << quoteSymbol(sexpr.getValue());
216
  } else {
217
6
    toStreamRec(out, sexpr, language, indent);
218
  }
219
14
}
220
221
120
void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
222
                        OutputLanguage language, int indent) {
223
240
  StreamFormatScope scope(out);
224
225
120
  if (sexpr.isInteger()) {
226
24
    out << sexpr.getIntegerValue();
227
96
  } else if (sexpr.isRational()) {
228
7
    const double approximation = sexpr.getRationalValue().getDouble();
229
7
    out << std::fixed << approximation;
230
89
  } else if (sexpr.isKeyword()) {
231
    out << sexpr.getValue();
232
89
  } else if (sexpr.isString()) {
233
100
    std::string s = sexpr.getValue();
234
    // escape backslash and quote
235
2771
    for (size_t i = 0; i < s.length(); ++i) {
236
2721
      if (s[i] == '"') {
237
2
        s.replace(i, 1, "\\\"");
238
2
        ++i;
239
2719
      } else if (s[i] == '\\') {
240
        s.replace(i, 1, "\\\\");
241
        ++i;
242
      }
243
    }
244
50
    out << "\"" << s << "\"";
245
  } else {
246
39
    const std::vector<SExpr>& kids = sexpr.getChildren();
247
39
    out << (indent > 0 && kids.size() > 1 ? "( " : "(");
248
39
    bool first = true;
249
153
    for (std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end();
250
         ++i) {
251
114
      if (first) {
252
39
        first = false;
253
      } else {
254
75
        if (indent > 0) {
255
          out << "\n" << std::string(indent, ' ');
256
        } else {
257
75
          out << ' ';
258
        }
259
      }
260
114
      toStreamRec(out, *i, language,
261
                  indent <= 0 || indent > 2 ? 0 : indent + 2);
262
    }
263
39
    if (indent > 0 && kids.size() > 1) {
264
      out << '\n';
265
      if (indent > 2) {
266
        out << std::string(indent - 2, ' ');
267
      }
268
    }
269
39
    out << ')';
270
  }
271
120
} /* toStreamRec() */
272
273
8
bool SExpr::languageQuotesKeywords(OutputLanguage language) {
274
8
  switch (language) {
275
    case language::output::LANG_TPTP:
276
      return true;
277
8
    case language::output::LANG_AST:
278
    case language::output::LANG_CVC3:
279
    case language::output::LANG_CVC4:
280
8
    default: return language::isOutputLang_smt2(language);
281
  };
282
}
283
284
58
std::string SExpr::getValue() const {
285
58
  PrettyCheckArgument(isAtom(), this);
286
58
  switch (d_sexprType) {
287
    case SEXPR_INTEGER:
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();
296
      return ss.str();
297
    }
298
58
    case SEXPR_STRING:
299
    case SEXPR_KEYWORD:
300
58
      return d_stringValue;
301
    case SEXPR_NOT_ATOM:
302
      return std::string();
303
  }
304
  return std::string();
305
}
306
307
24
const CVC4::Integer& SExpr::getIntegerValue() const {
308
24
  PrettyCheckArgument(isInteger(), this);
309
24
  return d_integerValue;
310
}
311
312
7
const CVC4::Rational& SExpr::getRationalValue() const {
313
7
  PrettyCheckArgument(isRational(), this);
314
7
  return d_rationalValue;
315
}
316
317
39
const std::vector<SExpr>& SExpr::getChildren() const {
318
39
  PrettyCheckArgument(!isAtom(), this);
319
39
  Assert(d_children != NULL);
320
39
  return *d_children;
321
}
322
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) {
328
      return true;
329
    } else if (d_children != NULL && s.d_children != NULL) {
330
      return getChildren() == s.getChildren();
331
    }
332
  }
333
  return false;
334
}
335
336
bool SExpr::operator!=(const SExpr& s) const { return !(*this == s); }
337
338
SExpr SExpr::parseAtom(const std::string& atom) {
339
  if (atom == "true") {
340
    return SExpr(true);
341
  } else if (atom == "false") {
342
    return SExpr(false);
343
  } else {
344
    try {
345
      Integer z(atom);
346
      return SExpr(z);
347
    } catch (std::invalid_argument&) {
348
      // Fall through to the next case
349
    }
350
    try {
351
      Rational q(atom);
352
      return SExpr(q);
353
    } catch (std::invalid_argument&) {
354
      // Fall through to the next case
355
    }
356
    return SExpr(atom);
357
  }
358
}
359
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));
365
  }
366
  return SExpr(parsedAtoms);
367
}
368
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();
374
       i != i_end; ++i) {
375
    parsedListsOfAtoms.push_back(parseListOfAtoms(*i));
376
  }
377
  return SExpr(parsedListsOfAtoms);
378
}
379
380
26685
} /* CVC4 namespace */