GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/sexpr.h Lines: 5 8 62.5 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sexpr.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Morgan Deters, Christopher L. Conway
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
 ** These are used when a simple, and obvious interface for basic
16
 ** expressions is appropriate.
17
 **
18
 ** These are quite ineffecient.
19
 ** These are totally disconnected from any ExprManager.
20
 ** These keep unique copies of all of their children.
21
 ** These are VERY overly verbose and keep much more data than is needed.
22
 **/
23
24
#include "cvc4_public.h"
25
26
#ifndef CVC4__SEXPR_H
27
#define CVC4__SEXPR_H
28
29
#include <iosfwd>
30
#include <string>
31
#include <vector>
32
33
#include "cvc4_export.h"
34
#include "options/language.h"
35
#include "util/integer.h"
36
#include "util/rational.h"
37
38
namespace CVC4 {
39
40
8
class SExprKeyword
41
{
42
 public:
43
8
  SExprKeyword(const std::string& s) : d_str(s) {}
44
8
  const std::string& getString() const { return d_str; }
45
46
 private:
47
  std::string d_str;
48
}; /* class SExpr::Keyword */
49
50
/**
51
 * A simple S-expression. An S-expression is either an atom with a
52
 * string value, or a list of other S-expressions.
53
 */
54
class CVC4_EXPORT SExpr
55
{
56
 public:
57
  typedef SExprKeyword Keyword;
58
59
  SExpr();
60
  SExpr(const SExpr&);
61
  SExpr& operator=(const SExpr& other);
62
  ~SExpr();
63
64
  SExpr(const CVC4::Integer& value);
65
66
  SExpr(int value);
67
  SExpr(long int value);
68
  SExpr(unsigned int value);
69
  SExpr(unsigned long int value);
70
71
  SExpr(const CVC4::Rational& value);
72
73
  SExpr(const std::string& value);
74
75
  /**
76
   * This constructs a string expression from a const char* value.
77
   * This cannot be removed in order to support SExpr("foo").
78
   * Given the other constructors this SExpr("foo") converts to bool.
79
   * instead of SExpr(string("foo")).
80
   */
81
  SExpr(const char* value);
82
83
  /**
84
   * This adds a convenience wrapper to SExpr to cast from bools.
85
   * This is internally handled as the strings "true" and "false"
86
   */
87
  SExpr(bool value);
88
  SExpr(const Keyword& value);
89
  SExpr(const std::vector<SExpr>& children);
90
91
  /** Is this S-expression an atom? */
92
  bool isAtom() const;
93
94
  /** Is this S-expression an integer? */
95
  bool isInteger() const;
96
97
  /** Is this S-expression a rational? */
98
  bool isRational() const;
99
100
  /** Is this S-expression a string? */
101
  bool isString() const;
102
103
  /** Is this S-expression a keyword? */
104
  bool isKeyword() const;
105
106
  /**
107
   * This wraps the toStream() printer.
108
   * NOTE: toString() and getValue() may differ on Keywords based on
109
   * the current language set in expr.
110
   */
111
  std::string toString() const;
112
113
  /**
114
   * Get the string value of this S-expression. This will cause an
115
   * error if this S-expression is not an atom.
116
   */
117
  std::string getValue() const;
118
119
  /**
120
   * Get the integer value of this S-expression. This will cause an
121
   * error if this S-expression is not an integer.
122
   */
123
  const CVC4::Integer& getIntegerValue() const;
124
125
  /**
126
   * Get the rational value of this S-expression. This will cause an
127
   * error if this S-expression is not a rational.
128
   */
129
  const CVC4::Rational& getRationalValue() const;
130
131
  /**
132
   * Get the children of this S-expression. This will cause an error
133
   * if this S-expression is not a list.
134
   */
135
  const std::vector<SExpr>& getChildren() const;
136
137
  /** Is this S-expression equal to another? */
138
  bool operator==(const SExpr& s) const;
139
140
  /** Is this S-expression different from another? */
141
  bool operator!=(const SExpr& s) const;
142
143
  /**
144
   * This returns the best match in the following order:
145
   * match atom with
146
   *  "true", "false" -> SExpr(value)
147
   * | is and integer -> as integer
148
   * | is a rational -> as rational
149
   * | _ -> SExpr()
150
   */
151
  static SExpr parseAtom(const std::string& atom);
152
153
  /**
154
   * Parses a list of atoms.
155
   */
156
  static SExpr parseListOfAtoms(const std::vector<std::string>& atoms);
157
158
  /**
159
   * Parses a list of list of atoms.
160
   */
161
  static SExpr parseListOfListOfAtoms(
162
      const std::vector<std::vector<std::string> >& atoms_lists);
163
164
  /**
165
   * Outputs the SExpr onto the ostream out. This version reads defaults to the
166
   * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level
167
   * is
168
   * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise.
169
   */
170
  static void toStream(std::ostream& out, const SExpr& sexpr);
171
172
  /**
173
   * Outputs the SExpr onto the ostream out. This version sets the indent level
174
   * to 2 if PrettySExprs::getPrettySExprs() is on.
175
   */
176
  static void toStream(std::ostream& out, const SExpr& sexpr,
177
                       OutputLanguage language);
178
179
  /**
180
   * Outputs the SExpr onto the ostream out.
181
   * If the languageQuotesKeywords(language), then a top level keyword, " X",
182
   * that needs quoting according to the SMT2 language standard is printed with
183
   * quotes, "| X|".
184
   * Otherwise this prints using toStreamRec().
185
   *
186
   * TIM: Keywords that are children are not currently quoted. This seems
187
   * incorrect but I am just reproduicing the old behavior even if it does not
188
   * make
189
   * sense.
190
   */
191
  static void toStream(std::ostream& out, const SExpr& sexpr,
192
                       OutputLanguage language, int indent);
193
194
 private:
195
  /**
196
   * Simple printer for SExpr to an ostream.
197
   * The current implementation is language independent.
198
   */
199
  static void toStreamRec(std::ostream& out, const SExpr& sexpr,
200
                          OutputLanguage language, int indent);
201
202
  /** Returns true if this language quotes Keywords when printing. */
203
  static bool languageQuotesKeywords(OutputLanguage language);
204
205
  enum SExprTypes {
206
    SEXPR_STRING,
207
    SEXPR_KEYWORD,
208
    SEXPR_INTEGER,
209
    SEXPR_RATIONAL,
210
    SEXPR_NOT_ATOM
211
  } d_sexprType;
212
213
  /** The value of an atomic integer-valued S-expression. */
214
  CVC4::Integer d_integerValue;
215
216
  /** The value of an atomic rational-valued S-expression. */
217
  CVC4::Rational d_rationalValue;
218
219
  /** The value of an atomic S-expression. */
220
  std::string d_stringValue;
221
222
  typedef std::vector<SExpr> SExprVector;
223
224
  /**
225
   * The children of a list S-expression.
226
   * Whenever the SExpr isAtom() holds, this points at NULL.
227
   *
228
   * This should be a pointer in case the implementation of vector<SExpr> ever
229
   * directly contained or allocated an SExpr. If this happened this would
230
   * trigger,
231
   * either the size being infinite or SExpr() being an infinite loop.
232
   */
233
  SExprVector* d_children;
234
}; /* class SExpr */
235
236
/** Prints an SExpr. */
237
std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_EXPORT;
238
239
/**
240
 * IOStream manipulator to pretty-print SExprs.
241
 */
242
class CVC4_EXPORT PrettySExprs
243
{
244
  /**
245
   * The allocated index in ios_base for our setting.
246
   */
247
  static const int s_iosIndex;
248
249
  /**
250
   * When this manipulator is used, the setting is stored here.
251
   */
252
  bool d_prettySExprs;
253
254
 public:
255
  /**
256
   * Construct a PrettySExprs with the given setting.
257
   */
258
  PrettySExprs(bool prettySExprs) : d_prettySExprs(prettySExprs) {}
259
260
  inline void applyPrettySExprs(std::ostream& out) {
261
    out.iword(s_iosIndex) = d_prettySExprs;
262
  }
263
264
14
  static inline bool getPrettySExprs(std::ostream& out) {
265
14
    return out.iword(s_iosIndex);
266
  }
267
268
  static inline void setPrettySExprs(std::ostream& out, bool prettySExprs) {
269
    out.iword(s_iosIndex) = prettySExprs;
270
  }
271
272
  /**
273
   * Set the pretty-sexprs state on the output stream for the current
274
   * stack scope.  This makes sure the old state is reset on the
275
   * stream after normal OR exceptional exit from the scope, using the
276
   * RAII C++ idiom.
277
   */
278
  class Scope {
279
    std::ostream& d_out;
280
    bool d_oldPrettySExprs;
281
282
   public:
283
    inline Scope(std::ostream& out, bool prettySExprs)
284
        : d_out(out), d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) {
285
      PrettySExprs::setPrettySExprs(out, prettySExprs);
286
    }
287
288
    inline ~Scope() { PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); }
289
290
  }; /* class PrettySExprs::Scope */
291
292
}; /* class PrettySExprs */
293
294
/**
295
 * Sets the default pretty-sexprs setting for an ostream.  Use like this:
296
 *
297
 *   // let out be an ostream, s an SExpr
298
 *   out << PrettySExprs(true) << s << endl;
299
 *
300
 * The setting stays permanently (until set again) with the stream.
301
 */
302
std::ostream& operator<<(std::ostream& out, PrettySExprs ps);
303
304
} /* CVC4 namespace */
305
306
#endif /* CVC4__SEXPR_H */