cvc4-1.3
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
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
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
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