1 /********************* */
2 /*! \file expr_template.h
4 ** Original author: dejan
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): taking, cconway
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Public-facing expression interface.
16 ** Public-facing expression interface.
19 #include "cvc4_public.h"
21 #ifndef __CVC4__EXPR_H
22 #define __CVC4__EXPR_H
24 #include "expr/type.h"
31 // This is a hack, but an important one: if there's an error, the
32 // compiler directs the user to the template file instead of the
33 // generated one. We don't want the user to modify the generated one,
34 // since it'll get overwritten on a later build.
35 #line 36 "${template}"
39 // The internal expression representation
40 template <bool ref_count
>
46 class CVC4_PUBLIC ExprSetDepth
;
47 class CVC4_PUBLIC ExprPrintTypes
;
48 }/* CVC4::expr namespace */
51 * Exception thrown in the case of type-checking errors.
53 class CVC4_PUBLIC TypeCheckingException
: public Exception
{
57 /** The expression responsible for the error */
62 TypeCheckingException(): Exception() {}
63 TypeCheckingException(const Expr
& expr
, std::string message
);
67 /** Copy constructor */
68 TypeCheckingException(const TypeCheckingException
& t
);
71 ~TypeCheckingException() throw ();
74 * Get the Expr that caused the type-checking to fail.
77 Expr
getExpression() const;
79 /** Returns the message corresponding to the type-checking failure */
80 std::string
toString() const;
82 friend class ExprManager
;
86 * Class encapsulating CVC4 expressions and methods for constructing new
89 class CVC4_PUBLIC Expr
{
92 /** The internal expression representation */
93 NodeTemplate
<true>* d_node
;
95 /** The responsible expression manager */
96 ExprManager
* d_exprManager
;
99 * Constructor for internal purposes.
100 * @param em the expression manager that handles this expression
101 * @param node the actual expression node pointer
103 Expr(ExprManager
* em
, NodeTemplate
<true>* node
);
107 /** Default constructor, makes a null expression. */
111 * Copy constructor, makes a copy of a given expression
112 * @param e the expression to copy
117 * Initialize from an integer. Fails if the integer is not 0.
118 * NOTE: This is here purely to support the auto-initialization
119 * behavior of the ANTLR3 C backend. Should be removed if future
120 * versions of ANTLR fix the problem.
128 * Assignment operator, makes a copy of the given expression. If the
129 * expression managers of the two expressions differ, the expression of
130 * the given expression will be used.
131 * @param e the expression to assign
132 * @return the reference to this expression after assignment
134 Expr
& operator=(const Expr
& e
);
137 * Syntactic comparison operator. Returns true if expressions belong to the
138 * same expression manager and are syntactically identical.
139 * @param e the expression to compare to
140 * @return true if expressions are syntactically the same, false otherwise
142 bool operator==(const Expr
& e
) const;
145 * Syntactic dis-equality operator.
146 * @param e the expression to compare to
147 * @return true if expressions differ syntactically, false otherwise
149 bool operator!=(const Expr
& e
) const;
152 * Order comparison operator. The only invariant on the order of expressions
153 * is that the expressions that were created sooner will be smaller in the
154 * ordering than all the expressions created later. Null expression is the
155 * smallest element of the ordering. The behavior of the operator is
156 * undefined if the expressions come from two different expression managers.
157 * @param e the expression to compare to
158 * @return true if this expression is smaller than the given one
160 bool operator<(const Expr
& e
) const;
163 * Order comparison operator. The only invariant on the order of expressions
164 * is that the expressions that were created sooner will be smaller in the
165 * ordering than all the expressions created later. Null expression is the
166 * smallest element of the ordering. The behavior of the operator is
167 * undefined if the expressions come from two different expression managers.
168 * @param e the expression to compare to
169 * @return true if this expression is greater than the given one
171 bool operator>(const Expr
& e
) const;
174 * Order comparison operator. The only invariant on the order of expressions
175 * is that the expressions that were created sooner will be smaller in the
176 * ordering than all the expressions created later. Null expression is the
177 * smallest element of the ordering. The behavior of the operator is
178 * undefined if the expressions come from two different expression managers.
179 * @param e the expression to compare to
180 * @return true if this expression is smaller or equal to the given one
182 bool operator<=(const Expr
& e
) const { return !(*this > e
); }
185 * Order comparison operator. The only invariant on the order of expressions
186 * is that the expressions that were created sooner will be smaller in the
187 * ordering than all the expressions created later. Null expression is the
188 * smallest element of the ordering. The behavior of the operator is
189 * undefined if the expressions come from two different expression managers.
190 * @param e the expression to compare to
191 * @return true if this expression is greater or equal to the given one
193 bool operator>=(const Expr
& e
) const { return !(*this < e
); }
196 * Returns the kind of the expression (AND, PLUS ...).
197 * @return the kind of the expression
199 Kind
getKind() const;
202 * Returns the number of children of this expression.
203 * @return the number of children
205 size_t getNumChildren() const;
208 * Returns the i'th child of this expression.
209 * @param i the index of the child to retrieve
212 Expr
getChild(unsigned int i
) const;
215 * Check if this is an expression that has an operator.
216 * @return true if this expression has an operator
218 bool hasOperator() const;
221 * Get the operator of this expression.
222 * @throws IllegalArgumentException if it has no operator
223 * @return the operator of this expression
225 Expr
getOperator() const;
228 * Get the type for this Expr and optionally do type checking.
230 * Initial type computation will be near-constant time if
231 * type checking is not requested. Results are memoized, so that
232 * subsequent calls to getType() without type checking will be
235 * Initial type checking is linear in the size of the expression.
236 * Again, the results are memoized, so that subsequent calls to
237 * getType(), with or without type checking, will be constant
240 * NOTE: A TypeCheckingException can be thrown even when type
241 * checking is not requested. getType() will always return a
242 * valid and correct type and, thus, an exception will be thrown
243 * when no valid or correct type can be computed (e.g., if the
244 * arguments to a bit-vector operation aren't bit-vectors). When
245 * type checking is not requested, getType() will do the minimum
246 * amount of checking required to return a valid result.
248 * @param check whether we should check the type as we compute it
251 Type
getType(bool check
= false) const throw (TypeCheckingException
);
254 * Returns the string representation of the expression.
255 * @return a string representation of the expression
257 std::string
toString() const;
260 * Outputs the string representation of the expression to the stream.
261 * @param out the output stream
263 void toStream(std::ostream
& out
, int depth
= -1, bool types
= false) const;
266 * Check if this is a null expression.
267 * @return true if a null expression
272 * Check if this is a null expression.
273 * @return true if NOT a null expression
275 operator bool() const;
278 * Check if this is an expression representing a constant.
279 * @return true if a constant expression
281 bool isConst() const;
283 /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
285 * It has been decided for now to hold off on implementations of
286 * these functions, as they may only be needed in CNF conversion,
287 * where it's pointless to do a lazy isAtomic determination by
288 * searching through the DAG, and storing it, since the result will
289 * only be used once. For more details see the 4/27/2010 CVC4
290 * developer's meeting notes at:
292 * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
294 // bool containsDecision(); // is "atomic"
295 // bool properlyContainsDecision(); // maybe not atomic but all children are
297 /** Extract a constant of type T */
299 const T
& getConst() const;
302 * Returns the expression reponsible for this expression.
304 ExprManager
* getExprManager() const;
307 * IOStream manipulator to set the maximum depth of Exprs when
308 * pretty-printing. -1 means print to any depth. E.g.:
310 * // let a, b, c, and d be VARIABLEs
311 * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
312 * out << setdepth(3) << e;
314 * gives "(OR a b (AND c (NOT d)))", but
316 * out << setdepth(1) << [same expr as above]
318 * gives "(OR a b (...))"
320 typedef expr::ExprSetDepth setdepth
;
323 * IOStream manipulator to print type ascriptions or not.
325 * // let a, b, c, and d be variables of sort U
326 * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
329 * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
331 typedef expr::ExprPrintTypes printtypes
;
334 * Very basic pretty printer for Expr.
335 * This is equivalent to calling e.getNode().printAst(...)
336 * @param out output stream to print to.
337 * @param indent number of spaces to indent the formula by.
339 void printAst(std::ostream
& out
, int indent
= 0) const;
344 * Pretty printer for use within gdb
345 * This is not intended to be used outside of gdb.
346 * This writes to the ostream Warning() and immediately flushes
354 * Returns the actual internal node.
355 * @return the internal node
357 NodeTemplate
<true> getNode() const;
359 // Friend to access the actual internal expr information and private methods
360 friend class SmtEngine
;
361 friend class ExprManager
;
365 * Output operator for expressions
366 * @param out the stream to output to
367 * @param e the expression to output
370 std::ostream
& operator<<(std::ostream
& out
, const Expr
& e
) CVC4_PUBLIC
;
373 * Extending the expression with the capability to construct Boolean
376 class CVC4_PUBLIC BoolExpr
: public Expr
{
380 /** Default constructor, makes a null expression */
384 * Convert an expression to a Boolean expression
386 BoolExpr(const Expr
& e
);
389 * Negate this expression.
390 * @return the logical negation of this expression.
392 BoolExpr
notExpr() const;
395 * Conjunct the given expression to this expression.
396 * @param e the expression to conjunct
397 * @return the conjunction of this expression and e
399 BoolExpr
andExpr(const BoolExpr
& e
) const;
402 * Disjunct the given expression to this expression.
403 * @param e the expression to disjunct
404 * @return the disjunction of this expression and e
406 BoolExpr
orExpr(const BoolExpr
& e
) const;
409 * Make an exclusive or expression out of this expression and the given
411 * @param e the right side of the xor
412 * @return the xor of this expression and e
414 BoolExpr
xorExpr(const BoolExpr
& e
) const;
417 * Make an equivalence expression out of this expression and the given
419 * @param e the right side of the equivalence
420 * @return the equivalence expression
422 BoolExpr
iffExpr(const BoolExpr
& e
) const;
425 * Make an implication expression out of this expression and the given
427 * @param e the right side of the equivalence
428 * @return the equivalence expression
430 BoolExpr
impExpr(const BoolExpr
& e
) const;
433 * Make a Boolean if-then-else expression using this expression as the
434 * condition, and given the then and else parts
435 * @param then_e the then branch expression
436 * @param else_e the else branch expression
437 * @return the if-then-else expression
439 BoolExpr
iteExpr(const BoolExpr
& then_e
, const BoolExpr
& else_e
) const;
442 * Make a term if-then-else expression using this expression as the
443 * condition, and given the then and else parts
444 * @param then_e the then branch expression
445 * @param else_e the else branch expression
446 * @return the if-then-else expression
448 Expr
iteExpr(const Expr
& then_e
, const Expr
& else_e
) const;
454 * IOStream manipulator to set the maximum depth of Exprs when
455 * pretty-printing. -1 means print to any depth. E.g.:
457 * // let a, b, c, and d be VARIABLEs
458 * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
459 * out << setdepth(3) << e;
461 * gives "(OR a b (AND c (NOT d)))", but
463 * out << setdepth(1) << [same expr as above]
465 * gives "(OR a b (...))".
467 * The implementation of this class serves two purposes; it holds
468 * information about the depth setting (such as the index of the
469 * allocated word in ios_base), and serves also as the manipulator
472 class CVC4_PUBLIC ExprSetDepth
{
474 * The allocated index in ios_base for our depth setting.
476 static const int s_iosIndex
;
479 * The default depth to print, for ostreams that haven't yet had a
480 * setdepth() applied to them.
482 static const int s_defaultPrintDepth
= 3;
485 * When this manipulator is used, the depth is stored here.
491 * Construct a ExprSetDepth with the given depth.
493 ExprSetDepth(long depth
) : d_depth(depth
) {}
495 inline void applyDepth(std::ostream
& out
) {
496 out
.iword(s_iosIndex
) = d_depth
;
499 static inline long getDepth(std::ostream
& out
) {
500 long& l
= out
.iword(s_iosIndex
);
502 // set the default print depth on this ostream
503 l
= s_defaultPrintDepth
;
508 static inline void setDepth(std::ostream
& out
, long depth
) {
509 out
.iword(s_iosIndex
) = depth
;
514 * IOStream manipulator to print type ascriptions or not.
516 * // let a, b, c, and d be variables of sort U
517 * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
520 * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
522 class CVC4_PUBLIC ExprPrintTypes
{
524 * The allocated index in ios_base for our depth setting.
526 static const int s_iosIndex
;
529 * The default depth to print, for ostreams that haven't yet had a
530 * setdepth() applied to them.
532 static const int s_defaultPrintTypes
= false;
535 * When this manipulator is used, the setting is stored here.
541 * Construct a ExprPrintTypes with the given setting.
543 ExprPrintTypes(bool printTypes
) : d_printTypes(printTypes
) {}
545 inline void applyPrintTypes(std::ostream
& out
) {
546 out
.iword(s_iosIndex
) = d_printTypes
;
549 static inline bool getPrintTypes(std::ostream
& out
) {
550 return out
.iword(s_iosIndex
);
553 static inline void setPrintTypes(std::ostream
& out
, bool printTypes
) {
554 out
.iword(s_iosIndex
) = printTypes
;
558 }/* CVC4::expr namespace */
560 $
{getConst_instantiations
}
562 #line 388 "${template}"
567 * Sets the default print-types setting when pretty-printing an Expr
568 * to an ostream. Use like this:
570 * // let out be an ostream, e an Expr
571 * out << Expr::setdepth(n) << e << endl;
573 * The depth stays permanently (until set again) with the stream.
575 inline std::ostream
& operator<<(std::ostream
& out
, ExprSetDepth sd
) {
581 * Sets the default depth when pretty-printing a Expr to an ostream.
584 * // let out be an ostream, e an Expr
585 * out << Expr::setprinttypes(true) << e << endl;
587 * The setting stays permanently (until set again) with the stream.
589 inline std::ostream
& operator<<(std::ostream
& out
, ExprPrintTypes pt
) {
590 pt
.applyPrintTypes(out
);
594 }/* CVC4::expr namespace */
596 }/* CVC4 namespace */
598 #endif /* __CVC4__EXPR_H */