summaryrefslogtreecommitdiff
path: root/src/expr/sexpr.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/sexpr.cpp')
-rw-r--r--src/expr/sexpr.cpp233
1 files changed, 233 insertions, 0 deletions
diff --git a/src/expr/sexpr.cpp b/src/expr/sexpr.cpp
new file mode 100644
index 000000000..a321f85aa
--- /dev/null
+++ b/src/expr/sexpr.cpp
@@ -0,0 +1,233 @@
+/********************* */
+/*! \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 "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;
+}
+
+std::string SExpr::toString() const {
+ std::stringstream ss;
+ ss << (*this);
+ return ss.str();
+}
+
+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, Expr::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 {
+ CheckArgument( isAtom(), this );
+ switch(d_sexprType) {
+ case SEXPR_INTEGER:
+ return d_integerValue.toString();
+ case SEXPR_RATIONAL: {
+ // We choose to represent rationals as decimal strings rather than
+ // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL
+ // could be added if we need both styles, even if it's backed by
+ // the same Rational object.
+ std::stringstream ss;
+ ss << std::fixed << d_rationalValue.getDouble();
+ return ss.str();
+ }
+ case SEXPR_STRING:
+ case SEXPR_KEYWORD:
+ return d_stringValue;
+ case SEXPR_NOT_ATOM:
+ return std::string();
+ }
+ return std::string();
+
+}
+
+const CVC4::Integer& SExpr::getIntegerValue() const {
+ CheckArgument( isInteger(), this );
+ return d_integerValue;
+}
+
+const CVC4::Rational& SExpr::getRationalValue() const {
+ CheckArgument( isRational(), this );
+ return d_rationalValue;
+}
+
+const std::vector<SExpr>& SExpr::getChildren() const {
+ CheckArgument( !isAtom(), this );
+ return d_children;
+}
+
+bool SExpr::operator==(const SExpr& s) const {
+ return d_sexprType == s.d_sexprType &&
+ d_integerValue == s.d_integerValue &&
+ d_rationalValue == s.d_rationalValue &&
+ d_stringValue == s.d_stringValue &&
+ d_children == s.d_children;
+}
+
+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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback