diff options
author | Tim King <taking@google.com> | 2015-12-18 17:19:07 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-18 17:19:07 -0800 |
commit | 5f207ba01302c3245e169bfbe2ed91ad0cd659cd (patch) | |
tree | e1131e8c2891e283ab028fba6a7a677bb4ac9f5f /src/expr | |
parent | 7e4468ba0aa0b08eeb4ba1a86b1fdd839ae169d6 (diff) |
Modifying emptyset.h and sexpr. Adding SetLanguage.
- Modifies expr/emptyset.h to use SetType only as an incomplete type within expr/emptyset.h. This breaks the include cycle between expr/emptyset.h, expr/expr.h and expr/type.h.
- Refactors SExpr to avoid a potentially infinite cycle. This is likely overkill, but it works.
- Moving Expr::setlanguage and related utilities out of the Expr class and into their own file. This allows files in util/ to know the output language set on an ostream.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.cpp | 9 | ||||
-rw-r--r-- | src/expr/emptyset.cpp | 60 | ||||
-rw-r--r-- | src/expr/emptyset.h | 63 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 1 | ||||
-rw-r--r-- | src/expr/expr_template.h | 104 | ||||
-rw-r--r-- | src/expr/node.h | 3 | ||||
-rw-r--r-- | src/expr/sexpr.cpp | 188 | ||||
-rw-r--r-- | src/expr/sexpr.h | 169 |
8 files changed, 319 insertions, 278 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index c758fe297..09fe2cdc3 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -27,6 +27,7 @@ #include "expr/node.h" #include "expr/node_manager.h" #include "expr/type.h" +#include "options/set_language.h" using namespace std; @@ -934,7 +935,7 @@ std::string DatatypeConstructorArg::getTypeName() const { // Unfortunately, in the case of complex selector types, we can // enter nontrivial recursion here. Make sure that doesn't happen. stringstream ss; - ss << Expr::setlanguage(language::output::LANG_CVC4); + ss << language::SetLanguage(language::output::LANG_CVC4); ss.iword(s_printDatatypeNamesOnly) = 1; t.toStream(ss); return ss.str(); @@ -961,7 +962,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { Debug("datatypes-output") << "printNameOnly is now " << printNameOnly << std::endl; // can only output datatypes in the CVC4 native language - Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); os << "DATATYPE " << dt.getName(); if(dt.isParametric()) { @@ -992,7 +993,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) { // can only output datatypes in the CVC4 native language - Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); os << ctor.getName(); @@ -1013,7 +1014,7 @@ std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) { std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) { // can only output datatypes in the CVC4 native language - Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); os << arg.getName() << ": " << arg.getTypeName(); diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp index 69e34b848..a6e2c1ece 100644 --- a/src/expr/emptyset.cpp +++ b/src/expr/emptyset.cpp @@ -17,7 +17,10 @@ #include "expr/emptyset.h" -#include <iostream> +#include <iosfwd> + +#include "expr/expr.h" +#include "expr/type.h" namespace CVC4 { @@ -25,4 +28,59 @@ std::ostream& operator<<(std::ostream& out, const EmptySet& asa) { return out << "emptyset(" << asa.getType() << ')'; } +size_t EmptySetHashFunction::operator()(const EmptySet& es) const { + return TypeHashFunction()(es.getType()); +} + +/** + * Constructs an emptyset of the specified type. Note that the argument + * is the type of the set itself, NOT the type of the elements. + */ +EmptySet::EmptySet(const SetType& setType) + : d_type(new SetType(setType)) +{ } + +EmptySet::EmptySet(const EmptySet& es) + : d_type(new SetType(es.getType())) +{ } + +EmptySet& EmptySet::operator=(const EmptySet& es) { + (*d_type) = es.getType(); + return *this; +} + + +EmptySet::~EmptySet() throw() { + delete d_type; +} + +const SetType& EmptySet::getType() const { + return *d_type; +} + +bool EmptySet::operator==(const EmptySet& es) const throw() { + return getType() == es.getType(); +} + +bool EmptySet::operator!=(const EmptySet& es) const throw() { + return !(*this == es); +} + +bool EmptySet::operator<(const EmptySet& es) const throw() { + return getType() < es.getType(); +} + +bool EmptySet::operator<=(const EmptySet& es) const throw() { + return getType() <= es.getType(); +} + +bool EmptySet::operator>(const EmptySet& es) const throw() { + return !(*this <= es); +} + +bool EmptySet::operator>=(const EmptySet& es) const throw() { + return !(*this < es); +} + + }/* CVC4 namespace */ diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h index 4b3bb204f..e5eada731 100644 --- a/src/expr/emptyset.h +++ b/src/expr/emptyset.h @@ -19,65 +19,50 @@ #pragma once +#include <iosfwd> + namespace CVC4 { // messy; Expr needs EmptySet (because it's the payload of a - // CONSTANT-kinded expression), and EmptySet needs Expr. - class CVC4_PUBLIC EmptySet; + // CONSTANT-kinded expression), EmptySet needs SetType, and + // SetType needs Expr. Using a forward declaration here in + // order to break the build cycle. + // Uses of SetType need to be as an incomplete type throughout + // this header. + class CVC4_PUBLIC SetType; }/* CVC4 namespace */ -#include "expr/expr.h" -#include "expr/type.h" -#include <iostream> - namespace CVC4 { - class CVC4_PUBLIC EmptySet { - - const SetType d_type; - - EmptySet() { } public: - /** * Constructs an emptyset of the specified type. Note that the argument * is the type of the set itself, NOT the type of the elements. */ - EmptySet(SetType setType):d_type(setType) { } - - - ~EmptySet() throw() { - } + EmptySet(const SetType& setType); + ~EmptySet() throw(); + EmptySet(const EmptySet& other); + EmptySet& operator=(const EmptySet& other); - SetType getType() const { return d_type; } + const SetType& getType() const; + bool operator==(const EmptySet& es) const throw(); + bool operator!=(const EmptySet& es) const throw(); + bool operator<(const EmptySet& es) const throw(); + bool operator<=(const EmptySet& es) const throw(); + bool operator>(const EmptySet& es) const throw() ; + bool operator>=(const EmptySet& es) const throw(); - bool operator==(const EmptySet& es) const throw() { - return d_type == es.d_type; - } - bool operator!=(const EmptySet& es) const throw() { - return !(*this == es); - } +private: + /** Pointer to the SetType node. This is never NULL. */ + SetType* d_type; - bool operator<(const EmptySet& es) const throw() { - return d_type < es.d_type; - } - bool operator<=(const EmptySet& es) const throw() { - return d_type <= es.d_type; - } - bool operator>(const EmptySet& es) const throw() { - return !(*this <= es); - } - bool operator>=(const EmptySet& es) const throw() { - return !(*this < es); - } + EmptySet(); };/* class EmptySet */ std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC; struct CVC4_PUBLIC EmptySetHashFunction { - inline size_t operator()(const EmptySet& es) const { - return TypeHashFunction()(es.getType()); - } + size_t operator()(const EmptySet& es) const; };/* struct EmptySetHashFunction */ }/* CVC4 namespace */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 0739e3355..dbd7c049b 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -45,7 +45,6 @@ namespace expr { const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc(); const int ExprDag::s_iosIndex = std::ios_base::xalloc(); -const int ExprSetLanguage::s_iosIndex = std::ios_base::xalloc(); }/* CVC4::expr namespace */ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index f609d8990..2e2f17742 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -80,7 +80,6 @@ namespace expr { class CVC4_PUBLIC ExprSetDepth; class CVC4_PUBLIC ExprPrintTypes; class CVC4_PUBLIC ExprDag; - class CVC4_PUBLIC ExprSetLanguage; class ExportPrivate; }/* CVC4::expr namespace */ @@ -550,11 +549,6 @@ public: typedef expr::ExprDag dag; /** - * IOStream manipulator to set the output language for Exprs. - */ - typedef expr::ExprSetLanguage setlanguage; - - /** * Very basic pretty printer for Expr. * This is equivalent to calling e.getNode().printAst(...) * @param out output stream to print to. @@ -847,90 +841,6 @@ public: };/* class ExprDag::Scope */ };/* class ExprDag */ - -/** - * IOStream manipulator to set the output language for Exprs. - */ -class CVC4_PUBLIC ExprSetLanguage { - /** - * The allocated index in ios_base for our depth setting. - */ - static const int s_iosIndex; - - /** - * The default language to use, for ostreams that haven't yet had a - * setlanguage() applied to them and where the current Options - * information isn't available. - */ - static const int s_defaultOutputLanguage = language::output::LANG_AUTO; - - /** - * When this manipulator is used, the setting is stored here. - */ - OutputLanguage d_language; - -public: - /** - * Construct a ExprSetLanguage with the given setting. - */ - ExprSetLanguage(OutputLanguage l) : d_language(l) {} - - inline void applyLanguage(std::ostream& out) { - // (offset by one to detect whether default has been set yet) - out.iword(s_iosIndex) = int(d_language) + 1; - } - - static inline OutputLanguage getLanguage(std::ostream& out) { - long& l = out.iword(s_iosIndex); - if(l == 0) { - // set the default language on this ostream - // (offset by one to detect whether default has been set yet) - if(not Options::isCurrentNull()) { - l = options::outputLanguage() + 1; - } - if(l <= 0 || l > language::output::LANG_MAX) { - // if called from outside the library, we may not have options - // available to us at this point (or perhaps the output language - // is not set in Options). Default to something reasonable, but - // don't set "l" since that would make it "sticky" for this - // stream. - return OutputLanguage(s_defaultOutputLanguage); - } - } - return OutputLanguage(l - 1); - } - - static inline void setLanguage(std::ostream& out, OutputLanguage l) { - // (offset by one to detect whether default has been set yet) - out.iword(s_iosIndex) = int(l) + 1; - } - - /** - * Set a language on the output stream for the current stack scope. - * This makes sure the old language is reset on the stream after - * normal OR exceptional exit from the scope, using the RAII C++ - * idiom. - */ - class Scope { - std::ostream& d_out; - OutputLanguage d_oldLanguage; - - public: - - inline Scope(std::ostream& out, OutputLanguage language) : - d_out(out), - d_oldLanguage(ExprSetLanguage::getLanguage(out)) { - ExprSetLanguage::setLanguage(out, language); - } - - inline ~Scope() { - ExprSetLanguage::setLanguage(d_out, d_oldLanguage); - } - - };/* class ExprSetLanguage::Scope */ - -};/* class ExprSetLanguage */ - }/* CVC4::expr namespace */ ${getConst_instantiations} @@ -981,20 +891,6 @@ inline std::ostream& operator<<(std::ostream& out, ExprDag d) { return out; } -/** - * Sets the output language when pretty-printing a Expr to an ostream. - * Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl; - * - * The setting stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) { - l.applyLanguage(out); - return out; -} - }/* CVC4::expr namespace */ inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { diff --git a/src/expr/node.h b/src/expr/node.h index 384dbcc03..f345ba552 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -38,6 +38,7 @@ #include "expr/metakind.h" #include "expr/expr.h" #include "options/language.h" +#include "options/set_language.h" #include "util/configuration.h" #include "util/utility.h" #include "util/hash.h" @@ -864,7 +865,7 @@ public: /** * IOStream manipulator to set the output language for Exprs. */ - typedef expr::ExprSetLanguage setlanguage; + typedef language::SetLanguage setlanguage; /** * Very basic pretty printer for Node. diff --git a/src/expr/sexpr.cpp b/src/expr/sexpr.cpp index b8ffca5e5..0c0828616 100644 --- a/src/expr/sexpr.cpp +++ b/src/expr/sexpr.cpp @@ -30,6 +30,7 @@ #include "base/cvc4_assert.h" #include "expr/expr.h" +#include "options/set_language.h" #include "util/smt2_quote_string.h" @@ -42,13 +43,151 @@ std::ostream& operator<<(std::ostream& out, PrettySExprs ps) { return out; } + +SExpr::~SExpr() { + if(d_children != NULL){ + delete d_children; + d_children = NULL; + } + Assert(d_children == NULL); +} + +SExpr& SExpr::operator=(const SExpr& other) { + d_sexprType = other.d_sexprType; + d_integerValue = other.d_integerValue; + d_rationalValue = other.d_rationalValue; + d_stringValue = other.d_stringValue; + + if(d_children == NULL && other.d_children == NULL){ + // Do nothing. + } else if(d_children == NULL){ + d_children = new SExprVector(*other.d_children); + } else if(other.d_children == NULL){ + delete d_children; + d_children = NULL; + } else { + (*d_children) = other.getChildren(); + } + Assert( isAtom() == other.isAtom() ); + Assert( (d_children == NULL) == isAtom() ); + return *this; +} + +SExpr::SExpr() : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { +} + + +SExpr::SExpr(const SExpr& other) : + d_sexprType(other.d_sexprType), + d_integerValue(other.d_integerValue), + d_rationalValue(other.d_rationalValue), + d_stringValue(other.d_stringValue), + d_children(NULL) +{ + d_children = (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children); + // d_children being NULL is equivalent to the node being an atom. + Assert( (d_children == NULL) == isAtom() ); +} + + +SExpr::SExpr(const CVC4::Integer& value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { + } + +SExpr::SExpr(int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { +} + +SExpr::SExpr(long int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { +} + +SExpr::SExpr(unsigned int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { +} + +SExpr::SExpr(unsigned long int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { +} + +SExpr::SExpr(const CVC4::Rational& value) : + d_sexprType(SEXPR_RATIONAL), + d_integerValue(0), + d_rationalValue(value), + d_stringValue(""), + d_children(NULL) { +} + +SExpr::SExpr(const std::string& value) : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children(NULL) { +} + + /** + * This constructs a string expression from a const char* value. + * This cannot be removed in order to support SExpr("foo"). + * Given the other constructors this SExpr("foo") converts to bool. + * instead of SExpr(string("foo")). + */ +SExpr::SExpr(const char* value) : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children(NULL) { +} + #warning "TODO: Discuss this change with Clark." SExpr::SExpr(bool value) : d_sexprType(SEXPR_KEYWORD), d_integerValue(0), d_rationalValue(0), d_stringValue(value ? "true" : "false"), - d_children() { + d_children(NULL) { +} + +SExpr::SExpr(const Keyword& value) : + d_sexprType(SEXPR_KEYWORD), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value.getString()), + d_children(NULL) { +} + +SExpr::SExpr(const std::vector<SExpr>& children) : + d_sexprType(SEXPR_NOT_ATOM), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children(new SExprVector(children)) { } std::string SExpr::toString() const { @@ -57,13 +196,39 @@ std::string SExpr::toString() const { return ss.str(); } +/** Is this S-expression an atom? */ +bool SExpr::isAtom() const { + return d_sexprType != SEXPR_NOT_ATOM; +} + +/** Is this S-expression an integer? */ +bool SExpr::isInteger() const { + return d_sexprType == SEXPR_INTEGER; +} + +/** Is this S-expression a rational? */ +bool SExpr::isRational() const { + return d_sexprType == SEXPR_RATIONAL; +} + +/** Is this S-expression a string? */ +bool SExpr::isString() const { + return d_sexprType == SEXPR_STRING; +} + +/** Is this S-expression a keyword? */ +bool SExpr::isKeyword() const { + return d_sexprType == SEXPR_KEYWORD; +} + + std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) { SExpr::toStream(out, sexpr); return out; } void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() { - toStream(out, sexpr, Expr::setlanguage::getLanguage(out)); + toStream(out, sexpr, language::SetLanguage::getLanguage(out)); } void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() { @@ -181,15 +346,22 @@ const CVC4::Rational& SExpr::getRationalValue() const { const std::vector<SExpr>& SExpr::getChildren() const { CheckArgument( !isAtom(), this ); - return d_children; + Assert( d_children != NULL ); + return *d_children; } bool SExpr::operator==(const SExpr& s) const { - return d_sexprType == s.d_sexprType && - d_integerValue == s.d_integerValue && - d_rationalValue == s.d_rationalValue && - d_stringValue == s.d_stringValue && - d_children == s.d_children; + if (d_sexprType == s.d_sexprType && + d_integerValue == s.d_integerValue && + d_rationalValue == s.d_rationalValue && + d_stringValue == s.d_stringValue) { + if(d_children == NULL && s.d_children == NULL){ + return true; + } else if(d_children != NULL && s.d_children != NULL){ + return getChildren() == s.getChildren(); + } + } + return false; } bool SExpr::operator!=(const SExpr& s) const { diff --git a/src/expr/sexpr.h b/src/expr/sexpr.h index 158be0efb..40fd9dd56 100644 --- a/src/expr/sexpr.h +++ b/src/expr/sexpr.h @@ -27,7 +27,7 @@ #define __CVC4__SEXPR_H #include <iomanip> -#include <sstream> +#include <iosfwd> #include <string> #include <vector> @@ -50,94 +50,25 @@ public: * string value, or a list of other S-expressions. */ class CVC4_PUBLIC SExpr { - - enum SExprTypes { - SEXPR_STRING, - SEXPR_KEYWORD, - SEXPR_INTEGER, - SEXPR_RATIONAL, - SEXPR_NOT_ATOM - } d_sexprType; - - /** The value of an atomic integer-valued S-expression. */ - CVC4::Integer d_integerValue; - - /** The value of an atomic rational-valued S-expression. */ - CVC4::Rational d_rationalValue; - - /** The value of an atomic S-expression. */ - std::string d_stringValue; - - /** The children of a list S-expression. */ - std::vector<SExpr> d_children; - public: typedef SExprKeyword Keyword; - SExpr() : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } + SExpr(); + SExpr(const SExpr&); + SExpr& operator=(const SExpr& other); + ~SExpr(); - SExpr(const CVC4::Integer& value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } + SExpr(const CVC4::Integer& value); - SExpr(int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } + SExpr(int value); + SExpr(long int value); + SExpr(unsigned int value); + SExpr(unsigned long int value); - SExpr(long int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } + SExpr(const CVC4::Rational& value); - SExpr(unsigned int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } - - SExpr(unsigned long int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } - - SExpr(const CVC4::Rational& value) : - d_sexprType(SEXPR_RATIONAL), - d_integerValue(0), - d_rationalValue(value), - d_stringValue(""), - d_children() { - } - - SExpr(const std::string& value) : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value), - d_children() { - } + SExpr(const std::string& value); /** * This constructs a string expression from a const char* value. @@ -145,60 +76,30 @@ public: * Given the other constructors this SExpr("foo") converts to bool. * instead of SExpr(string("foo")). */ - SExpr(const char* value) : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value), - d_children() { - } + SExpr(const char* value); /** * This adds a convenience wrapper to SExpr to cast from bools. * This is internally handled as the strings "true" and "false" */ SExpr(bool value); - - SExpr(const Keyword& value) : - d_sexprType(SEXPR_KEYWORD), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value.getString()), - d_children() { - } - - SExpr(const std::vector<SExpr>& children) : - d_sexprType(SEXPR_NOT_ATOM), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(""), - d_children(children) { - } + SExpr(const Keyword& value); + SExpr(const std::vector<SExpr>& children); /** Is this S-expression an atom? */ - bool isAtom() const { - return d_sexprType != SEXPR_NOT_ATOM; - } + bool isAtom() const; /** Is this S-expression an integer? */ - bool isInteger() const { - return d_sexprType == SEXPR_INTEGER; - } + bool isInteger() const; /** Is this S-expression a rational? */ - bool isRational() const { - return d_sexprType == SEXPR_RATIONAL; - } + bool isRational() const; /** Is this S-expression a string? */ - bool isString() const { - return d_sexprType == SEXPR_STRING; - } + bool isString() const; /** Is this S-expression a keyword? */ - bool isKeyword() const { - return d_sexprType == SEXPR_KEYWORD; - } + bool isKeyword() const; /** * This wraps the toStream() printer. @@ -261,7 +162,7 @@ public: /** * Outputs the SExpr onto the ostream out. This version reads defaults to the - * OutputLanguage, Expr::setlanguage::getLanguage(out). The indent level is + * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level is * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise. */ static void toStream(std::ostream& out, const SExpr& sexpr) throw(); @@ -297,6 +198,34 @@ private: /** Returns true if this language quotes Keywords when printing. */ static bool languageQuotesKeywords(OutputLanguage language); + enum SExprTypes { + SEXPR_STRING, + SEXPR_KEYWORD, + SEXPR_INTEGER, + SEXPR_RATIONAL, + SEXPR_NOT_ATOM + } d_sexprType; + + /** The value of an atomic integer-valued S-expression. */ + CVC4::Integer d_integerValue; + + /** The value of an atomic rational-valued S-expression. */ + CVC4::Rational d_rationalValue; + + /** The value of an atomic S-expression. */ + std::string d_stringValue; + + typedef std::vector<SExpr> SExprVector; + + /** + * The children of a list S-expression. + * Whenever the SExpr isAtom() holds, this points at NULL. + * + * This should be a pointer in case the implementation of vector<SExpr> ever + * directly contained or allocated an SExpr. If this happened this would trigger, + * either the size being infinite or SExpr() being an infinite loop. + */ + SExprVector* d_children; };/* class SExpr */ /** Prints an SExpr. */ |