#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"
#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.
#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
// 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"
pickler.h \
resource_manager.cpp \
resource_manager.h \
- sexpr.cpp \
- sexpr.h \
symbol_table.cpp \
symbol_table.h \
type.cpp \
kind.i \
expr.i \
resource_manager.i \
- sexpr.i \
record.i \
predicate.i \
variable_type_map.i \
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-%{
-#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"
#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;
#include <string>
#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 {
#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"
#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)
#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"
#include "smt/smt_engine_scope.h"
#include "smt_util/dump.h"
#include "smt_util/model.h"
+#include "util/sexpr.h"
using namespace std;
#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 {
regexp.h \
result.cpp \
result.h \
+ sexpr.cpp \
+ sexpr.h \
smt2_quote_string.cpp \
smt2_quote_string.h \
subrange_bound.cpp \
rational_gmp_imp.h \
regexp.i \
result.i \
+ sexpr.i \
subrange_bound.i \
tuple.i \
unsafe_interrupt_exception.i
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+#include <sstream>
+#include <vector>
+
+#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<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 */
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+%{
+#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"
#include <sstream>
#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;
projects / cvc5.git / commitdiff