From: Tim King Date: Wed, 6 Jan 2016 01:28:38 +0000 (-0800) Subject: Moving sexpr.{cpp,h,i} from expr/ back into util/. X-Git-Tag: cvc5-1.0.0~6119 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b5f91dae58691468f6c8f2d7c6aebf639f1d017b;p=cvc5.git Moving sexpr.{cpp,h,i} from expr/ back into util/. --- diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 24c4d8112..9ae394b97 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -28,7 +28,6 @@ #include "expr/expr_iomanip.h" #include "expr/kind.h" #include "expr/predicate.h" -#include "expr/sexpr.h" #include "options/base_options.h" #include "options/expr_options.h" #include "options/parser_options.h" @@ -41,9 +40,9 @@ #include "util/hash.h" #include "util/integer.h" #include "util/rational.h" +#include "util/sexpr.h" #include "util/subrange_bound.h" - using namespace std; // Matches base/cvc4_assert.h's PrettyCheckArgument. diff --git a/src/cvc4.i b/src/cvc4.i index e81276f23..601c9a878 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -52,12 +52,12 @@ using namespace CVC4; #include "base/modal_exception.h" #include "expr/datatype.h" #include "expr/expr.h" -#include "expr/sexpr.h" #include "expr/type.h" #include "options/option_exception.h" #include "smt_util/command.h" -#include "util/integer.h" #include "util/bitvector.h" +#include "util/integer.h" +#include "util/sexpr.h" #include "util/unsafe_interrupt_exception.h" #ifdef SWIGJAVA @@ -306,25 +306,24 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; // At the moment, the header includes seem to need to follow a special order. // I don't know why. I am following the build order %include "base/exception.i" -%include "util/unsafe_interrupt_exception.i" -%include "util/integer.i" -%include "util/rational.i" -%include "options/language.i" -%include "util/configuration.i" -%include "util/bool.i" -%include "util/cardinality.i" %include "base/modal_exception.i" -%include "expr/sexpr.i" - -%include "util/bitvector.i" +%include "options/language.i" +%include "util/bitvector.i" +%include "util/bool.i" +%include "util/cardinality.i" +%include "util/configuration.i" %include "util/hash.i" +%include "util/integer.i" %include "util/proof.i" +%include "util/rational.i" %include "util/regexp.i" %include "util/result.i" +%include "util/sexpr.i" %include "util/subrange_bound.i" %include "util/tuple.i" +%include "util/unsafe_interrupt_exception.i" //%include "util/floatingpoint.i" %include "expr/uninterpreted_constant.i" 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 -#include -#include - -#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& 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& kids = sexpr.getChildren(); - out << (indent > 0 && kids.size() > 1 ? "( " : "("); - bool first = true; - for(std::vector::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::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& atoms) { - std::vector parsedAtoms; - typedef std::vector::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 >& atoms_lists) { - std::vector parsedListsOfAtoms; - typedef std::vector< std::vector >::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 -#include -#include -#include - -#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& 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& 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& atoms); - - /** - * Parses a list of list of atoms. - */ - static SExpr parseListOfListOfAtoms(const std::vector< std::vector >& 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 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 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 #include #include #include #include +#include "util/sexpr.h" + namespace CVC4 { class Stat; diff --git a/src/printer/printer.h b/src/printer/printer.h index 48787f70a..ca9aff65d 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -23,10 +23,10 @@ #include #include "expr/node.h" -#include "expr/sexpr.h" #include "options/language.h" #include "smt_util/command.h" #include "smt_util/model.h" +#include "util/sexpr.h" namespace CVC4 { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3f049e392..531b499ac 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -28,7 +28,6 @@ #include "context/cdlist_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" -#include "expr/sexpr.h" #include "expr/statistics.h" #include "options/options.h" #include "proof/unsat_core.h" @@ -38,6 +37,7 @@ #include "util/hash.h" #include "util/proof.h" #include "util/result.h" +#include "util/sexpr.h" #include "util/unsafe_interrupt_exception.h" // In terms of abstraction, this is below (and provides services to) diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp index 5917d71da..8cc8a421c 100644 --- a/src/smt_util/command.cpp +++ b/src/smt_util/command.cpp @@ -27,7 +27,6 @@ #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/node.h" -#include "expr/sexpr.h" #include "options/options.h" #include "options/smt_options.h" #include "printer/printer.h" @@ -35,6 +34,7 @@ #include "smt/smt_engine_scope.h" #include "smt_util/dump.h" #include "smt_util/model.h" +#include "util/sexpr.h" using namespace std; diff --git a/src/smt_util/command.h b/src/smt_util/command.h index c9b968722..d8f9789f5 100644 --- a/src/smt_util/command.h +++ b/src/smt_util/command.h @@ -30,12 +30,12 @@ #include "expr/datatype.h" #include "expr/expr.h" -#include "expr/sexpr.h" #include "expr/type.h" #include "expr/variable_type_map.h" #include "proof/unsat_core.h" #include "util/proof.h" #include "util/result.h" +#include "util/sexpr.h" namespace CVC4 { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index b06666ae3..d086e3068 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -45,6 +45,8 @@ libutil_la_SOURCES = \ regexp.h \ result.cpp \ result.h \ + sexpr.cpp \ + sexpr.h \ smt2_quote_string.cpp \ smt2_quote_string.h \ subrange_bound.cpp \ @@ -92,6 +94,7 @@ EXTRA_DIST = \ rational_gmp_imp.h \ regexp.i \ result.i \ + sexpr.i \ subrange_bound.i \ tuple.i \ unsafe_interrupt_exception.i diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp new file mode 100644 index 000000000..eb53e34c2 --- /dev/null +++ b/src/util/sexpr.cpp @@ -0,0 +1,412 @@ +/********************* */ +/*! \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 "util/sexpr.h" + +#include +#include +#include + +#include "base/cvc4_assert.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& 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& kids = sexpr.getChildren(); + out << (indent > 0 && kids.size() > 1 ? "( " : "("); + bool first = true; + for(std::vector::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::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& atoms) { + std::vector parsedAtoms; + typedef std::vector::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 >& atoms_lists) { + std::vector parsedListsOfAtoms; + typedef std::vector< std::vector >::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/util/sexpr.h b/src/util/sexpr.h new file mode 100644 index 000000000..40fd9dd56 --- /dev/null +++ b/src/util/sexpr.h @@ -0,0 +1,305 @@ +/********************* */ +/*! \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 +#include +#include +#include + +#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& 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& 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& atoms); + + /** + * Parses a list of list of atoms. + */ + static SExpr parseListOfListOfAtoms(const std::vector< std::vector >& 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 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 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/util/sexpr.i b/src/util/sexpr.i new file mode 100644 index 000000000..4c89c5019 --- /dev/null +++ b/src/util/sexpr.i @@ -0,0 +1,21 @@ +%{ +#include "util/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 "util/sexpr.h" diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp index baa901540..884ffb8a6 100644 --- a/test/system/statistics.cpp +++ b/test/system/statistics.cpp @@ -19,9 +19,9 @@ #include #include "expr/expr.h" -#include "expr/sexpr.h" #include "expr/statistics.h" #include "smt/smt_engine.h" +#include "util/sexpr.h" using namespace CVC4; using namespace std;