summaryrefslogtreecommitdiff
path: root/src/util/sexpr.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/sexpr.h')
-rw-r--r--src/util/sexpr.h304
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback