summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/datatype.cpp9
-rw-r--r--src/expr/emptyset.cpp60
-rw-r--r--src/expr/emptyset.h63
-rw-r--r--src/expr/expr_template.cpp1
-rw-r--r--src/expr/expr_template.h104
-rw-r--r--src/expr/node.h3
-rw-r--r--src/expr/sexpr.cpp188
-rw-r--r--src/expr/sexpr.h169
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. */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback