src/util/sexpr.cpp

   1 /*********************                                                        */
   2 /*! \file sexpr.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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 consistent
  21  ** with the previous version, the printing of SExprs in different languages is
  22  ** 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
  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
  82
  83 SExpr::SExpr(const SExpr& other) :
  84     d_sexprType(other.d_sexprType),
  85     d_integerValue(other.d_integerValue),
  86     d_rationalValue(other.d_rationalValue),
  87     d_stringValue(other.d_stringValue),
  88     d_children(NULL)
  89 {
  90   d_children = (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children);
  91   // d_children being NULL is equivalent to the node being an atom.
  92   Assert( (d_children == NULL) == isAtom() );
  93 }
  94
  95
  96 SExpr::SExpr(const CVC4::Integer& value) :
  97     d_sexprType(SEXPR_INTEGER),
  98     d_integerValue(value),
  99     d_rationalValue(0),
 100     d_stringValue(""),
 101     d_children(NULL) {
 102   }
 103
 104 SExpr::SExpr(int value) :
 105     d_sexprType(SEXPR_INTEGER),
 106     d_integerValue(value),
 107     d_rationalValue(0),
 108     d_stringValue(""),
 109     d_children(NULL) {
 110 }
 111
 112 SExpr::SExpr(long int value) :
 113     d_sexprType(SEXPR_INTEGER),
 114     d_integerValue(value),
 115     d_rationalValue(0),
 116     d_stringValue(""),
 117     d_children(NULL) {
 118 }
 119
 120 SExpr::SExpr(unsigned int value) :
 121     d_sexprType(SEXPR_INTEGER),
 122     d_integerValue(value),
 123     d_rationalValue(0),
 124     d_stringValue(""),
 125     d_children(NULL) {
 126 }
 127
 128 SExpr::SExpr(unsigned long int value) :
 129     d_sexprType(SEXPR_INTEGER),
 130     d_integerValue(value),
 131     d_rationalValue(0),
 132     d_stringValue(""),
 133     d_children(NULL) {
 134 }
 135
 136 SExpr::SExpr(const CVC4::Rational& value) :
 137     d_sexprType(SEXPR_RATIONAL),
 138     d_integerValue(0),
 139     d_rationalValue(value),
 140     d_stringValue(""),
 141     d_children(NULL) {
 142 }
 143
 144 SExpr::SExpr(const std::string& value) :
 145     d_sexprType(SEXPR_STRING),
 146     d_integerValue(0),
 147     d_rationalValue(0),
 148     d_stringValue(value),
 149     d_children(NULL) {
 150 }
 151
 152   /**
 153    * This constructs a string expression from a const char* value.
 154    * This cannot be removed in order to support SExpr("foo").
 155    * Given the other constructors this SExpr("foo") converts to bool.
 156    * instead of SExpr(string("foo")).
 157    */
 158 SExpr::SExpr(const char* value) :
 159     d_sexprType(SEXPR_STRING),
 160     d_integerValue(0),
 161     d_rationalValue(0),
 162     d_stringValue(value),
 163     d_children(NULL) {
 164 }
 165
 166 #warning "TODO: Discuss this change with Clark."
 167 SExpr::SExpr(bool value) :
 168     d_sexprType(SEXPR_KEYWORD),
 169     d_integerValue(0),
 170     d_rationalValue(0),
 171     d_stringValue(value ? "true" : "false"),
 172     d_children(NULL) {
 173 }
 174
 175 SExpr::SExpr(const Keyword& value) :
 176     d_sexprType(SEXPR_KEYWORD),
 177     d_integerValue(0),
 178     d_rationalValue(0),
 179     d_stringValue(value.getString()),
 180     d_children(NULL) {
 181 }
 182
 183 SExpr::SExpr(const std::vector<SExpr>& children) :
 184     d_sexprType(SEXPR_NOT_ATOM),
 185     d_integerValue(0),
 186     d_rationalValue(0),
 187     d_stringValue(""),
 188     d_children(new SExprVector(children)) {
 189 }
 190
 191 std::string SExpr::toString() const {
 192   std::stringstream ss;
 193   ss << (*this);
 194   return ss.str();
 195 }
 196
 197 /** Is this S-expression an atom? */
 198 bool SExpr::isAtom() const {
 199   return d_sexprType != SEXPR_NOT_ATOM;
 200 }
 201
 202 /** Is this S-expression an integer? */
 203 bool SExpr::isInteger() const {
 204   return d_sexprType == SEXPR_INTEGER;
 205 }
 206
 207 /** Is this S-expression a rational? */
 208 bool SExpr::isRational() const {
 209   return d_sexprType == SEXPR_RATIONAL;
 210 }
 211
 212 /** Is this S-expression a string? */
 213 bool SExpr::isString() const {
 214   return d_sexprType == SEXPR_STRING;
 215 }
 216
 217 /** Is this S-expression a keyword? */
 218 bool SExpr::isKeyword() const {
 219   return d_sexprType == SEXPR_KEYWORD;
 220 }
 221
 222
 223 std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
 224   SExpr::toStream(out, sexpr);
 225   return out;
 226 }
 227
 228 void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() {
 229   toStream(out, sexpr, language::SetLanguage::getLanguage(out));
 230 }
 231
 232 void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() {
 233   toStream(out, sexpr, language, PrettySExprs::getPrettySExprs(out) ? 2 : 0);
 234 }
 235
 236 void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() {
 237   if( sexpr.isKeyword() && languageQuotesKeywords(language) ){
 238     out << quoteSymbol(sexpr.getValue());
 239   } else {
 240     toStreamRec(out, sexpr, language, indent);
 241   }
 242 }
 243
 244
 245 void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() {
 246   if(sexpr.isInteger()) {
 247     out << sexpr.getIntegerValue();
 248   } else if(sexpr.isRational()) {
 249     out << std::fixed << sexpr.getRationalValue().getDouble();
 250   } else if(sexpr.isKeyword()) {
 251     out << sexpr.getValue();
 252   } else if(sexpr.isString()) {
 253     std::string s = sexpr.getValue();
 254     // escape backslash and quote
 255     for(size_t i = 0; i < s.length(); ++i) {
 256       if(s[i] == '"') {
 257         s.replace(i, 1, "\\\"");
 258         ++i;
 259       } else if(s[i] == '\\') {
 260         s.replace(i, 1, "\\\\");
 261         ++i;
 262       }
 263     }
 264     out << "\"" << s << "\"";
 265   } else {
 266     const std::vector<SExpr>& kids = sexpr.getChildren();
 267     out << (indent > 0 && kids.size() > 1 ? "( " : "(");
 268     bool first = true;
 269     for(std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
 270       if(first) {
 271         first = false;
 272       } else {
 273         if(indent > 0) {
 274           out << "\n" << std::string(indent, ' ');
 275         } else {
 276           out << ' ';
 277         }
 278       }
 279       toStreamRec(out, *i, language, indent <= 0 || indent > 2 ? 0 : indent + 2);
 280     }
 281     if(indent > 0 && kids.size() > 1) {
 282       out << '\n';
 283       if(indent > 2) {
 284         out << std::string(indent - 2, ' ');
 285       }
 286     }
 287     out << ')';
 288   }
 289 }/* toStreamRec() */
 290
 291
 292 bool SExpr::languageQuotesKeywords(OutputLanguage language) {
 293   switch(language) {
 294     case language::output::LANG_SMTLIB_V1:
 295     case language::output::LANG_SMTLIB_V2_0:
 296     case language::output::LANG_SMTLIB_V2_5:
 297     case language::output::LANG_SYGUS:
 298     case language::output::LANG_TPTP:
 299     case language::output::LANG_Z3STR:
 300       return true;
 301     case language::output::LANG_AST:
 302     case language::output::LANG_CVC3:
 303     case language::output::LANG_CVC4:
 304     default:
 305       return false;
 306   };
 307 }
 308
 309
 310
 311 std::string SExpr::getValue() const {
 312   PrettyCheckArgument( isAtom(), this );
 313   switch(d_sexprType) {
 314   case SEXPR_INTEGER:
 315     return d_integerValue.toString();
 316   case SEXPR_RATIONAL: {
 317     // We choose to represent rationals as decimal strings rather than
 318     // "numerator/denominator."  Perhaps an additional SEXPR_DECIMAL
 319     // could be added if we need both styles, even if it's backed by
 320     // the same Rational object.
 321     std::stringstream ss;
 322     ss << std::fixed << d_rationalValue.getDouble();
 323     return ss.str();
 324   }
 325   case SEXPR_STRING:
 326   case SEXPR_KEYWORD:
 327     return d_stringValue;
 328   case SEXPR_NOT_ATOM:
 329     return std::string();
 330   }
 331   return std::string();
 332
 333 }
 334
 335 const CVC4::Integer& SExpr::getIntegerValue() const {
 336   PrettyCheckArgument( isInteger(), this );
 337   return d_integerValue;
 338 }
 339
 340 const CVC4::Rational& SExpr::getRationalValue() const {
 341   PrettyCheckArgument( isRational(), this );
 342   return d_rationalValue;
 343 }
 344
 345 const std::vector<SExpr>& SExpr::getChildren() const {
 346   PrettyCheckArgument( !isAtom(), this );
 347   Assert( d_children != NULL );
 348   return *d_children;
 349 }
 350
 351 bool SExpr::operator==(const SExpr& s) const {
 352   if (d_sexprType == s.d_sexprType &&
 353       d_integerValue == s.d_integerValue &&
 354       d_rationalValue == s.d_rationalValue &&
 355       d_stringValue == s.d_stringValue) {
 356     if(d_children == NULL && s.d_children == NULL){
 357       return true;
 358     } else if(d_children != NULL && s.d_children != NULL){
 359       return getChildren() == s.getChildren();
 360     }
 361   }
 362   return false;
 363 }
 364
 365 bool SExpr::operator!=(const SExpr& s) const {
 366   return !(*this == s);
 367 }
 368
 369
 370 SExpr SExpr::parseAtom(const std::string& atom) {
 371   if(atom == "true"){
 372     return SExpr(true);
 373   } else if(atom == "false"){
 374     return SExpr(false);
 375   } else {
 376     try {
 377       Integer z(atom);
 378       return SExpr(z);
 379     }catch(std::invalid_argument&){
 380       // Fall through to the next case
 381     }
 382     try {
 383       Rational q(atom);
 384       return SExpr(q);
 385     }catch(std::invalid_argument&){
 386       // Fall through to the next case
 387     }
 388     return SExpr(atom);
 389   }
 390 }
 391
 392 SExpr SExpr::parseListOfAtoms(const std::vector<std::string>& atoms) {
 393   std::vector<SExpr> parsedAtoms;
 394   typedef std::vector<std::string>::const_iterator const_iterator;
 395   for(const_iterator i = atoms.begin(), i_end=atoms.end(); i != i_end; ++i){
 396     parsedAtoms.push_back(parseAtom(*i));
 397   }
 398   return SExpr(parsedAtoms);
 399 }
 400
 401 SExpr SExpr::parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists) {
 402   std::vector<SExpr> parsedListsOfAtoms;
 403   typedef std::vector< std::vector<std::string> >::const_iterator const_iterator;
 404   for(const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); i != i_end; ++i){
 405     parsedListsOfAtoms.push_back(parseListOfAtoms(*i));
 406   }
 407   return SExpr(parsedListsOfAtoms);
 408 }
 409
 410
 411
 412 }/* CVC4 namespace */