1 /********************* */
2 /*! \file expr_template.h
4 ** Original author: Morgan Deters
5 ** Major contributors: Dejan Jovanovic
6 ** Minor contributors (to current version): Liana Hadarean, Kshitij Bansal, Tim King, Christopher L. Conway
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Public-facing expression interface.
14 ** Public-facing expression interface.
17 #include "cvc4_public.h"
19 // putting the constant-payload #includes up here allows circularity
20 // (some of them may require a completely-defined Expr type). This
21 // way, those #includes can forward-declare some stuff to get Expr's
22 // getConst<> template instantiations correct, and then #include
23 // "expr.h" safely, then go on to completely declare their own stuff.
26 #ifndef __CVC4__EXPR_H
27 #define __CVC4__EXPR_H
34 #include "util/exception.h"
35 #include "util/language.h"
36 #include "util/hash.h"
37 #include "expr/options.h"
39 // This is a hack, but an important one: if there's an error, the
40 // compiler directs the user to the template file instead of the
41 // generated one. We don't want the user to modify the generated one,
42 // since it'll get overwritten on a later build.
43 #line 44 "${template}"
47 // The internal expression representation
48 template <bool ref_count
>
57 class TypeCheckingException
;
58 class TypeCheckingExceptionPrivate
;
63 }/* CVC4::expr::pickle namespace */
64 }/* CVC4::expr namespace */
68 }/* CVC4::prop namespace */
70 struct ExprManagerMapCollection
;
72 struct ExprHashFunction
;
75 class SmtEnginePrivate
;
76 }/* CVC4::smt namespace */
79 class CVC4_PUBLIC ExprSetDepth
;
80 class CVC4_PUBLIC ExprPrintTypes
;
81 class CVC4_PUBLIC ExprDag
;
82 class CVC4_PUBLIC ExprSetLanguage
;
85 }/* CVC4::expr namespace */
88 * Exception thrown in the case of type-checking errors.
90 class CVC4_PUBLIC TypeCheckingException
: public Exception
{
92 friend class SmtEngine
;
93 friend class smt::SmtEnginePrivate
;
97 /** The expression responsible for the error */
102 TypeCheckingException() throw() : Exception() {}
103 TypeCheckingException(ExprManager
* em
,
104 const TypeCheckingExceptionPrivate
* exc
) throw();
108 TypeCheckingException(const Expr
& expr
, std::string message
) throw();
110 /** Copy constructor */
111 TypeCheckingException(const TypeCheckingException
& t
) throw();
114 ~TypeCheckingException() throw();
117 * Get the Expr that caused the type-checking to fail.
121 Expr
getExpression() const throw();
124 * Returns the message corresponding to the type-checking failure.
125 * We prefer toStream() to toString() because that keeps the expr-depth
126 * and expr-language settings present in the stream.
128 void toStream(std::ostream
& out
) const throw();
130 friend class ExprManager
;
131 };/* class TypeCheckingException */
134 * Exception thrown in case of failure to export
136 class CVC4_PUBLIC ExportUnsupportedException
: public Exception
{
138 ExportUnsupportedException() throw():
139 Exception("export unsupported") {
141 ExportUnsupportedException(const char* msg
) throw():
144 };/* class DatatypeExportUnsupportedException */
146 std::ostream
& operator<<(std::ostream
& out
,
147 const TypeCheckingException
& e
) CVC4_PUBLIC
;
150 * Output operator for expressions
151 * @param out the stream to output to
152 * @param e the expression to output
155 std::ostream
& operator<<(std::ostream
& out
, const Expr
& e
) CVC4_PUBLIC
;
157 // for hash_maps, hash_sets..
158 struct ExprHashFunction
{
159 size_t operator()(CVC4::Expr e
) const;
160 };/* struct ExprHashFunction */
163 * Class encapsulating CVC4 expressions and methods for constructing new
166 class CVC4_PUBLIC Expr
{
168 /** The internal expression representation */
169 NodeTemplate
<true>* d_node
;
171 /** The responsible expression manager */
172 ExprManager
* d_exprManager
;
175 * Constructor for internal purposes.
177 * @param em the expression manager that handles this expression
178 * @param node the actual expression node pointer
180 Expr(ExprManager
* em
, NodeTemplate
<true>* node
);
184 /** Default constructor, makes a null expression. */
188 * Copy constructor, makes a copy of a given expression
190 * @param e the expression to copy
198 * Assignment operator, makes a copy of the given expression. If the
199 * expression managers of the two expressions differ, the expression of
200 * the given expression will be used.
202 * @param e the expression to assign
203 * @return the reference to this expression after assignment
205 Expr
& operator=(const Expr
& e
);
208 * Syntactic comparison operator. Returns true if expressions belong to the
209 * same expression manager and are syntactically identical.
211 * @param e the expression to compare to
212 * @return true if expressions are syntactically the same, false otherwise
214 bool operator==(const Expr
& e
) const;
217 * Syntactic disequality operator.
219 * @param e the expression to compare to
220 * @return true if expressions differ syntactically, false otherwise
222 bool operator!=(const Expr
& e
) const;
225 * Order comparison operator. The only invariant on the order of expressions
226 * is that the expressions that were created sooner will be smaller in the
227 * ordering than all the expressions created later. Null expression is the
228 * smallest element of the ordering. The behavior of the operator is
229 * undefined if the expressions come from two different expression managers.
231 * @param e the expression to compare to
232 * @return true if this expression is smaller than the given one
234 bool operator<(const Expr
& e
) const;
237 * Order comparison operator. The only invariant on the order of expressions
238 * is that the expressions that were created sooner will be smaller in the
239 * ordering than all the expressions created later. Null expression is the
240 * smallest element of the ordering. The behavior of the operator is
241 * undefined if the expressions come from two different expression managers.
243 * @param e the expression to compare to
244 * @return true if this expression is greater than the given one
246 bool operator>(const Expr
& e
) const;
249 * Order comparison operator. The only invariant on the order of expressions
250 * is that the expressions that were created sooner will be smaller in the
251 * ordering than all the expressions created later. Null expression is the
252 * smallest element of the ordering. The behavior of the operator is
253 * undefined if the expressions come from two different expression managers.
255 * @param e the expression to compare to
256 * @return true if this expression is smaller or equal to the given one
258 bool operator<=(const Expr
& e
) const { return !(*this > e
); }
261 * Order comparison operator. The only invariant on the order of expressions
262 * is that the expressions that were created sooner will be smaller in the
263 * ordering than all the expressions created later. Null expression is the
264 * smallest element of the ordering. The behavior of the operator is
265 * undefined if the expressions come from two different expression managers.
267 * @param e the expression to compare to
268 * @return true if this expression is greater or equal to the given one
270 bool operator>=(const Expr
& e
) const { return !(*this < e
); }
273 * Get the ID of this expression (used for the comparison operators).
275 * @return an identifier uniquely identifying the value this
278 unsigned long getId() const;
281 * Returns the kind of the expression (AND, PLUS ...).
283 * @return the kind of the expression
285 Kind
getKind() const;
288 * Returns the number of children of this expression.
290 * @return the number of children
292 size_t getNumChildren() const;
295 * Returns the i'th child of this expression.
297 * @param i the index of the child to retrieve
300 Expr
operator[](unsigned i
) const;
303 * Returns the children of this Expr.
305 std::vector
<Expr
> getChildren() const {
306 return std::vector
<Expr
>(begin(), end());
310 * Returns the Boolean negation of this Expr.
312 Expr
notExpr() const;
315 * Returns the conjunction of this expression and
316 * the given expression.
318 Expr
andExpr(const Expr
& e
) const;
321 * Returns the disjunction of this expression and
322 * the given expression.
324 Expr
orExpr(const Expr
& e
) const;
327 * Returns the exclusive disjunction of this expression and
328 * the given expression.
330 Expr
xorExpr(const Expr
& e
) const;
333 * Returns the Boolean equivalence of this expression and
334 * the given expression.
336 Expr
iffExpr(const Expr
& e
) const;
339 * Returns the implication of this expression and
340 * the given expression.
342 Expr
impExpr(const Expr
& e
) const;
345 * Returns the if-then-else expression with this expression
346 * as the Boolean condition and the given expressions as
347 * the "then" and "else" expressions.
349 Expr
iteExpr(const Expr
& then_e
, const Expr
& else_e
) const;
352 * Iterator type for the children of an Expr.
354 class const_iterator
: public std::iterator
<std::input_iterator_tag
, Expr
> {
355 ExprManager
* d_exprManager
;
358 explicit const_iterator(ExprManager
*, void*);
360 friend class Expr
;// to access void* constructor
364 const_iterator(const const_iterator
& it
);
365 const_iterator
& operator=(const const_iterator
& it
);
367 bool operator==(const const_iterator
& it
) const;
368 bool operator!=(const const_iterator
& it
) const {
369 return !(*this == it
);
371 const_iterator
& operator++();
372 const_iterator
operator++(int);
373 Expr
operator*() const;
374 };/* class Expr::const_iterator */
377 * Returns an iterator to the first child of this Expr.
379 const_iterator
begin() const;
382 * Returns an iterator to one-off-the-last child of this Expr.
384 const_iterator
end() const;
387 * Check if this is an expression that has an operator.
389 * @return true if this expression has an operator
391 bool hasOperator() const;
394 * Get the operator of this expression.
396 * @throws IllegalArgumentException if it has no operator
397 * @return the operator of this expression
399 Expr
getOperator() const;
402 * Get the type for this Expr and optionally do type checking.
404 * Initial type computation will be near-constant time if
405 * type checking is not requested. Results are memoized, so that
406 * subsequent calls to getType() without type checking will be
409 * Initial type checking is linear in the size of the expression.
410 * Again, the results are memoized, so that subsequent calls to
411 * getType(), with or without type checking, will be constant
414 * NOTE: A TypeCheckingException can be thrown even when type
415 * checking is not requested. getType() will always return a
416 * valid and correct type and, thus, an exception will be thrown
417 * when no valid or correct type can be computed (e.g., if the
418 * arguments to a bit-vector operation aren't bit-vectors). When
419 * type checking is not requested, getType() will do the minimum
420 * amount of checking required to return a valid result.
422 * @param check whether we should check the type as we compute it
425 Type
getType(bool check
= false) const throw (TypeCheckingException
);
428 * Substitute "replacement" in for "e".
430 Expr
substitute(Expr e
, Expr replacement
) const;
433 * Substitute "replacements" in for "exes".
435 Expr
substitute(const std::vector
<Expr
> exes
,
436 const std::vector
<Expr
>& replacements
) const;
439 * Substitute pairs of (ex,replacement) from the given map.
441 Expr
substitute(const std::hash_map
<Expr
, Expr
, ExprHashFunction
> map
) const;
444 * Returns the string representation of the expression.
445 * @return a string representation of the expression
447 std::string
toString() const;
450 * Outputs the string representation of the expression to the stream.
452 * @param out the stream to serialize this expression to
453 * @param toDepth the depth to which to print this expression, or -1
455 * @param types set to true to ascribe types to the output
456 * expressions (might break language compliance, but good for
457 * debugging expressions)
458 * @param dag the dagification threshold to use (0 == off)
459 * @param language the language in which to output
461 void toStream(std::ostream
& out
, int toDepth
= -1, bool types
= false, size_t dag
= 1,
462 OutputLanguage language
= language::output::LANG_AST
) const;
465 * Check if this is a null expression.
467 * @return true if a null expression
472 * Check if this is an expression representing a variable.
474 * @return true if a variable expression
476 bool isVariable() const;
479 * Check if this is an expression representing a constant.
481 * @return true if a constant expression
483 bool isConst() const;
485 /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
487 * It has been decided for now to hold off on implementations of
488 * these functions, as they may only be needed in CNF conversion,
489 * where it's pointless to do a lazy isAtomic determination by
490 * searching through the DAG, and storing it, since the result will
491 * only be used once. For more details see the 4/27/2010 CVC4
492 * developer's meeting notes at:
494 * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
496 // bool containsDecision(); // is "atomic"
497 // bool properlyContainsDecision(); // maybe not atomic but all children are
499 /** Extract a constant of type T */
501 const T
& getConst() const;
504 * Returns the expression reponsible for this expression.
506 ExprManager
* getExprManager() const;
509 * Maps this Expr into one for a different ExprManager, using
510 * variableMap for the translation and extending it with any new
513 Expr
exportTo(ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
, uint32_t flags
= 0) const;
516 * IOStream manipulator to set the maximum depth of Exprs when
517 * pretty-printing. -1 means print to any depth. E.g.:
519 * // let a, b, c, and d be VARIABLEs
520 * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
521 * out << setdepth(3) << e;
523 * gives "(OR a b (AND c (NOT d)))", but
525 * out << setdepth(1) << [same expr as above]
527 * gives "(OR a b (...))"
529 typedef expr::ExprSetDepth setdepth
;
532 * IOStream manipulator to print type ascriptions or not.
534 * // let a, b, c, and d be variables of sort U
535 * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
536 * out << printtypes(true) << e;
538 * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
540 * out << printtypes(false) << [same expr as above]
542 * gives "(OR a b (AND c (NOT d)))"
544 typedef expr::ExprPrintTypes printtypes
;
547 * IOStream manipulator to print expressions as a DAG (or not).
549 typedef expr::ExprDag dag
;
552 * IOStream manipulator to set the output language for Exprs.
554 typedef expr::ExprSetLanguage setlanguage
;
557 * Very basic pretty printer for Expr.
558 * This is equivalent to calling e.getNode().printAst(...)
559 * @param out output stream to print to.
560 * @param indent number of spaces to indent the formula by.
562 void printAst(std::ostream
& out
, int indent
= 0) const;
567 * Pretty printer for use within gdb
568 * This is not intended to be used outside of gdb.
569 * This writes to the ostream Warning() and immediately flushes
575 * Returns the actual internal node.
576 * @return the internal node
578 NodeTemplate
<true> getNode() const throw();
581 * Returns the actual internal node as a TNode.
582 * @return the internal node
584 NodeTemplate
<false> getTNode() const throw();
586 // Friend to access the actual internal expr information and private methods
587 friend class SmtEngine
;
588 friend class smt::SmtEnginePrivate
;
589 friend class ExprManager
;
590 friend class NodeManager
;
591 friend class TypeCheckingException
;
592 friend class expr::pickle::Pickler
;
593 friend class prop::TheoryProxy
;
594 friend class expr::ExportPrivate
;
595 friend std::ostream
& CVC4::operator<<(std::ostream
& out
, const Expr
& e
);
596 template <bool ref_count
> friend class NodeTemplate
;
603 * IOStream manipulator to set the maximum depth of Exprs when
604 * pretty-printing. -1 means print to any depth. E.g.:
606 * // let a, b, c, and d be VARIABLEs
607 * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
608 * out << setdepth(3) << e;
610 * gives "(OR a b (AND c (NOT d)))", but
612 * out << setdepth(1) << [same expr as above]
614 * gives "(OR a b (...))".
616 * The implementation of this class serves two purposes; it holds
617 * information about the depth setting (such as the index of the
618 * allocated word in ios_base), and serves also as the manipulator
621 class CVC4_PUBLIC ExprSetDepth
{
623 * The allocated index in ios_base for our depth setting.
625 static const int s_iosIndex
;
628 * The default depth to print, for ostreams that haven't yet had a
629 * setdepth() applied to them.
631 static const int s_defaultPrintDepth
= -1;
634 * When this manipulator is used, the depth is stored here.
640 * Construct a ExprSetDepth with the given depth.
642 ExprSetDepth(long depth
) : d_depth(depth
) {}
644 inline void applyDepth(std::ostream
& out
) {
645 out
.iword(s_iosIndex
) = d_depth
;
648 static inline long getDepth(std::ostream
& out
) {
649 long& l
= out
.iword(s_iosIndex
);
651 // set the default print depth on this ostream
652 if(&Options::current() != NULL
) {
653 l
= options::defaultExprDepth();
656 // if called from outside the library, we may not have options
657 // available to us at this point (or perhaps the output language
658 // is not set in Options). Default to something reasonable, but
659 // don't set "l" since that would make it "sticky" for this
661 return s_defaultPrintDepth
;
667 static inline void setDepth(std::ostream
& out
, long depth
) {
668 out
.iword(s_iosIndex
) = depth
;
672 * Set the expression depth on the output stream for the current
673 * stack scope. This makes sure the old depth is reset on the stream
674 * after normal OR exceptional exit from the scope, using the RAII
683 inline Scope(std::ostream
& out
, long depth
) :
685 d_oldDepth(ExprSetDepth::getDepth(out
)) {
686 ExprSetDepth::setDepth(out
, depth
);
690 ExprSetDepth::setDepth(d_out
, d_oldDepth
);
693 };/* class ExprSetDepth::Scope */
695 };/* class ExprSetDepth */
698 * IOStream manipulator to print type ascriptions or not.
700 * // let a, b, c, and d be variables of sort U
701 * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
704 * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
706 class CVC4_PUBLIC ExprPrintTypes
{
708 * The allocated index in ios_base for our setting.
710 static const int s_iosIndex
;
713 * When this manipulator is used, the setting is stored here.
719 * Construct a ExprPrintTypes with the given setting.
721 ExprPrintTypes(bool printTypes
) : d_printTypes(printTypes
) {}
723 inline void applyPrintTypes(std::ostream
& out
) {
724 out
.iword(s_iosIndex
) = d_printTypes
;
727 static inline bool getPrintTypes(std::ostream
& out
) {
728 return out
.iword(s_iosIndex
);
731 static inline void setPrintTypes(std::ostream
& out
, bool printTypes
) {
732 out
.iword(s_iosIndex
) = printTypes
;
736 * Set the print-types state on the output stream for the current
737 * stack scope. This makes sure the old state is reset on the
738 * stream after normal OR exceptional exit from the scope, using the
743 bool d_oldPrintTypes
;
747 inline Scope(std::ostream
& out
, bool printTypes
) :
749 d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out
)) {
750 ExprPrintTypes::setPrintTypes(out
, printTypes
);
754 ExprPrintTypes::setPrintTypes(d_out
, d_oldPrintTypes
);
757 };/* class ExprPrintTypes::Scope */
759 };/* class ExprPrintTypes */
762 * IOStream manipulator to print expressions as a dag (or not).
764 class CVC4_PUBLIC ExprDag
{
766 * The allocated index in ios_base for our setting.
768 static const int s_iosIndex
;
771 * The default setting, for ostreams that haven't yet had a
772 * dag() applied to them.
774 static const size_t s_defaultDag
= 1;
777 * When this manipulator is used, the setting is stored here.
783 * Construct a ExprDag with the given setting (dagification on or off).
785 explicit ExprDag(bool dag
) : d_dag(dag
? 1 : 0) {}
788 * Construct a ExprDag with the given setting (letify only common
789 * subexpressions that appear more than 'dag' times). dag <= 0 means
792 explicit ExprDag(int dag
) : d_dag(dag
< 0 ? 0 : dag
) {}
794 inline void applyDag(std::ostream
& out
) {
795 // (offset by one to detect whether default has been set yet)
796 out
.iword(s_iosIndex
) = static_cast<long>(d_dag
) + 1;
799 static inline size_t getDag(std::ostream
& out
) {
800 long& l
= out
.iword(s_iosIndex
);
802 // set the default dag setting on this ostream
803 // (offset by one to detect whether default has been set yet)
804 if(&Options::current() != NULL
) {
805 l
= options::defaultDagThresh() + 1;
808 // if called from outside the library, we may not have options
809 // available to us at this point (or perhaps the output language
810 // is not set in Options). Default to something reasonable, but
811 // don't set "l" since that would make it "sticky" for this
813 return s_defaultDag
+ 1;
816 return static_cast<size_t>(l
- 1);
819 static inline void setDag(std::ostream
& out
, size_t dag
) {
820 // (offset by one to detect whether default has been set yet)
821 out
.iword(s_iosIndex
) = static_cast<long>(dag
) + 1;
825 * Set the dag state on the output stream for the current
826 * stack scope. This makes sure the old state is reset on the
827 * stream after normal OR exceptional exit from the scope, using the
836 inline Scope(std::ostream
& out
, size_t dag
) :
838 d_oldDag(ExprDag::getDag(out
)) {
839 ExprDag::setDag(out
, dag
);
843 ExprDag::setDag(d_out
, d_oldDag
);
846 };/* class ExprDag::Scope */
848 };/* class ExprDag */
851 * IOStream manipulator to set the output language for Exprs.
853 class CVC4_PUBLIC ExprSetLanguage
{
855 * The allocated index in ios_base for our depth setting.
857 static const int s_iosIndex
;
860 * The default language to use, for ostreams that haven't yet had a
861 * setlanguage() applied to them and where the current Options
862 * information isn't available.
864 static const int s_defaultOutputLanguage
= language::output::LANG_AST
;
867 * When this manipulator is used, the setting is stored here.
869 OutputLanguage d_language
;
873 * Construct a ExprSetLanguage with the given setting.
875 ExprSetLanguage(OutputLanguage l
) : d_language(l
) {}
877 inline void applyLanguage(std::ostream
& out
) {
878 // (offset by one to detect whether default has been set yet)
879 out
.iword(s_iosIndex
) = int(d_language
) + 1;
882 static inline OutputLanguage
getLanguage(std::ostream
& out
) {
883 long& l
= out
.iword(s_iosIndex
);
885 // set the default language on this ostream
886 // (offset by one to detect whether default has been set yet)
887 if(&Options::current() != NULL
) {
888 l
= options::outputLanguage() + 1;
890 if(l
<= 0 || l
> language::output::LANG_MAX
) {
891 // if called from outside the library, we may not have options
892 // available to us at this point (or perhaps the output language
893 // is not set in Options). Default to something reasonable, but
894 // don't set "l" since that would make it "sticky" for this
896 return OutputLanguage(s_defaultOutputLanguage
);
899 return OutputLanguage(l
- 1);
902 static inline void setLanguage(std::ostream
& out
, OutputLanguage l
) {
903 // (offset by one to detect whether default has been set yet)
904 out
.iword(s_iosIndex
) = int(l
) + 1;
908 * Set a language on the output stream for the current stack scope.
909 * This makes sure the old language is reset on the stream after
910 * normal OR exceptional exit from the scope, using the RAII C++
915 OutputLanguage d_oldLanguage
;
919 inline Scope(std::ostream
& out
, OutputLanguage language
) :
921 d_oldLanguage(ExprSetLanguage::getLanguage(out
)) {
922 ExprSetLanguage::setLanguage(out
, language
);
926 ExprSetLanguage::setLanguage(d_out
, d_oldLanguage
);
929 };/* class ExprSetLanguage::Scope */
931 };/* class ExprSetLanguage */
933 }/* CVC4::expr namespace */
935 $
{getConst_instantiations
}
937 #line 938 "${template}"
942 * Sets the default depth when pretty-printing a Expr to an ostream.
945 * // let out be an ostream, e an Expr
946 * out << Expr::setdepth(n) << e << endl;
948 * The depth stays permanently (until set again) with the stream.
950 inline std::ostream
& operator<<(std::ostream
& out
, ExprSetDepth sd
) {
956 * Sets the default print-types setting when pretty-printing an Expr
957 * to an ostream. Use like this:
959 * // let out be an ostream, e an Expr
960 * out << Expr::printtypes(true) << e << endl;
962 * The setting stays permanently (until set again) with the stream.
964 inline std::ostream
& operator<<(std::ostream
& out
, ExprPrintTypes pt
) {
965 pt
.applyPrintTypes(out
);
970 * Sets the default dag setting when pretty-printing a Expr to an ostream.
973 * // let out be an ostream, e an Expr
974 * out << Expr::dag(true) << e << endl;
976 * The setting stays permanently (until set again) with the stream.
978 inline std::ostream
& operator<<(std::ostream
& out
, ExprDag d
) {
984 * Sets the output language when pretty-printing a Expr to an ostream.
987 * // let out be an ostream, e an Expr
988 * out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl;
990 * The setting stays permanently (until set again) with the stream.
992 inline std::ostream
& operator<<(std::ostream
& out
, ExprSetLanguage l
) {
993 l
.applyLanguage(out
);
997 }/* CVC4::expr namespace */
999 inline size_t ExprHashFunction::operator()(CVC4::Expr e
) const {
1000 return (size_t) e
.getId();
1003 }/* CVC4 namespace */
1005 #endif /* __CVC4__EXPR_H */