Moving sexpr.{cpp,h,i} from expr/ back into util/.

5 files changed, 2 insertions, 745 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index d4964f56a..5c046c282 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -54,8 +54,6 @@ libexpr_la_SOURCES = \
 	pickler.h \
 	resource_manager.cpp \
 	resource_manager.h \
-	sexpr.cpp \
-	sexpr.h \
 	symbol_table.cpp \
 	symbol_table.h \
 	type.cpp \
@@ -109,7 +107,6 @@ EXTRA_DIST = \
 	kind.i \
 	expr.i \
 	resource_manager.i \
-	sexpr.i \
 	record.i \
 	predicate.i \
 	variable_type_map.i \
diff --git a/src/expr/sexpr.cpp b/src/expr/sexpr.cpp
deleted file mode 100644
index 69741859f..000000000
--- a/src/expr/sexpr.cpp
+++ /dev/null
@@ -1,414 +0,0 @@
-/*********************                                                        */
-/*! \file sexpr.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** 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.
- **
- ** SExprs have their own language specific printing procedures. The reason for
- ** this being implemented on SExpr and not on the Printer class is that the
- ** Printer class lives in libcvc4. It has to currently as it prints fairly
- ** complicated objects, like Model, which in turn uses SmtEngine pointers.
- ** However, SExprs need to be printed by Statistics. To get the output consistent
- ** with the previous version, the printing of SExprs in different languages is
- ** handled in the SExpr class and the libexpr library.
- **/
-
-#include "expr/sexpr.h"
-
-#include <iostream>
-#include <sstream>
-#include <vector>
-
-#include "base/cvc4_assert.h"
-#include "expr/expr.h"
-#include "options/set_language.h"
-#include "util/smt2_quote_string.h"
-
-
-namespace CVC4 {
-
-const int PrettySExprs::s_iosIndex = std::ios_base::xalloc();
-
-std::ostream& operator<<(std::ostream& out, PrettySExprs ps) {
-  ps.applyPrettySExprs(out);
-  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(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 {
-  std::stringstream ss;
-  ss << (*this);
-  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, language::SetLanguage::getLanguage(out));
-}
-
-void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() {
-  toStream(out, sexpr, language, PrettySExprs::getPrettySExprs(out) ? 2 : 0);
-}
-
-void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() {
-  if( sexpr.isKeyword() && languageQuotesKeywords(language) ){
-    out << quoteSymbol(sexpr.getValue());
-  } else {
-    toStreamRec(out, sexpr, language, indent);
-  }
-}
-
-
-void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() {
-  if(sexpr.isInteger()) {
-    out << sexpr.getIntegerValue();
-  } else if(sexpr.isRational()) {
-    out << std::fixed << sexpr.getRationalValue().getDouble();
-  } else if(sexpr.isKeyword()) {
-    out << sexpr.getValue();
-  } else if(sexpr.isString()) {
-    std::string s = sexpr.getValue();
-    // escape backslash and quote
-    for(size_t i = 0; i < s.length(); ++i) {
-      if(s[i] == '"') {
-        s.replace(i, 1, "\\\"");
-        ++i;
-      } else if(s[i] == '\\') {
-        s.replace(i, 1, "\\\\");
-        ++i;
-      }
-    }
-    out << "\"" << s << "\"";
-  } else {
-    const std::vector<SExpr>& kids = sexpr.getChildren();
-    out << (indent > 0 && kids.size() > 1 ? "( " : "(");
-    bool first = true;
-    for(std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
-      if(first) {
-        first = false;
-      } else {
-        if(indent > 0) {
-          out << "\n" << std::string(indent, ' ');
-        } else {
-          out << ' ';
-        }
-      }
-      toStreamRec(out, *i, language, indent <= 0 || indent > 2 ? 0 : indent + 2);
-    }
-    if(indent > 0 && kids.size() > 1) {
-      out << '\n';
-      if(indent > 2) {
-        out << std::string(indent - 2, ' ');
-      }
-    }
-    out << ')';
-  }
-}/* toStreamRec() */
-
-
-bool SExpr::languageQuotesKeywords(OutputLanguage language) {
-  switch(language) {
-    case language::output::LANG_SMTLIB_V1:
-    case language::output::LANG_SMTLIB_V2_0:
-    case language::output::LANG_SMTLIB_V2_5:
-    case language::output::LANG_SYGUS:
-    case language::output::LANG_TPTP:
-    case language::output::LANG_Z3STR:
-      return true;
-    case language::output::LANG_AST:
-    case language::output::LANG_CVC3:
-    case language::output::LANG_CVC4:
-    default:
-      return false;
-  };
-}
-
-
-
-std::string SExpr::getValue() const {
-  PrettyCheckArgument( 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();
-
-}
-
-const CVC4::Integer& SExpr::getIntegerValue() const {
-  PrettyCheckArgument( isInteger(), this );
-  return d_integerValue;
-}
-
-const CVC4::Rational& SExpr::getRationalValue() const {
-  PrettyCheckArgument( isRational(), this );
-  return d_rationalValue;
-}
-
-const std::vector<SExpr>& SExpr::getChildren() const {
-  PrettyCheckArgument( !isAtom(), this );
-  Assert( d_children != NULL );
-  return *d_children;
-}
-
-bool SExpr::operator==(const SExpr& s) const {
-  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 {
-  return !(*this == s);
-}
-
-
-SExpr SExpr::parseAtom(const std::string& atom) {
-  if(atom == "true"){
-    return SExpr(true);
-  } else if(atom == "false"){
-    return SExpr(false);
-  } else {
-    try {
-      Integer z(atom);
-      return SExpr(z);
-    }catch(std::invalid_argument&){
-      // Fall through to the next case
-    }
-    try {
-      Rational q(atom);
-      return SExpr(q);
-    }catch(std::invalid_argument&){
-      // Fall through to the next case
-    }
-    return SExpr(atom);
-  }
-}
-
-SExpr SExpr::parseListOfAtoms(const std::vector<std::string>& atoms) {
-  std::vector<SExpr> parsedAtoms;
-  typedef std::vector<std::string>::const_iterator const_iterator;
-  for(const_iterator i = atoms.begin(), i_end=atoms.end(); i != i_end; ++i){
-    parsedAtoms.push_back(parseAtom(*i));
-  }
-  return SExpr(parsedAtoms);
-}
-
-SExpr SExpr::parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists) {
-  std::vector<SExpr> parsedListsOfAtoms;
-  typedef std::vector< std::vector<std::string> >::const_iterator const_iterator;
-  for(const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); i != i_end; ++i){
-    parsedListsOfAtoms.push_back(parseListOfAtoms(*i));
-  }
-  return SExpr(parsedListsOfAtoms);
-}
-
-
-
-}/* CVC4 namespace */
diff --git a/src/expr/sexpr.h b/src/expr/sexpr.h
deleted file mode 100644
index 40fd9dd56..000000000
--- a/src/expr/sexpr.h
+++ /dev/null
@@ -1,305 +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 <iomanip>
-#include <iosfwd>
-#include <string>
-#include <vector>
-
-#include "base/exception.h"
-#include "options/language.h"
-#include "util/integer.h"
-#include "util/rational.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 {
-public:
-
-  typedef SExprKeyword Keyword;
-
-  SExpr();
-  SExpr(const SExpr&);
-  SExpr& operator=(const SExpr& other);
-  ~SExpr();
-
-  SExpr(const CVC4::Integer& value);
-
-  SExpr(int value);
-  SExpr(long int value);
-  SExpr(unsigned int value);
-  SExpr(unsigned long int value);
-
-  SExpr(const CVC4::Rational& value);
-
-  SExpr(const std::string& value);
-
-  /**
-   * 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);
-
-  /**
-   * 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);
-  SExpr(const std::vector<SExpr>& 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;
-
-  /**
-   * This wraps the toStream() printer.
-   * NOTE: toString() and getValue() may differ on Keywords based on
-   * the current language set in expr.
-   */
-  std::string toString() 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;
-
-
-  /**
-   * This returns the best match in the following order:
-   * match atom with
-   *  "true", "false" -> SExpr(value)
-   * | is and integer -> as integer
-   * | is a rational -> as rational
-   * | _ -> SExpr()
-   */
-  static SExpr parseAtom(const std::string& atom);
-
-  /**
-   * Parses a list of atoms.
-   */
-  static SExpr parseListOfAtoms(const std::vector<std::string>& atoms);
-
-  /**
-   * Parses a list of list of atoms.
-   */
-  static SExpr parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists);
-
-
-  /**
-   * Outputs the SExpr onto the ostream out. This version reads defaults to the
-   * 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();
-
-  /**
-   * Outputs the SExpr onto the ostream out. This version sets the indent level
-   * to 2 if PrettySExprs::getPrettySExprs() is on.
-   */
-  static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw();
-
-  /**
-   * Outputs the SExpr onto the ostream out.
-   * If the languageQuotesKeywords(language), then a top level keyword, " X",
-   * that needs quoting according to the SMT2 language standard is printed with
-   * quotes, "| X|".
-   * Otherwise this prints using toStreamRec().
-   *
-   * TIM: Keywords that are children are not currently quoted. This seems
-   * incorrect but I am just reproduicing the old behavior even if it does not make
-   * sense.
-   */
-  static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw();
-
-private:
-
-  /**
-   * Simple printer for SExpr to an ostream.
-   * The current implementation is language independent.
-   */
-  static void toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw();
-
-
-  /** 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. */
-std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC;
-
-/**
- * IOStream manipulator to pretty-print SExprs.
- */
-class CVC4_PUBLIC PrettySExprs {
-  /**
-   * The allocated index in ios_base for our setting.
-   */
-  static const int s_iosIndex;
-
-  /**
-   * When this manipulator is used, the setting is stored here.
-   */
-  bool d_prettySExprs;
-
-public:
-  /**
-   * Construct a PrettySExprs with the given setting.
-   */
-  PrettySExprs(bool prettySExprs) : d_prettySExprs(prettySExprs) {}
-
-  inline void applyPrettySExprs(std::ostream& out) {
-    out.iword(s_iosIndex) = d_prettySExprs;
-  }
-
-  static inline bool getPrettySExprs(std::ostream& out) {
-    return out.iword(s_iosIndex);
-  }
-
-  static inline void setPrettySExprs(std::ostream& out, bool prettySExprs) {
-    out.iword(s_iosIndex) = prettySExprs;
-  }
-
-  /**
-   * Set the pretty-sexprs state on the output stream for the current
-   * stack scope.  This makes sure the old state is reset on the
-   * stream after normal OR exceptional exit from the scope, using the
-   * RAII C++ idiom.
-   */
-  class Scope {
-    std::ostream& d_out;
-    bool d_oldPrettySExprs;
-
-  public:
-
-    inline Scope(std::ostream& out, bool prettySExprs) :
-      d_out(out),
-      d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) {
-      PrettySExprs::setPrettySExprs(out, prettySExprs);
-    }
-
-    inline ~Scope() {
-      PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs);
-    }
-
-  };/* class PrettySExprs::Scope */
-
-};/* class PrettySExprs */
-
-/**
- * Sets the default pretty-sexprs setting for an ostream.  Use like this:
- *
- *   // let out be an ostream, s an SExpr
- *   out << PrettySExprs(true) << s << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-std::ostream& operator<<(std::ostream& out, PrettySExprs ps);
-
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SEXPR_H */
diff --git a/src/expr/sexpr.i b/src/expr/sexpr.i
deleted file mode 100644
index f6229782e..000000000
--- a/src/expr/sexpr.i
+++ /dev/null
@@ -1,21 +0,0 @@
-%{
-#include "expr/sexpr.h"
-%}
-
-%ignore CVC4::operator<<(std::ostream&, const SExpr&);
-%ignore CVC4::operator<<(std::ostream&, SExpr::SexprTypes);
-
-// for Java and the like
-%extend CVC4::SExpr {
-  std::string toString() const { return self->getValue(); }
-};/* CVC4::SExpr */
-
-%ignore CVC4::SExpr::SExpr(int);
-%ignore CVC4::SExpr::SExpr(unsigned int);
-%ignore CVC4::SExpr::SExpr(unsigned long);
-%ignore CVC4::SExpr::SExpr(const char*);
-
-%rename(equals) CVC4::SExpr::operator==(const SExpr&) const;
-%ignore CVC4::SExpr::operator!=(const SExpr&) const;
-
-%include "expr/sexpr.h"
diff --git a/src/expr/statistics.h b/src/expr/statistics.h
index 425404692..a0b6ed083 100644
--- a/src/expr/statistics.h
+++ b/src/expr/statistics.h
@@ -20,14 +20,14 @@
 #ifndef __CVC4__STATISTICS_H
 #define __CVC4__STATISTICS_H
 
-#include "expr/sexpr.h"
-
 #include <iterator>
 #include <ostream>
 #include <set>
 #include <string>
 #include <utility>
 
+#include "util/sexpr.h"
+
 namespace CVC4 {
 
 class Stat;