diff options
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r-- | src/expr/expr_template.h | 97 |
1 files changed, 83 insertions, 14 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 29164ffa5..2eac4ab62 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -26,6 +26,7 @@ #include <stdint.h> #include "util/exception.h" +#include "util/language.h" ${includes} @@ -33,7 +34,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 37 "${template}" +#line 38 "${template}" namespace CVC4 { @@ -45,6 +46,8 @@ class Expr; class ExprManager; class SmtEngine; class Type; +class TypeCheckingException; +class TypeCheckingExceptionPrivate; namespace smt { class SmtEnginePrivate; @@ -53,6 +56,7 @@ namespace smt { namespace expr { class CVC4_PUBLIC ExprSetDepth; class CVC4_PUBLIC ExprPrintTypes; + class CVC4_PUBLIC ExprSetLanguage; }/* CVC4::expr namespace */ /** @@ -61,6 +65,7 @@ namespace expr { class CVC4_PUBLIC TypeCheckingException : public Exception { friend class SmtEngine; + friend class smt::SmtEnginePrivate; private: @@ -69,8 +74,10 @@ private: protected: - TypeCheckingException(): Exception() {} + TypeCheckingException() : Exception() {} TypeCheckingException(const Expr& expr, std::string message); + TypeCheckingException(ExprManager* em, + const TypeCheckingExceptionPrivate* exc); public: @@ -97,6 +104,14 @@ std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) CVC4_PUBLIC; /** + * Output operator for expressions + * @param out the stream to output to + * @param e the expression to output + * @return the stream + */ +std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC; + +/** * Class encapsulating CVC4 expressions and methods for constructing new * expressions. */ @@ -281,7 +296,7 @@ public: * type checking is not requested, getType() will do the minimum * amount of checking required to return a valid result. * - * @param check whether we should check the type as we compute it + * @param check whether we should check the type as we compute it * (default: false) */ Type getType(bool check = false) const throw (TypeCheckingException); @@ -296,7 +311,8 @@ public: * Outputs the string representation of the expression to the stream. * @param out the output stream */ - void toStream(std::ostream& out, int depth = -1, bool types = false) const; + void toStream(std::ostream& out, int depth = -1, bool types = false, + OutputLanguage lang = language::output::LANG_AST) const; /** * Check if this is a null expression. @@ -367,6 +383,11 @@ public: typedef expr::ExprPrintTypes printtypes; /** + * IOStream manipulator to set the output language for Exprs. + */ + typedef expr::ExprSetLanguage setlanguage; + + /** * Very basic pretty printer for Expr. * This is equivalent to calling e.getNode().printAst(...) * @param out output stream to print to. @@ -402,15 +423,10 @@ protected: friend class SmtEngine; friend class smt::SmtEnginePrivate; friend class ExprManager; -}; + friend class TypeCheckingException; + friend std::ostream& operator<<(std::ostream& out, const Expr& e); -/** - * Output operator for expressions - * @param out the stream to output to - * @param e the expression to output - * @return the stream - */ -std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC; +};/* class Expr */ /** * Extending the expression with the capability to construct Boolean @@ -551,7 +567,7 @@ public: static inline void setDepth(std::ostream& out, long depth) { out.iword(s_iosIndex) = depth; } -}; +};/* class ExprSetDepth */ /** * IOStream manipulator to print type ascriptions or not. @@ -598,11 +614,50 @@ public: } };/* class ExprPrintTypes */ +/** + * IOStream manipulator to set the output language for Exprs. + */ +class CVC4_PUBLIC ExprSetLanguage { + /** + * The allocated index in ios_base for our depth setting. + */ + static const int s_iosIndex; + + /** + * The default language to use, for ostreams that haven't yet had a + * setlanguage() applied to them. + */ + static const int s_defaultLanguage = language::output::LANG_AST; + + /** + * When this manipulator is used, the setting is stored here. + */ + OutputLanguage d_language; + +public: + /** + * Construct a ExprSetLanguage with the given setting. + */ + ExprSetLanguage(OutputLanguage l) : d_language(l) {} + + inline void applyLanguage(std::ostream& out) { + out.iword(s_iosIndex) = int(d_language); + } + + static inline OutputLanguage getLanguage(std::ostream& out) { + return OutputLanguage(out.iword(s_iosIndex)); + } + + static inline void setLanguage(std::ostream& out, OutputLanguage l) { + out.iword(s_iosIndex) = int(l); + } +};/* class ExprSetLanguage */ + }/* CVC4::expr namespace */ ${getConst_instantiations} -#line 566 "${template}" +#line 659 "${template}" namespace expr { @@ -634,6 +689,20 @@ inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) { return out; } +/** + * Sets the output language when pretty-printing a Expr to an ostream. + * Use like this: + * + * // let out be an ostream, e an Expr + * out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl; + * + * The setting stays permanently (until set again) with the stream. + */ +inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) { + l.applyLanguage(out); + return out; +} + }/* CVC4::expr namespace */ // for hash_maps, hash_sets.. |