26 #ifndef __CVC4__SEXPR_H 27 #define __CVC4__SEXPR_H 34 #include "util/integer.h" 35 #include "util/rational.h" 44 const std::string&
getString()
const {
return d_str; }
68 std::string d_stringValue;
71 std::vector<SExpr> d_children;
78 d_sexprType(SEXPR_STRING),
86 d_sexprType(SEXPR_INTEGER),
87 d_integerValue(value),
94 d_sexprType(SEXPR_INTEGER),
95 d_integerValue(value),
102 d_sexprType(SEXPR_INTEGER),
103 d_integerValue(value),
110 d_sexprType(SEXPR_INTEGER),
111 d_integerValue(value),
118 d_sexprType(SEXPR_INTEGER),
119 d_integerValue(value),
126 d_sexprType(SEXPR_RATIONAL),
128 d_rationalValue(value),
134 d_sexprType(SEXPR_STRING),
137 d_stringValue(value),
148 d_sexprType(SEXPR_STRING),
151 d_stringValue(value),
160 d_sexprType(SEXPR_STRING),
163 d_stringValue(value ?
"true" :
"false"),
168 d_sexprType(SEXPR_KEYWORD),
171 d_stringValue(value.getString()),
175 SExpr(
const std::vector<SExpr>& children) :
176 d_sexprType(SEXPR_NOT_ATOM),
180 d_children(children) {
187 bool isInteger()
const;
190 bool isRational()
const;
193 bool isString()
const;
196 bool isKeyword()
const;
202 std::string getValue()
const;
220 const std::vector<SExpr>& getChildren()
const;
231 return d_sexprType != SEXPR_NOT_ATOM;
235 return d_sexprType == SEXPR_INTEGER;
239 return d_sexprType == SEXPR_RATIONAL;
243 return d_sexprType == SEXPR_STRING;
247 return d_sexprType == SEXPR_KEYWORD;
252 switch(d_sexprType) {
254 return d_integerValue.toString();
255 case SEXPR_RATIONAL: {
260 std::stringstream ss;
261 ss << std::fixed << d_rationalValue.getDouble();
266 return d_stringValue;
268 return std::string();
270 return std::string();
275 return d_integerValue;
280 return d_rationalValue;
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;
297 return !(*
this == s);
bool isAtom() const
Is this S-expression an atom?
SExpr(const std::vector< SExpr > &children)
bool operator!=(const SExpr &s) const
Is this S-expression different from another?
SExpr(bool value)
This adds a convenience wrapper to SExpr to cast from bools.
std::string getValue() const
Get the string value of this S-expression.
A multi-precision rational constant.
const std::string & getString() const
bool isRational() const
Is this S-expression a rational?
std::ostream & operator<<(std::ostream &, const Command &)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
CVC4's exception base class and some associated utilities.
SExpr(const char *value)
This constructs a string expression from a const char* value.
const CVC4::Integer & getIntegerValue() const
Get the integer value of this S-expression.
bool isInteger() const
Is this S-expression an integer?
bool isKeyword() const
Is this S-expression a keyword?
SExpr(const std::string &value)
Macros that should be defined everywhere during the building of the libraries and driver binary...
SExpr(unsigned int value)
const CVC4::Rational & getRationalValue() const
Get the rational value of this S-expression.
SExpr(const CVC4::Integer &value)
SExpr(const Keyword &value)
SExprKeyword(const std::string &s)
SExpr(unsigned long int value)
bool operator==(const SExpr &s) const
Is this S-expression equal to another?
struct CVC4::options::out__option_t out
const std::vector< SExpr > & getChildren() const
Get the children of this S-expression.
bool operator!=(enum Result::Sat s, const Result &r)
bool operator==(enum Result::Sat s, const Result &r)
SExpr(const CVC4::Rational &value)
bool isString() const
Is this S-expression a string?