src/util/sexpr.h

   1 /*********************                                                        */
   2 /*! \file sexpr.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Morgan Deters, Christopher L. Conway
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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  ** These are used when a simple, and obvious interface for basic
  16  ** expressions is appropriate.
  17  **
  18  ** These are quite ineffecient.
  19  ** These are totally disconnected from any ExprManager.
  20  ** These keep unique copies of all of their children.
  21  ** These are VERY overly verbose and keep much more data than is needed.
  22  **/
  23
  24 #include "cvc4_public.h"
  25
  26 #ifndef CVC4__SEXPR_H
  27 #define CVC4__SEXPR_H
  28
  29 #include <iomanip>
  30 #include <iosfwd>
  31 #include <string>
  32 #include <vector>
  33
  34 #include "base/exception.h"
  35 #include "options/language.h"
  36 #include "util/integer.h"
  37 #include "util/rational.h"
  38
  39 namespace CVC4 {
  40
  41 class CVC4_PUBLIC SExprKeyword {
  42  public:
  43   SExprKeyword(const std::string& s) : d_str(s) {}
  44   const std::string& getString() const { return d_str; }
  45
  46  private:
  47   std::string d_str;
  48 }; /* class SExpr::Keyword */
  49
  50 /**
  51  * A simple S-expression. An S-expression is either an atom with a
  52  * string value, or a list of other S-expressions.
  53  */
  54 class CVC4_PUBLIC SExpr {
  55  public:
  56   typedef SExprKeyword Keyword;
  57
  58   SExpr();
  59   SExpr(const SExpr&);
  60   SExpr& operator=(const SExpr& other);
  61   ~SExpr();
  62
  63   SExpr(const CVC4::Integer& value);
  64
  65   SExpr(int value);
  66   SExpr(long int value);
  67   SExpr(unsigned int value);
  68   SExpr(unsigned long int value);
  69
  70   SExpr(const CVC4::Rational& value);
  71
  72   SExpr(const std::string& value);
  73
  74   /**
  75    * This constructs a string expression from a const char* value.
  76    * This cannot be removed in order to support SExpr("foo").
  77    * Given the other constructors this SExpr("foo") converts to bool.
  78    * instead of SExpr(string("foo")).
  79    */
  80   SExpr(const char* value);
  81
  82   /**
  83    * This adds a convenience wrapper to SExpr to cast from bools.
  84    * This is internally handled as the strings "true" and "false"
  85    */
  86   SExpr(bool value);
  87   SExpr(const Keyword& value);
  88   SExpr(const std::vector<SExpr>& children);
  89
  90   /** Is this S-expression an atom? */
  91   bool isAtom() const;
  92
  93   /** Is this S-expression an integer? */
  94   bool isInteger() const;
  95
  96   /** Is this S-expression a rational? */
  97   bool isRational() const;
  98
  99   /** Is this S-expression a string? */
 100   bool isString() const;
 101
 102   /** Is this S-expression a keyword? */
 103   bool isKeyword() const;
 104
 105   /**
 106    * This wraps the toStream() printer.
 107    * NOTE: toString() and getValue() may differ on Keywords based on
 108    * the current language set in expr.
 109    */
 110   std::string toString() const;
 111
 112   /**
 113    * Get the string value of this S-expression. This will cause an
 114    * error if this S-expression is not an atom.
 115    */
 116   std::string getValue() const;
 117
 118   /**
 119    * Get the integer value of this S-expression. This will cause an
 120    * error if this S-expression is not an integer.
 121    */
 122   const CVC4::Integer& getIntegerValue() const;
 123
 124   /**
 125    * Get the rational value of this S-expression. This will cause an
 126    * error if this S-expression is not a rational.
 127    */
 128   const CVC4::Rational& getRationalValue() const;
 129
 130   /**
 131    * Get the children of this S-expression. This will cause an error
 132    * if this S-expression is not a list.
 133    */
 134   const std::vector<SExpr>& getChildren() const;
 135
 136   /** Is this S-expression equal to another? */
 137   bool operator==(const SExpr& s) const;
 138
 139   /** Is this S-expression different from another? */
 140   bool operator!=(const SExpr& s) const;
 141
 142   /**
 143    * This returns the best match in the following order:
 144    * match atom with
 145    *  "true", "false" -> SExpr(value)
 146    * | is and integer -> as integer
 147    * | is a rational -> as rational
 148    * | _ -> SExpr()
 149    */
 150   static SExpr parseAtom(const std::string& atom);
 151
 152   /**
 153    * Parses a list of atoms.
 154    */
 155   static SExpr parseListOfAtoms(const std::vector<std::string>& atoms);
 156
 157   /**
 158    * Parses a list of list of atoms.
 159    */
 160   static SExpr parseListOfListOfAtoms(
 161       const std::vector<std::vector<std::string> >& atoms_lists);
 162
 163   /**
 164    * Outputs the SExpr onto the ostream out. This version reads defaults to the
 165    * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level
 166    * is
 167    * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise.
 168    */
 169   static void toStream(std::ostream& out, const SExpr& sexpr);
 170
 171   /**
 172    * Outputs the SExpr onto the ostream out. This version sets the indent level
 173    * to 2 if PrettySExprs::getPrettySExprs() is on.
 174    */
 175   static void toStream(std::ostream& out, const SExpr& sexpr,
 176                        OutputLanguage language);
 177
 178   /**
 179    * Outputs the SExpr onto the ostream out.
 180    * If the languageQuotesKeywords(language), then a top level keyword, " X",
 181    * that needs quoting according to the SMT2 language standard is printed with
 182    * quotes, "| X|".
 183    * Otherwise this prints using toStreamRec().
 184    *
 185    * TIM: Keywords that are children are not currently quoted. This seems
 186    * incorrect but I am just reproduicing the old behavior even if it does not
 187    * make
 188    * sense.
 189    */
 190   static void toStream(std::ostream& out, const SExpr& sexpr,
 191                        OutputLanguage language, int indent);
 192
 193  private:
 194   /**
 195    * Simple printer for SExpr to an ostream.
 196    * The current implementation is language independent.
 197    */
 198   static void toStreamRec(std::ostream& out, const SExpr& sexpr,
 199                           OutputLanguage language, int indent);
 200
 201   /** Returns true if this language quotes Keywords when printing. */
 202   static bool languageQuotesKeywords(OutputLanguage language);
 203
 204   enum SExprTypes {
 205     SEXPR_STRING,
 206     SEXPR_KEYWORD,
 207     SEXPR_INTEGER,
 208     SEXPR_RATIONAL,
 209     SEXPR_NOT_ATOM
 210   } d_sexprType;
 211
 212   /** The value of an atomic integer-valued S-expression. */
 213   CVC4::Integer d_integerValue;
 214
 215   /** The value of an atomic rational-valued S-expression. */
 216   CVC4::Rational d_rationalValue;
 217
 218   /** The value of an atomic S-expression. */
 219   std::string d_stringValue;
 220
 221   typedef std::vector<SExpr> SExprVector;
 222
 223   /**
 224    * The children of a list S-expression.
 225    * Whenever the SExpr isAtom() holds, this points at NULL.
 226    *
 227    * This should be a pointer in case the implementation of vector<SExpr> ever
 228    * directly contained or allocated an SExpr. If this happened this would
 229    * trigger,
 230    * either the size being infinite or SExpr() being an infinite loop.
 231    */
 232   SExprVector* d_children;
 233 }; /* class SExpr */
 234
 235 /** Prints an SExpr. */
 236 std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC;
 237
 238 /**
 239  * IOStream manipulator to pretty-print SExprs.
 240  */
 241 class CVC4_PUBLIC PrettySExprs {
 242   /**
 243    * The allocated index in ios_base for our setting.
 244    */
 245   static const int s_iosIndex;
 246
 247   /**
 248    * When this manipulator is used, the setting is stored here.
 249    */
 250   bool d_prettySExprs;
 251
 252  public:
 253   /**
 254    * Construct a PrettySExprs with the given setting.
 255    */
 256   PrettySExprs(bool prettySExprs) : d_prettySExprs(prettySExprs) {}
 257
 258   inline void applyPrettySExprs(std::ostream& out) {
 259     out.iword(s_iosIndex) = d_prettySExprs;
 260   }
 261
 262   static inline bool getPrettySExprs(std::ostream& out) {
 263     return out.iword(s_iosIndex);
 264   }
 265
 266   static inline void setPrettySExprs(std::ostream& out, bool prettySExprs) {
 267     out.iword(s_iosIndex) = prettySExprs;
 268   }
 269
 270   /**
 271    * Set the pretty-sexprs state on the output stream for the current
 272    * stack scope.  This makes sure the old state is reset on the
 273    * stream after normal OR exceptional exit from the scope, using the
 274    * RAII C++ idiom.
 275    */
 276   class Scope {
 277     std::ostream& d_out;
 278     bool d_oldPrettySExprs;
 279
 280    public:
 281     inline Scope(std::ostream& out, bool prettySExprs)
 282         : d_out(out), d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) {
 283       PrettySExprs::setPrettySExprs(out, prettySExprs);
 284     }
 285
 286     inline ~Scope() { PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); }
 287
 288   }; /* class PrettySExprs::Scope */
 289
 290 }; /* class PrettySExprs */
 291
 292 /**
 293  * Sets the default pretty-sexprs setting for an ostream.  Use like this:
 294  *
 295  *   // let out be an ostream, s an SExpr
 296  *   out << PrettySExprs(true) << s << endl;
 297  *
 298  * The setting stays permanently (until set again) with the stream.
 299  */
 300 std::ostream& operator<<(std::ostream& out, PrettySExprs ps);
 301
 302 } /* CVC4 namespace */
 303
 304 #endif /* CVC4__SEXPR_H */