src/util/sexpr.cpp

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