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) {
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);
std::string toString(int base=10) const
bool isRational() const
Is this S-expression a rational?
SExpr(const std::vector< SExpr > &children)
SExpr(bool value)
This adds a convenience wrapper to SExpr to cast from bools.
bool isString() const
Is this S-expression a string?
A multi-precision rational constant.
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
bool isKeyword() const
Is this S-expression a keyword?
CVC4's exception base class and some associated utilities.
const CVC4::Integer & getIntegerValue() const
Get the integer value of this S-expression.
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
SExpr(const char *value)
This constructs a string expression from a const char* value.
bool isAtom() const
Is this S-expression an atom?
const std::string & getString() const
std::string getValue() const
Get the string value of this S-expression.
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)
bool operator==(const SExpr &s) const
Is this S-expression equal to another?
SExpr(const Keyword &value)
SExprKeyword(const std::string &s)
SExpr(unsigned long int value)
std::ostream & operator<<(std::ostream &out, ModelFormatMode mode)
struct CVC4::options::out__option_t out
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)
bool isInteger() const
Is this S-expression an integer?
const std::vector< SExpr > & getChildren() const
Get the children of this S-expression.
bool operator!=(const SExpr &s) const
Is this S-expression different from another?