cvc4-1.4
sexpr.h
Go to the documentation of this file.
1 /********************* */
24 #include "cvc4_public.h"
25 
26 #ifndef __CVC4__SEXPR_H
27 #define __CVC4__SEXPR_H
28 
29 #include <vector>
30 #include <string>
31 #include <iomanip>
32 #include <sstream>
33 
34 #include "util/integer.h"
35 #include "util/rational.h"
36 #include "util/exception.h"
37 
38 namespace CVC4 {
39 
41  std::string d_str;
42 public:
43  SExprKeyword(const std::string& s) : d_str(s) {}
44  const std::string& getString() const { return d_str; }
45 };/* class SExpr::Keyword */
46 
52 
53  enum SExprTypes {
54  SEXPR_STRING,
55  SEXPR_KEYWORD,
56  SEXPR_INTEGER,
57  SEXPR_RATIONAL,
58  SEXPR_NOT_ATOM
59  } d_sexprType;
60 
62  CVC4::Integer d_integerValue;
63 
65  CVC4::Rational d_rationalValue;
66 
68  std::string d_stringValue;
69 
71  std::vector<SExpr> d_children;
72 
73 public:
74 
76 
77  SExpr() :
78  d_sexprType(SEXPR_STRING),
79  d_integerValue(0),
80  d_rationalValue(0),
81  d_stringValue(""),
82  d_children() {
83  }
84 
85  SExpr(const CVC4::Integer& value) :
86  d_sexprType(SEXPR_INTEGER),
87  d_integerValue(value),
88  d_rationalValue(0),
89  d_stringValue(""),
90  d_children() {
91  }
92 
93  SExpr(int value) :
94  d_sexprType(SEXPR_INTEGER),
95  d_integerValue(value),
96  d_rationalValue(0),
97  d_stringValue(""),
98  d_children() {
99  }
100 
101  SExpr(long int value) :
102  d_sexprType(SEXPR_INTEGER),
103  d_integerValue(value),
104  d_rationalValue(0),
105  d_stringValue(""),
106  d_children() {
107  }
108 
109  SExpr(unsigned int value) :
110  d_sexprType(SEXPR_INTEGER),
111  d_integerValue(value),
112  d_rationalValue(0),
113  d_stringValue(""),
114  d_children() {
115  }
116 
117  SExpr(unsigned long int value) :
118  d_sexprType(SEXPR_INTEGER),
119  d_integerValue(value),
120  d_rationalValue(0),
121  d_stringValue(""),
122  d_children() {
123  }
124 
125  SExpr(const CVC4::Rational& value) :
126  d_sexprType(SEXPR_RATIONAL),
127  d_integerValue(0),
128  d_rationalValue(value),
129  d_stringValue(""),
130  d_children() {
131  }
132 
133  SExpr(const std::string& value) :
134  d_sexprType(SEXPR_STRING),
135  d_integerValue(0),
136  d_rationalValue(0),
137  d_stringValue(value),
138  d_children() {
139  }
140 
147  SExpr(const char* value) :
148  d_sexprType(SEXPR_STRING),
149  d_integerValue(0),
150  d_rationalValue(0),
151  d_stringValue(value),
152  d_children() {
153  }
154 
159  SExpr(bool value) :
160  d_sexprType(SEXPR_STRING),
161  d_integerValue(0),
162  d_rationalValue(0),
163  d_stringValue(value ? "true" : "false"),
164  d_children() {
165  }
166 
167  SExpr(const Keyword& value) :
168  d_sexprType(SEXPR_KEYWORD),
169  d_integerValue(0),
170  d_rationalValue(0),
171  d_stringValue(value.getString()),
172  d_children() {
173  }
174 
175  SExpr(const std::vector<SExpr>& children) :
176  d_sexprType(SEXPR_NOT_ATOM),
177  d_integerValue(0),
178  d_rationalValue(0),
179  d_stringValue(""),
180  d_children(children) {
181  }
182 
184  bool isAtom() const;
185 
187  bool isInteger() const;
188 
190  bool isRational() const;
191 
193  bool isString() const;
194 
196  bool isKeyword() const;
197 
202  std::string getValue() const;
203 
208  const CVC4::Integer& getIntegerValue() const;
209 
214  const CVC4::Rational& getRationalValue() const;
215 
220  const std::vector<SExpr>& getChildren() const;
221 
223  bool operator==(const SExpr& s) const;
224 
226  bool operator!=(const SExpr& s) const;
227 
228 };/* class SExpr */
229 
230 inline bool SExpr::isAtom() const {
231  return d_sexprType != SEXPR_NOT_ATOM;
232 }
233 
234 inline bool SExpr::isInteger() const {
235  return d_sexprType == SEXPR_INTEGER;
236 }
237 
238 inline bool SExpr::isRational() const {
239  return d_sexprType == SEXPR_RATIONAL;
240 }
241 
242 inline bool SExpr::isString() const {
243  return d_sexprType == SEXPR_STRING;
244 }
245 
246 inline bool SExpr::isKeyword() const {
247  return d_sexprType == SEXPR_KEYWORD;
248 }
249 
250 inline std::string SExpr::getValue() const {
251  CheckArgument( isAtom(), this );
252  switch(d_sexprType) {
253  case SEXPR_INTEGER:
254  return d_integerValue.toString();
255  case SEXPR_RATIONAL: {
256  // We choose to represent rationals as decimal strings rather than
257  // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL
258  // could be added if we need both styles, even if it's backed by
259  // the same Rational object.
260  std::stringstream ss;
261  ss << std::fixed << d_rationalValue.getDouble();
262  return ss.str();
263  }
264  case SEXPR_STRING:
265  case SEXPR_KEYWORD:
266  return d_stringValue;
267  case SEXPR_NOT_ATOM:
268  return std::string();
269  }
270  return std::string();
271 }
272 
273 inline const CVC4::Integer& SExpr::getIntegerValue() const {
274  CheckArgument( isInteger(), this );
275  return d_integerValue;
276 }
277 
279  CheckArgument( isRational(), this );
280  return d_rationalValue;
281 }
282 
283 inline const std::vector<SExpr>& SExpr::getChildren() const {
284  CheckArgument( !isAtom(), this );
285  return d_children;
286 }
287 
288 inline bool SExpr::operator==(const SExpr& s) const {
289  return d_sexprType == s.d_sexprType &&
290  d_integerValue == s.d_integerValue &&
291  d_rationalValue == s.d_rationalValue &&
292  d_stringValue == s.d_stringValue &&
293  d_children == s.d_children;
294 }
295 
296 inline bool SExpr::operator!=(const SExpr& s) const {
297  return !(*this == s);
298 }
299 
300 std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC;
301 
302 }/* CVC4 namespace */
303 
304 #endif /* __CVC4__SEXPR_H */
std::string toString(int base=10) const
SExpr(long int value)
Definition: sexpr.h:101
Definition: input.h:32
bool isRational() const
Is this S-expression a rational?
Definition: sexpr.h:238
SExpr(const std::vector< SExpr > &children)
Definition: sexpr.h:175
SExpr(bool value)
This adds a convenience wrapper to SExpr to cast from bools.
Definition: sexpr.h:159
bool isString() const
Is this S-expression a string?
Definition: sexpr.h:242
A multi-precision rational constant.
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
bool isKeyword() const
Is this S-expression a keyword?
Definition: sexpr.h:246
SExprKeyword Keyword
Definition: sexpr.h:75
SExpr(int value)
Definition: sexpr.h:93
CVC4's exception base class and some associated utilities.
const CVC4::Integer & getIntegerValue() const
Get the integer value of this S-expression.
Definition: sexpr.h:273
SExpr(const char *value)
This constructs a string expression from a const char* value.
Definition: sexpr.h:147
SExpr()
Definition: sexpr.h:77
bool isAtom() const
Is this S-expression an atom?
Definition: sexpr.h:230
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
const std::string & getString() const
Definition: sexpr.h:44
std::string getValue() const
Get the string value of this S-expression.
Definition: sexpr.h:250
SExpr(const std::string &value)
Definition: sexpr.h:133
Macros that should be defined everywhere during the building of the libraries and driver binary...
SExpr(unsigned int value)
Definition: sexpr.h:109
const CVC4::Rational & getRationalValue() const
Get the rational value of this S-expression.
Definition: sexpr.h:278
SExpr(const CVC4::Integer &value)
Definition: sexpr.h:85
bool operator==(const SExpr &s) const
Is this S-expression equal to another?
Definition: sexpr.h:288
SExpr(const Keyword &value)
Definition: sexpr.h:167
SExprKeyword(const std::string &s)
Definition: sexpr.h:43
SExpr(unsigned long int value)
Definition: sexpr.h:117
struct CVC4::options::out__option_t out
std::ostream & operator<<(std::ostream &out, SimplificationMode mode)
A simple S-expression.
Definition: sexpr.h:51
bool operator!=(enum Result::Sat s, const Result &r)
bool operator==(enum Result::Sat s, const Result &r)
double getDouble() const
Get a double representation of this Rational, which is approximate: truncation may occur...
SExpr(const CVC4::Rational &value)
Definition: sexpr.h:125
bool isInteger() const
Is this S-expression an integer?
Definition: sexpr.h:234
const std::vector< SExpr > & getChildren() const
Get the children of this S-expression.
Definition: sexpr.h:283
bool operator!=(const SExpr &s) const
Is this S-expression different from another?
Definition: sexpr.h:296