diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-06 22:06:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-06 22:06:52 +0000 |
commit | 7237456b4e2e5a119feacf98f52ec9e55d7a62a5 (patch) | |
tree | ea510f4987dadcdbbb361684445419e4939cdf00 /src/util/sexpr.h | |
parent | 6a5fb6d945b109921cb9b6117f4ede0b6d110c08 (diff) |
* Fix ITEs and functions in CVC language printer.
* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF
internally, except in strict mode).
* SExpr atoms now can be string-, integer-, or rational-valued.
* SmtEngine::setInfo(":status", ...) now properly dumps a
SetBenchmarkStatusCommand rather than a SetInfoCommand.
* Some dumping fixes (resolves bug 313)
Diffstat (limited to 'src/util/sexpr.h')
-rw-r--r-- | src/util/sexpr.h | 110 |
1 files changed, 100 insertions, 10 deletions
diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 63ce23874..005d9411d 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -34,8 +34,18 @@ namespace CVC4 { */ class CVC4_PUBLIC SExpr { - /** Flag telling us if this is an atom or a list. */ - bool d_isAtom; + enum { + SEXPR_STRING, + SEXPR_INTEGER, + SEXPR_RATIONAL, + SEXPR_NOT_ATOM + } d_atomType; + + /** The value of an atomic integer-valued S-expression. */ + Integer d_integerValue; + + /** The value of an atomic rational-valued S-expression. */ + Rational d_rationalValue; /** The value of an atomic S-expression. */ std::string d_stringValue; @@ -45,22 +55,57 @@ class CVC4_PUBLIC SExpr { public: SExpr() : - d_isAtom(true) { + d_atomType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(const Integer& value) : + d_atomType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(const Rational& value) : + d_atomType(SEXPR_RATIONAL), + d_integerValue(0), + d_rationalValue(value), + d_stringValue(""), + d_children() { } SExpr(const std::string& value) : - d_isAtom(true), - d_stringValue(value) { + d_atomType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children() { } SExpr(const std::vector<SExpr> children) : - d_isAtom(false), + d_atomType(SEXPR_NOT_ATOM), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), d_children(children) { } /** Is this S-expression an atom? */ bool isAtom() const; + /** Is this S-expression an integer? */ + bool isInteger() const; + + /** Is this S-expression a rational? */ + bool isRational() const; + + /** Is this S-expression a string? */ + bool isString() const; + /** * Get the string value of this S-expression. This will cause an * error if this S-expression is not an atom. @@ -68,23 +113,68 @@ public: const std::string getValue() const; /** + * Get the integer value of this S-expression. This will cause an + * error if this S-expression is not an integer. + */ + const Integer& getIntegerValue() const; + + /** + * Get the rational value of this S-expression. This will cause an + * error if this S-expression is not a rational. + */ + const Rational& getRationalValue() const; + + /** * Get the children of this S-expression. This will cause an error * if this S-expression is not a list. */ const std::vector<SExpr> getChildren() const; -}; + +};/* class SExpr */ inline bool SExpr::isAtom() const { - return d_isAtom; + return d_atomType != SEXPR_NOT_ATOM; +} + +inline bool SExpr::isInteger() const { + return d_atomType == SEXPR_INTEGER; +} + +inline bool SExpr::isRational() const { + return d_atomType == SEXPR_RATIONAL; +} + +inline bool SExpr::isString() const { + return d_atomType == SEXPR_STRING; } inline const std::string SExpr::getValue() const { - AlwaysAssert( d_isAtom ); + AlwaysAssert( isAtom() ); + switch(d_atomType) { + case SEXPR_INTEGER: + return d_integerValue.toString(); + case SEXPR_RATIONAL: + return d_rationalValue.toString(); + case SEXPR_STRING: + return d_stringValue; + default: + Unhandled(d_atomType); + } return d_stringValue; } +inline const Integer& SExpr::getIntegerValue() const { + AlwaysAssert( isInteger() ); + return d_integerValue; +} + +inline const Rational& SExpr::getRationalValue() const { + AlwaysAssert( isRational() ); + return d_rationalValue; +} + inline const std::vector<SExpr> SExpr::getChildren() const { - AlwaysAssert( !d_isAtom ); + AlwaysAssert( !isAtom() ); return d_children; } |