9c80a1b1f9781875d8bbdd0f571d757ef156b6e0
1 /********************* */
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-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
12 ** \brief Simple representation of S-expressions
14 ** Simple representation of S-expressions.
15 ** These are used when a simple, and obvious interface for basic
16 ** expressions is appropraite.
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.
24 #include "cvc4_public.h"
26 #ifndef __CVC4__SEXPR_H
27 #define __CVC4__SEXPR_H
34 #include "base/exception.h"
35 #include "options/language.h"
36 #include "util/integer.h"
37 #include "util/rational.h"
41 class CVC4_PUBLIC SExprKeyword
{
44 SExprKeyword(const std::string
& s
) : d_str(s
) {}
45 const std::string
& getString() const { return d_str
; }
46 };/* class SExpr::Keyword */
49 * A simple S-expression. An S-expression is either an atom with a
50 * string value, or a list of other S-expressions.
52 class CVC4_PUBLIC SExpr
{
55 typedef SExprKeyword Keyword
;
59 SExpr
& operator=(const SExpr
& other
);
62 SExpr(const CVC4::Integer
& value
);
65 SExpr(long int value
);
66 SExpr(unsigned int value
);
67 SExpr(unsigned long int value
);
69 SExpr(const CVC4::Rational
& value
);
71 SExpr(const std::string
& value
);
74 * This constructs a string expression from a const char* value.
75 * This cannot be removed in order to support SExpr("foo").
76 * Given the other constructors this SExpr("foo") converts to bool.
77 * instead of SExpr(string("foo")).
79 SExpr(const char* value
);
82 * This adds a convenience wrapper to SExpr to cast from bools.
83 * This is internally handled as the strings "true" and "false"
86 SExpr(const Keyword
& value
);
87 SExpr(const std::vector
<SExpr
>& children
);
89 /** Is this S-expression an atom? */
92 /** Is this S-expression an integer? */
93 bool isInteger() const;
95 /** Is this S-expression a rational? */
96 bool isRational() const;
98 /** Is this S-expression a string? */
99 bool isString() const;
101 /** Is this S-expression a keyword? */
102 bool isKeyword() const;
105 * This wraps the toStream() printer.
106 * NOTE: toString() and getValue() may differ on Keywords based on
107 * the current language set in expr.
109 std::string
toString() const;
112 * Get the string value of this S-expression. This will cause an
113 * error if this S-expression is not an atom.
115 std::string
getValue() const;
118 * Get the integer value of this S-expression. This will cause an
119 * error if this S-expression is not an integer.
121 const CVC4::Integer
& getIntegerValue() const;
124 * Get the rational value of this S-expression. This will cause an
125 * error if this S-expression is not a rational.
127 const CVC4::Rational
& getRationalValue() const;
130 * Get the children of this S-expression. This will cause an error
131 * if this S-expression is not a list.
133 const std::vector
<SExpr
>& getChildren() const;
135 /** Is this S-expression equal to another? */
136 bool operator==(const SExpr
& s
) const;
138 /** Is this S-expression different from another? */
139 bool operator!=(const SExpr
& s
) const;
143 * This returns the best match in the following order:
145 * "true", "false" -> SExpr(value)
146 * | is and integer -> as integer
147 * | is a rational -> as rational
150 static SExpr
parseAtom(const std::string
& atom
);
153 * Parses a list of atoms.
155 static SExpr
parseListOfAtoms(const std::vector
<std::string
>& atoms
);
158 * Parses a list of list of atoms.
160 static SExpr
parseListOfListOfAtoms(const std::vector
< std::vector
<std::string
> >& atoms_lists
);
164 * Outputs the SExpr onto the ostream out. This version reads defaults to the
165 * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level is
166 * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise.
168 static void toStream(std::ostream
& out
, const SExpr
& sexpr
) throw();
171 * Outputs the SExpr onto the ostream out. This version sets the indent level
172 * to 2 if PrettySExprs::getPrettySExprs() is on.
174 static void toStream(std::ostream
& out
, const SExpr
& sexpr
, OutputLanguage language
) throw();
177 * Outputs the SExpr onto the ostream out.
178 * If the languageQuotesKeywords(language), then a top level keyword, " X",
179 * that needs quoting according to the SMT2 language standard is printed with
181 * Otherwise this prints using toStreamRec().
183 * TIM: Keywords that are children are not currently quoted. This seems
184 * incorrect but I am just reproduicing the old behavior even if it does not make
187 static void toStream(std::ostream
& out
, const SExpr
& sexpr
, OutputLanguage language
, int indent
) throw();
192 * Simple printer for SExpr to an ostream.
193 * The current implementation is language independent.
195 static void toStreamRec(std::ostream
& out
, const SExpr
& sexpr
, OutputLanguage language
, int indent
) throw();
198 /** Returns true if this language quotes Keywords when printing. */
199 static bool languageQuotesKeywords(OutputLanguage language
);
209 /** The value of an atomic integer-valued S-expression. */
210 CVC4::Integer d_integerValue
;
212 /** The value of an atomic rational-valued S-expression. */
213 CVC4::Rational d_rationalValue
;
215 /** The value of an atomic S-expression. */
216 std::string d_stringValue
;
218 typedef std::vector
<SExpr
> SExprVector
;
221 * The children of a list S-expression.
222 * Whenever the SExpr isAtom() holds, this points at NULL.
224 * This should be a pointer in case the implementation of vector<SExpr> ever
225 * directly contained or allocated an SExpr. If this happened this would trigger,
226 * either the size being infinite or SExpr() being an infinite loop.
228 SExprVector
* d_children
;
231 /** Prints an SExpr. */
232 std::ostream
& operator<<(std::ostream
& out
, const SExpr
& sexpr
) CVC4_PUBLIC
;
235 * IOStream manipulator to pretty-print SExprs.
237 class CVC4_PUBLIC PrettySExprs
{
239 * The allocated index in ios_base for our setting.
241 static const int s_iosIndex
;
244 * When this manipulator is used, the setting is stored here.
250 * Construct a PrettySExprs with the given setting.
252 PrettySExprs(bool prettySExprs
) : d_prettySExprs(prettySExprs
) {}
254 inline void applyPrettySExprs(std::ostream
& out
) {
255 out
.iword(s_iosIndex
) = d_prettySExprs
;
258 static inline bool getPrettySExprs(std::ostream
& out
) {
259 return out
.iword(s_iosIndex
);
262 static inline void setPrettySExprs(std::ostream
& out
, bool prettySExprs
) {
263 out
.iword(s_iosIndex
) = prettySExprs
;
267 * Set the pretty-sexprs state on the output stream for the current
268 * stack scope. This makes sure the old state is reset on the
269 * stream after normal OR exceptional exit from the scope, using the
274 bool d_oldPrettySExprs
;
278 inline Scope(std::ostream
& out
, bool prettySExprs
) :
280 d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out
)) {
281 PrettySExprs::setPrettySExprs(out
, prettySExprs
);
285 PrettySExprs::setPrettySExprs(d_out
, d_oldPrettySExprs
);
288 };/* class PrettySExprs::Scope */
290 };/* class PrettySExprs */
293 * Sets the default pretty-sexprs setting for an ostream. Use like this:
295 * // let out be an ostream, s an SExpr
296 * out << PrettySExprs(true) << s << endl;
298 * The setting stays permanently (until set again) with the stream.
300 std::ostream
& operator<<(std::ostream
& out
, PrettySExprs ps
);
303 }/* CVC4 namespace */
305 #endif /* __CVC4__SEXPR_H */