src/util/sexpr.cpp

   1 /*********************                                                        */
   2 /*! \file sexpr.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Simple representation of S-expressions
  13  **
  14  ** Simple representation of S-expressions.
  15  **
  16  ** SExprs have their own language specific printing procedures. The reason for
  17  ** this being implemented on SExpr and not on the Printer class is that the
  18  ** Printer class lives in libcvc4. It has to currently as it prints fairly
  19  ** complicated objects, like Model, which in turn uses SmtEngine pointers.
  20  ** However, SExprs need to be printed by Statistics. To get the output
  21  ** consistent with the previous version, the printing of SExprs in different
  22  ** languages is handled in the SExpr class and the libexpr library.
  23  **/
  24
  25 #include "util/sexpr.h"
  26
  27 #include <iostream>
  28 #include <sstream>
  29 #include <vector>
  30
  31 #include "base/cvc4_assert.h"
  32 #include "options/set_language.h"
  33 #include "util/smt2_quote_string.h"
  34
  35 namespace CVC4 {
  36
  37 const int PrettySExprs::s_iosIndex = std::ios_base::xalloc();
  38
  39 std::ostream& operator<<(std::ostream& out, PrettySExprs ps) {
  40   ps.applyPrettySExprs(out);
  41   return out;
  42 }
  43
  44 SExpr::~SExpr() {
  45   if (d_children != NULL) {
  46     delete d_children;
  47     d_children = NULL;
  48   }
  49   Assert(d_children == NULL);
  50 }
  51
  52 SExpr& SExpr::operator=(const SExpr& other) {
  53   d_sexprType = other.d_sexprType;
  54   d_integerValue = other.d_integerValue;
  55   d_rationalValue = other.d_rationalValue;
  56   d_stringValue = other.d_stringValue;
  57
  58   if (d_children == NULL && other.d_children == NULL) {
  59     // Do nothing.
  60   } else if (d_children == NULL) {
  61     d_children = new SExprVector(*other.d_children);
  62   } else if (other.d_children == NULL) {
  63     delete d_children;
  64     d_children = NULL;
  65   } else {
  66     (*d_children) = other.getChildren();
  67   }
  68   Assert(isAtom() == other.isAtom());
  69   Assert((d_children == NULL) == isAtom());
  70   return *this;
  71 }
  72
  73 SExpr::SExpr()
  74     : d_sexprType(SEXPR_STRING),
  75       d_integerValue(0),
  76       d_rationalValue(0),
  77       d_stringValue(""),
  78       d_children(NULL) {}
  79
  80 SExpr::SExpr(const SExpr& other)
  81     : d_sexprType(other.d_sexprType),
  82       d_integerValue(other.d_integerValue),
  83       d_rationalValue(other.d_rationalValue),
  84       d_stringValue(other.d_stringValue),
  85       d_children(NULL) {
  86   d_children =
  87       (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children);
  88   // d_children being NULL is equivalent to the node being an atom.
  89   Assert((d_children == NULL) == isAtom());
  90 }
  91
  92 SExpr::SExpr(const CVC4::Integer& value)
  93     : d_sexprType(SEXPR_INTEGER),
  94       d_integerValue(value),
  95       d_rationalValue(0),
  96       d_stringValue(""),
  97       d_children(NULL) {}
  98
  99 SExpr::SExpr(int value)
 100     : d_sexprType(SEXPR_INTEGER),
 101       d_integerValue(value),
 102       d_rationalValue(0),
 103       d_stringValue(""),
 104       d_children(NULL) {}
 105
 106 SExpr::SExpr(long int value)
 107     : d_sexprType(SEXPR_INTEGER),
 108       d_integerValue(value),
 109       d_rationalValue(0),
 110       d_stringValue(""),
 111       d_children(NULL) {}
 112
 113 SExpr::SExpr(unsigned int value)
 114     : d_sexprType(SEXPR_INTEGER),
 115       d_integerValue(value),
 116       d_rationalValue(0),
 117       d_stringValue(""),
 118       d_children(NULL) {}
 119
 120 SExpr::SExpr(unsigned long int value)
 121     : d_sexprType(SEXPR_INTEGER),
 122       d_integerValue(value),
 123       d_rationalValue(0),
 124       d_stringValue(""),
 125       d_children(NULL) {}
 126
 127 SExpr::SExpr(const CVC4::Rational& value)
 128     : d_sexprType(SEXPR_RATIONAL),
 129       d_integerValue(0),
 130       d_rationalValue(value),
 131       d_stringValue(""),
 132       d_children(NULL) {}
 133
 134 SExpr::SExpr(const std::string& value)
 135     : d_sexprType(SEXPR_STRING),
 136       d_integerValue(0),
 137       d_rationalValue(0),
 138       d_stringValue(value),
 139       d_children(NULL) {}
 140
 141 /**
 142  * This constructs a string expression from a const char* value.
 143  * This cannot be removed in order to support SExpr("foo").
 144  * Given the other constructors this SExpr("foo") converts to bool.
 145  * instead of SExpr(string("foo")).
 146  */
 147 SExpr::SExpr(const char* value)
 148     : d_sexprType(SEXPR_STRING),
 149       d_integerValue(0),
 150       d_rationalValue(0),
 151       d_stringValue(value),
 152       d_children(NULL) {}
 153
 154 SExpr::SExpr(bool value)
 155     : d_sexprType(SEXPR_KEYWORD),
 156       d_integerValue(0),
 157       d_rationalValue(0),
 158       d_stringValue(value ? "true" : "false"),
 159       d_children(NULL) {}
 160
 161 SExpr::SExpr(const Keyword& value)
 162     : d_sexprType(SEXPR_KEYWORD),
 163       d_integerValue(0),
 164       d_rationalValue(0),
 165       d_stringValue(value.getString()),
 166       d_children(NULL) {}
 167
 168 SExpr::SExpr(const std::vector<SExpr>& children)
 169     : d_sexprType(SEXPR_NOT_ATOM),
 170       d_integerValue(0),
 171       d_rationalValue(0),
 172       d_stringValue(""),
 173       d_children(new SExprVector(children)) {}
 174
 175 std::string SExpr::toString() const {
 176   std::stringstream ss;
 177   ss << (*this);
 178   return ss.str();
 179 }
 180
 181 /** Is this S-expression an atom? */
 182 bool SExpr::isAtom() const { return d_sexprType != SEXPR_NOT_ATOM; }
 183
 184 /** Is this S-expression an integer? */
 185 bool SExpr::isInteger() const { return d_sexprType == SEXPR_INTEGER; }
 186
 187 /** Is this S-expression a rational? */
 188 bool SExpr::isRational() const { return d_sexprType == SEXPR_RATIONAL; }
 189
 190 /** Is this S-expression a string? */
 191 bool SExpr::isString() const { return d_sexprType == SEXPR_STRING; }
 192
 193 /** Is this S-expression a keyword? */
 194 bool SExpr::isKeyword() const { return d_sexprType == SEXPR_KEYWORD; }
 195
 196 std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
 197   SExpr::toStream(out, sexpr);
 198   return out;
 199 }
 200
 201 void SExpr::toStream(std::ostream& out, const SExpr& sexpr) {
 202   toStream(out, sexpr, language::SetLanguage::getLanguage(out));
 203 }
 204
 205 void SExpr::toStream(std::ostream& out, const SExpr& sexpr,
 206                      OutputLanguage language) {
 207   const int indent = PrettySExprs::getPrettySExprs(out) ? 2 : 0;
 208   toStream(out, sexpr, language, indent);
 209 }
 210
 211 void SExpr::toStream(std::ostream& out, const SExpr& sexpr,
 212                      OutputLanguage language, int indent) {
 213   if (sexpr.isKeyword() && languageQuotesKeywords(language)) {
 214     out << quoteSymbol(sexpr.getValue());
 215   } else {
 216     toStreamRec(out, sexpr, language, indent);
 217   }
 218 }
 219
 220 void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
 221                         OutputLanguage language, int indent) {
 222   if (sexpr.isInteger()) {
 223     out << sexpr.getIntegerValue();
 224   } else if (sexpr.isRational()) {
 225     const double approximation = sexpr.getRationalValue().getDouble();
 226     out << std::fixed << approximation;
 227   } else if (sexpr.isKeyword()) {
 228     out << sexpr.getValue();
 229   } else if (sexpr.isString()) {
 230     std::string s = sexpr.getValue();
 231     // escape backslash and quote
 232     for (size_t i = 0; i < s.length(); ++i) {
 233       if (s[i] == '"') {
 234         s.replace(i, 1, "\\\"");
 235         ++i;
 236       } else if (s[i] == '\\') {
 237         s.replace(i, 1, "\\\\");
 238         ++i;
 239       }
 240     }
 241     out << "\"" << s << "\"";
 242   } else {
 243     const std::vector<SExpr>& kids = sexpr.getChildren();
 244     out << (indent > 0 && kids.size() > 1 ? "( " : "(");
 245     bool first = true;
 246     for (std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end();
 247          ++i) {
 248       if (first) {
 249         first = false;
 250       } else {
 251         if (indent > 0) {
 252           out << "\n" << std::string(indent, ' ');
 253         } else {
 254           out << ' ';
 255         }
 256       }
 257       toStreamRec(out, *i, language,
 258                   indent <= 0 || indent > 2 ? 0 : indent + 2);
 259     }
 260     if (indent > 0 && kids.size() > 1) {
 261       out << '\n';
 262       if (indent > 2) {
 263         out << std::string(indent - 2, ' ');
 264       }
 265     }
 266     out << ')';
 267   }
 268 } /* toStreamRec() */
 269
 270 bool SExpr::languageQuotesKeywords(OutputLanguage language) {
 271   switch (language) {
 272     case language::output::LANG_SMTLIB_V1:
 273     case language::output::LANG_SMTLIB_V2_0:
 274     case language::output::LANG_SMTLIB_V2_5:
 275     case language::output::LANG_SMTLIB_V2_6:
 276     case language::output::LANG_SYGUS:
 277     case language::output::LANG_TPTP:
 278     case language::output::LANG_Z3STR:
 279       return true;
 280     case language::output::LANG_AST:
 281     case language::output::LANG_CVC3:
 282     case language::output::LANG_CVC4:
 283     default:
 284       return false;
 285   };
 286 }
 287
 288 std::string SExpr::getValue() const {
 289   PrettyCheckArgument(isAtom(), this);
 290   switch (d_sexprType) {
 291     case SEXPR_INTEGER:
 292       return d_integerValue.toString();
 293     case SEXPR_RATIONAL: {
 294       // We choose to represent rationals as decimal strings rather than
 295       // "numerator/denominator."  Perhaps an additional SEXPR_DECIMAL
 296       // could be added if we need both styles, even if it's backed by
 297       // the same Rational object.
 298       std::stringstream ss;
 299       ss << std::fixed << d_rationalValue.getDouble();
 300       return ss.str();
 301     }
 302     case SEXPR_STRING:
 303     case SEXPR_KEYWORD:
 304       return d_stringValue;
 305     case SEXPR_NOT_ATOM:
 306       return std::string();
 307   }
 308   return std::string();
 309 }
 310
 311 const CVC4::Integer& SExpr::getIntegerValue() const {
 312   PrettyCheckArgument(isInteger(), this);
 313   return d_integerValue;
 314 }
 315
 316 const CVC4::Rational& SExpr::getRationalValue() const {
 317   PrettyCheckArgument(isRational(), this);
 318   return d_rationalValue;
 319 }
 320
 321 const std::vector<SExpr>& SExpr::getChildren() const {
 322   PrettyCheckArgument(!isAtom(), this);
 323   Assert(d_children != NULL);
 324   return *d_children;
 325 }
 326
 327 bool SExpr::operator==(const SExpr& s) const {
 328   if (d_sexprType == s.d_sexprType && d_integerValue == s.d_integerValue &&
 329       d_rationalValue == s.d_rationalValue &&
 330       d_stringValue == s.d_stringValue) {
 331     if (d_children == NULL && s.d_children == NULL) {
 332       return true;
 333     } else if (d_children != NULL && s.d_children != NULL) {
 334       return getChildren() == s.getChildren();
 335     }
 336   }
 337   return false;
 338 }
 339
 340 bool SExpr::operator!=(const SExpr& s) const { return !(*this == s); }
 341
 342 SExpr SExpr::parseAtom(const std::string& atom) {
 343   if (atom == "true") {
 344     return SExpr(true);
 345   } else if (atom == "false") {
 346     return SExpr(false);
 347   } else {
 348     try {
 349       Integer z(atom);
 350       return SExpr(z);
 351     } catch (std::invalid_argument&) {
 352       // Fall through to the next case
 353     }
 354     try {
 355       Rational q(atom);
 356       return SExpr(q);
 357     } catch (std::invalid_argument&) {
 358       // Fall through to the next case
 359     }
 360     return SExpr(atom);
 361   }
 362 }
 363
 364 SExpr SExpr::parseListOfAtoms(const std::vector<std::string>& atoms) {
 365   std::vector<SExpr> parsedAtoms;
 366   typedef std::vector<std::string>::const_iterator const_iterator;
 367   for (const_iterator i = atoms.begin(), i_end = atoms.end(); i != i_end; ++i) {
 368     parsedAtoms.push_back(parseAtom(*i));
 369   }
 370   return SExpr(parsedAtoms);
 371 }
 372
 373 SExpr SExpr::parseListOfListOfAtoms(
 374     const std::vector<std::vector<std::string> >& atoms_lists) {
 375   std::vector<SExpr> parsedListsOfAtoms;
 376   typedef std::vector<std::vector<std::string> >::const_iterator const_iterator;
 377   for (const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end();
 378        i != i_end; ++i) {
 379     parsedListsOfAtoms.push_back(parseListOfAtoms(*i));
 380   }
 381   return SExpr(parsedListsOfAtoms);
 382 }
 383
 384 } /* CVC4 namespace */