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-2021 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 cvc5 {
  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 cvc5::Integer& value)
  94     : d_sexprType(SEXPR_INTEGER),
  95       d_integerValue(value),
  96       d_rationalValue(0),
  97       d_stringValue(""),
  98       d_children(NULL)
  99 {
 100 }
 101
 102 SExpr::SExpr(int value)
 103     : d_sexprType(SEXPR_INTEGER),
 104       d_integerValue(value),
 105       d_rationalValue(0),
 106       d_stringValue(""),
 107       d_children(NULL) {}
 108
 109 SExpr::SExpr(long int value)
 110     : d_sexprType(SEXPR_INTEGER),
 111       d_integerValue(value),
 112       d_rationalValue(0),
 113       d_stringValue(""),
 114       d_children(NULL) {}
 115
 116 SExpr::SExpr(unsigned int value)
 117     : d_sexprType(SEXPR_INTEGER),
 118       d_integerValue(value),
 119       d_rationalValue(0),
 120       d_stringValue(""),
 121       d_children(NULL) {}
 122
 123 SExpr::SExpr(unsigned long int value)
 124     : d_sexprType(SEXPR_INTEGER),
 125       d_integerValue(value),
 126       d_rationalValue(0),
 127       d_stringValue(""),
 128       d_children(NULL) {}
 129
 130 SExpr::SExpr(const cvc5::Rational& value)
 131     : d_sexprType(SEXPR_RATIONAL),
 132       d_integerValue(0),
 133       d_rationalValue(value),
 134       d_stringValue(""),
 135       d_children(NULL)
 136 {
 137 }
 138
 139 SExpr::SExpr(const std::string& value)
 140     : d_sexprType(SEXPR_STRING),
 141       d_integerValue(0),
 142       d_rationalValue(0),
 143       d_stringValue(value),
 144       d_children(NULL) {}
 145
 146 /**
 147  * This constructs a string expression from a const char* value.
 148  * This cannot be removed in order to support SExpr("foo").
 149  * Given the other constructors this SExpr("foo") converts to bool.
 150  * instead of SExpr(string("foo")).
 151  */
 152 SExpr::SExpr(const char* value)
 153     : d_sexprType(SEXPR_STRING),
 154       d_integerValue(0),
 155       d_rationalValue(0),
 156       d_stringValue(value),
 157       d_children(NULL) {}
 158
 159 SExpr::SExpr(bool value)
 160     : d_sexprType(SEXPR_KEYWORD),
 161       d_integerValue(0),
 162       d_rationalValue(0),
 163       d_stringValue(value ? "true" : "false"),
 164       d_children(NULL) {}
 165
 166 SExpr::SExpr(const Keyword& value)
 167     : d_sexprType(SEXPR_KEYWORD),
 168       d_integerValue(0),
 169       d_rationalValue(0),
 170       d_stringValue(value.getString()),
 171       d_children(NULL) {}
 172
 173 SExpr::SExpr(const std::vector<SExpr>& children)
 174     : d_sexprType(SEXPR_NOT_ATOM),
 175       d_integerValue(0),
 176       d_rationalValue(0),
 177       d_stringValue(""),
 178       d_children(new SExprVector(children)) {}
 179
 180 std::string SExpr::toString() const {
 181   std::stringstream ss;
 182   ss << (*this);
 183   return ss.str();
 184 }
 185
 186 /** Is this S-expression an atom? */
 187 bool SExpr::isAtom() const { return d_sexprType != SEXPR_NOT_ATOM; }
 188
 189 /** Is this S-expression an integer? */
 190 bool SExpr::isInteger() const { return d_sexprType == SEXPR_INTEGER; }
 191
 192 /** Is this S-expression a rational? */
 193 bool SExpr::isRational() const { return d_sexprType == SEXPR_RATIONAL; }
 194
 195 /** Is this S-expression a string? */
 196 bool SExpr::isString() const { return d_sexprType == SEXPR_STRING; }
 197
 198 /** Is this S-expression a keyword? */
 199 bool SExpr::isKeyword() const { return d_sexprType == SEXPR_KEYWORD; }
 200
 201 std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
 202   SExpr::toStream(out, sexpr);
 203   return out;
 204 }
 205
 206 void SExpr::toStream(std::ostream& out, const SExpr& sexpr) {
 207   toStream(out, sexpr, language::SetLanguage::getLanguage(out));
 208 }
 209
 210 void SExpr::toStream(std::ostream& out, const SExpr& sexpr,
 211                      OutputLanguage language) {
 212   const int indent = PrettySExprs::getPrettySExprs(out) ? 2 : 0;
 213   toStream(out, sexpr, language, indent);
 214 }
 215
 216 void SExpr::toStream(std::ostream& out, const SExpr& sexpr,
 217                      OutputLanguage language, int indent) {
 218   if (sexpr.isKeyword() && languageQuotesKeywords(language)) {
 219     out << quoteSymbol(sexpr.getValue());
 220   } else {
 221     toStreamRec(out, sexpr, language, indent);
 222   }
 223 }
 224
 225 void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
 226                         OutputLanguage language, int indent) {
 227   StreamFormatScope scope(out);
 228
 229   if (sexpr.isInteger()) {
 230     out << sexpr.getIntegerValue();
 231   } else if (sexpr.isRational()) {
 232     const double approximation = sexpr.getRationalValue().getDouble();
 233     out << std::fixed << approximation;
 234   } else if (sexpr.isKeyword()) {
 235     out << sexpr.getValue();
 236   } else if (sexpr.isString()) {
 237     std::string s = sexpr.getValue();
 238     // escape backslash and quote
 239     for (size_t i = 0; i < s.length(); ++i) {
 240       if (s[i] == '"') {
 241         s.replace(i, 1, "\\\"");
 242         ++i;
 243       } else if (s[i] == '\\') {
 244         s.replace(i, 1, "\\\\");
 245         ++i;
 246       }
 247     }
 248     out << "\"" << s << "\"";
 249   } else {
 250     const std::vector<SExpr>& kids = sexpr.getChildren();
 251     out << (indent > 0 && kids.size() > 1 ? "( " : "(");
 252     bool first = true;
 253     for (std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end();
 254          ++i) {
 255       if (first) {
 256         first = false;
 257       } else {
 258         if (indent > 0) {
 259           out << "\n" << std::string(indent, ' ');
 260         } else {
 261           out << ' ';
 262         }
 263       }
 264       toStreamRec(out, *i, language,
 265                   indent <= 0 || indent > 2 ? 0 : indent + 2);
 266     }
 267     if (indent > 0 && kids.size() > 1) {
 268       out << '\n';
 269       if (indent > 2) {
 270         out << std::string(indent - 2, ' ');
 271       }
 272     }
 273     out << ')';
 274   }
 275 } /* toStreamRec() */
 276
 277 bool SExpr::languageQuotesKeywords(OutputLanguage language) {
 278   switch (language) {
 279     case language::output::LANG_TPTP:
 280       return true;
 281     case language::output::LANG_AST:
 282     case language::output::LANG_CVC3:
 283     case language::output::LANG_CVC4:
 284     default: return language::isOutputLang_smt2(language);
 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 cvc5::Integer& SExpr::getIntegerValue() const
 312 {
 313   PrettyCheckArgument(isInteger(), this);
 314   return d_integerValue;
 315 }
 316
 317 const cvc5::Rational& SExpr::getRationalValue() const
 318 {
 319   PrettyCheckArgument(isRational(), this);
 320   return d_rationalValue;
 321 }
 322
 323 const std::vector<SExpr>& SExpr::getChildren() const {
 324   PrettyCheckArgument(!isAtom(), this);
 325   Assert(d_children != NULL);
 326   return *d_children;
 327 }
 328
 329 bool SExpr::operator==(const SExpr& s) const {
 330   if (d_sexprType == s.d_sexprType && d_integerValue == s.d_integerValue &&
 331       d_rationalValue == s.d_rationalValue &&
 332       d_stringValue == s.d_stringValue) {
 333     if (d_children == NULL && s.d_children == NULL) {
 334       return true;
 335     } else if (d_children != NULL && s.d_children != NULL) {
 336       return getChildren() == s.getChildren();
 337     }
 338   }
 339   return false;
 340 }
 341
 342 bool SExpr::operator!=(const SExpr& s) const { return !(*this == s); }
 343
 344 SExpr SExpr::parseAtom(const std::string& atom) {
 345   if (atom == "true") {
 346     return SExpr(true);
 347   } else if (atom == "false") {
 348     return SExpr(false);
 349   } else {
 350     try {
 351       Integer z(atom);
 352       return SExpr(z);
 353     } catch (std::invalid_argument&) {
 354       // Fall through to the next case
 355     }
 356     try {
 357       Rational q(atom);
 358       return SExpr(q);
 359     } catch (std::invalid_argument&) {
 360       // Fall through to the next case
 361     }
 362     return SExpr(atom);
 363   }
 364 }
 365
 366 SExpr SExpr::parseListOfAtoms(const std::vector<std::string>& atoms) {
 367   std::vector<SExpr> parsedAtoms;
 368   typedef std::vector<std::string>::const_iterator const_iterator;
 369   for (const_iterator i = atoms.begin(), i_end = atoms.end(); i != i_end; ++i) {
 370     parsedAtoms.push_back(parseAtom(*i));
 371   }
 372   return SExpr(parsedAtoms);
 373 }
 374
 375 SExpr SExpr::parseListOfListOfAtoms(
 376     const std::vector<std::vector<std::string> >& atoms_lists) {
 377   std::vector<SExpr> parsedListsOfAtoms;
 378   typedef std::vector<std::vector<std::string> >::const_iterator const_iterator;
 379   for (const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end();
 380        i != i_end; ++i) {
 381     parsedListsOfAtoms.push_back(parseListOfAtoms(*i));
 382   }
 383   return SExpr(parsedListsOfAtoms);
 384 }
 385
 386 }  // namespace cvc5