diff options
Diffstat (limited to 'src/util/sexpr.h')
-rw-r--r-- | src/util/sexpr.h | 304 |
1 files changed, 0 insertions, 304 deletions
diff --git a/src/util/sexpr.h b/src/util/sexpr.h deleted file mode 100644 index a121b5195..000000000 --- a/src/util/sexpr.h +++ /dev/null @@ -1,304 +0,0 @@ -/********************* */ -/*! \file sexpr.h - ** \verbatim - ** Original author: Christopher L. Conway - ** Major contributors: Tim King, Morgan Deters - ** Minor contributors (to current version): Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Simple representation of S-expressions - ** - ** Simple representation of S-expressions. - ** These are used when a simple, and obvious interface for basic - ** expressions is appropraite. - ** - ** These are quite ineffecient. - ** These are totally disconnected from any ExprManager. - ** These keep unique copies of all of their children. - ** These are VERY overly verbose and keep much more data than is needed. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__SEXPR_H -#define __CVC4__SEXPR_H - -#include <vector> -#include <string> -#include <iomanip> -#include <sstream> - -#include "util/integer.h" -#include "util/rational.h" -#include "util/exception.h" - -namespace CVC4 { - -class CVC4_PUBLIC SExprKeyword { - std::string d_str; -public: - SExprKeyword(const std::string& s) : d_str(s) {} - const std::string& getString() const { return d_str; } -};/* class SExpr::Keyword */ - -/** - * A simple S-expression. An S-expression is either an atom with a - * 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(const CVC4::Integer& value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } - - SExpr(int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } - - SExpr(long int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } - - 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() { - } - - /** - * 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(const char* value) : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value), - d_children() { - } - - /** - * This adds a convenience wrapper to SExpr to cast from bools. - * This is internally handled as the strings "true" and "false" - */ - SExpr(bool value) : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value ? "true" : "false"), - d_children() { - } - - 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) { - } - - /** 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; - - /** Is this S-expression a keyword? */ - bool isKeyword() const; - - /** - * Get the string value of this S-expression. This will cause an - * error if this S-expression is not an atom. - */ - 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 CVC4::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 CVC4::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; - - /** Is this S-expression equal to another? */ - bool operator==(const SExpr& s) const; - - /** Is this S-expression different from another? */ - bool operator!=(const SExpr& s) const; - -};/* class SExpr */ - -inline bool SExpr::isAtom() const { - return d_sexprType != SEXPR_NOT_ATOM; -} - -inline bool SExpr::isInteger() const { - return d_sexprType == SEXPR_INTEGER; -} - -inline bool SExpr::isRational() const { - return d_sexprType == SEXPR_RATIONAL; -} - -inline bool SExpr::isString() const { - return d_sexprType == SEXPR_STRING; -} - -inline bool SExpr::isKeyword() const { - return d_sexprType == SEXPR_KEYWORD; -} - -inline std::string SExpr::getValue() const { - CheckArgument( isAtom(), this ); - switch(d_sexprType) { - case SEXPR_INTEGER: - return d_integerValue.toString(); - case SEXPR_RATIONAL: { - // We choose to represent rationals as decimal strings rather than - // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL - // could be added if we need both styles, even if it's backed by - // the same Rational object. - std::stringstream ss; - ss << std::fixed << d_rationalValue.getDouble(); - return ss.str(); - } - case SEXPR_STRING: - case SEXPR_KEYWORD: - return d_stringValue; - case SEXPR_NOT_ATOM: - return std::string(); - } - return std::string(); -} - -inline const CVC4::Integer& SExpr::getIntegerValue() const { - CheckArgument( isInteger(), this ); - return d_integerValue; -} - -inline const CVC4::Rational& SExpr::getRationalValue() const { - CheckArgument( isRational(), this ); - return d_rationalValue; -} - -inline const std::vector<SExpr>& SExpr::getChildren() const { - CheckArgument( !isAtom(), this ); - return d_children; -} - -inline 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; -} - -inline bool SExpr::operator!=(const SExpr& s) const { - return !(*this == s); -} - -std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__SEXPR_H */ |