diff options
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r-- | src/expr/expr_template.h | 338 |
1 files changed, 0 insertions, 338 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 2e2f17742..7d82cb222 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -33,7 +33,6 @@ ${includes} #include <string> #include "base/exception.h" -#include "options/expr_options.h" #include "options/language.h" #include "util/hash.h" @@ -77,10 +76,6 @@ namespace smt { }/* CVC4::smt namespace */ namespace expr { - class CVC4_PUBLIC ExprSetDepth; - class CVC4_PUBLIC ExprPrintTypes; - class CVC4_PUBLIC ExprDag; - class ExportPrivate; }/* CVC4::expr namespace */ @@ -513,42 +508,6 @@ public: Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const; /** - * IOStream manipulator to set the maximum depth of Exprs when - * pretty-printing. -1 means print to any depth. E.g.: - * - * // let a, b, c, and d be VARIABLEs - * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << setdepth(3) << e; - * - * gives "(OR a b (AND c (NOT d)))", but - * - * out << setdepth(1) << [same expr as above] - * - * gives "(OR a b (...))" - */ - typedef expr::ExprSetDepth setdepth; - - /** - * IOStream manipulator to print type ascriptions or not. - * - * // let a, b, c, and d be variables of sort U - * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << printtypes(true) << e; - * - * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but - * - * out << printtypes(false) << [same expr as above] - * - * gives "(OR a b (AND c (NOT d)))" - */ - typedef expr::ExprPrintTypes printtypes; - - /** - * IOStream manipulator to print expressions as a DAG (or not). - */ - typedef expr::ExprDag dag; - - /** * Very basic pretty printer for Expr. * This is equivalent to calling e.getNode().printAst(...) * @param out output stream to print to. @@ -592,307 +551,10 @@ private: };/* class Expr */ -namespace expr { - -/** - * IOStream manipulator to set the maximum depth of Exprs when - * pretty-printing. -1 means print to any depth. E.g.: - * - * // let a, b, c, and d be VARIABLEs - * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << setdepth(3) << e; - * - * gives "(OR a b (AND c (NOT d)))", but - * - * out << setdepth(1) << [same expr as above] - * - * gives "(OR a b (...))". - * - * The implementation of this class serves two purposes; it holds - * information about the depth setting (such as the index of the - * allocated word in ios_base), and serves also as the manipulator - * itself (as above). - */ -class CVC4_PUBLIC ExprSetDepth { - /** - * The allocated index in ios_base for our depth setting. - */ - static const int s_iosIndex; - - /** - * The default depth to print, for ostreams that haven't yet had a - * setdepth() applied to them. - */ - static const int s_defaultPrintDepth = -1; - - /** - * When this manipulator is used, the depth is stored here. - */ - long d_depth; - -public: - /** - * Construct a ExprSetDepth with the given depth. - */ - ExprSetDepth(long depth) : d_depth(depth) {} - - inline void applyDepth(std::ostream& out) { - out.iword(s_iosIndex) = d_depth; - } - - static inline long getDepth(std::ostream& out) { - long& l = out.iword(s_iosIndex); - if(l == 0) { - // set the default print depth on this ostream - if(not Options::isCurrentNull()) { - l = options::defaultExprDepth(); - } - if(l == 0) { - // if called from outside the library, we may not have options - // available to us at this point (or perhaps the output language - // is not set in Options). Default to something reasonable, but - // don't set "l" since that would make it "sticky" for this - // stream. - return s_defaultPrintDepth; - } - } - return l; - } - - static inline void setDepth(std::ostream& out, long depth) { - out.iword(s_iosIndex) = depth; - } - - /** - * Set the expression depth on the output stream for the current - * stack scope. This makes sure the old depth is reset on the stream - * after normal OR exceptional exit from the scope, using the RAII - * C++ idiom. - */ - class Scope { - std::ostream& d_out; - long d_oldDepth; - - public: - - inline Scope(std::ostream& out, long depth) : - d_out(out), - d_oldDepth(ExprSetDepth::getDepth(out)) { - ExprSetDepth::setDepth(out, depth); - } - - inline ~Scope() { - ExprSetDepth::setDepth(d_out, d_oldDepth); - } - - };/* class ExprSetDepth::Scope */ - -};/* class ExprSetDepth */ - -/** - * IOStream manipulator to print type ascriptions or not. - * - * // let a, b, c, and d be variables of sort U - * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << e; - * - * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but - */ -class CVC4_PUBLIC ExprPrintTypes { - /** - * The allocated index in ios_base for our setting. - */ - static const int s_iosIndex; - - /** - * When this manipulator is used, the setting is stored here. - */ - bool d_printTypes; - -public: - /** - * Construct a ExprPrintTypes with the given setting. - */ - ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {} - - inline void applyPrintTypes(std::ostream& out) { - out.iword(s_iosIndex) = d_printTypes; - } - - static inline bool getPrintTypes(std::ostream& out) { - return out.iword(s_iosIndex); - } - - static inline void setPrintTypes(std::ostream& out, bool printTypes) { - out.iword(s_iosIndex) = printTypes; - } - - /** - * Set the print-types state on the output stream for the current - * stack scope. This makes sure the old state is reset on the - * stream after normal OR exceptional exit from the scope, using the - * RAII C++ idiom. - */ - class Scope { - std::ostream& d_out; - bool d_oldPrintTypes; - - public: - - inline Scope(std::ostream& out, bool printTypes) : - d_out(out), - d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) { - ExprPrintTypes::setPrintTypes(out, printTypes); - } - - inline ~Scope() { - ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes); - } - - };/* class ExprPrintTypes::Scope */ - -};/* class ExprPrintTypes */ - -/** - * IOStream manipulator to print expressions as a dag (or not). - */ -class CVC4_PUBLIC ExprDag { - /** - * The allocated index in ios_base for our setting. - */ - static const int s_iosIndex; - - /** - * The default setting, for ostreams that haven't yet had a - * dag() applied to them. - */ - static const size_t s_defaultDag = 1; - - /** - * When this manipulator is used, the setting is stored here. - */ - size_t d_dag; - -public: - /** - * Construct a ExprDag with the given setting (dagification on or off). - */ - explicit ExprDag(bool dag) : d_dag(dag ? 1 : 0) {} - - /** - * Construct a ExprDag with the given setting (letify only common - * subexpressions that appear more than 'dag' times). dag <= 0 means - * don't dagify. - */ - explicit ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {} - - inline void applyDag(std::ostream& out) { - // (offset by one to detect whether default has been set yet) - out.iword(s_iosIndex) = static_cast<long>(d_dag) + 1; - } - - static inline size_t getDag(std::ostream& out) { - long& l = out.iword(s_iosIndex); - if(l == 0) { - // set the default dag setting on this ostream - // (offset by one to detect whether default has been set yet) - if(not Options::isCurrentNull()) { - l = options::defaultDagThresh() + 1; - } - if(l == 0) { - // if called from outside the library, we may not have options - // available to us at this point (or perhaps the output language - // is not set in Options). Default to something reasonable, but - // don't set "l" since that would make it "sticky" for this - // stream. - return s_defaultDag + 1; - } - } - return static_cast<size_t>(l - 1); - } - - static inline void setDag(std::ostream& out, size_t dag) { - // (offset by one to detect whether default has been set yet) - out.iword(s_iosIndex) = static_cast<long>(dag) + 1; - } - - /** - * Set the dag state on the output stream for the current - * stack scope. This makes sure the old state is reset on the - * stream after normal OR exceptional exit from the scope, using the - * RAII C++ idiom. - */ - class Scope { - std::ostream& d_out; - size_t d_oldDag; - - public: - - inline Scope(std::ostream& out, size_t dag) : - d_out(out), - d_oldDag(ExprDag::getDag(out)) { - ExprDag::setDag(out, dag); - } - - inline ~Scope() { - ExprDag::setDag(d_out, d_oldDag); - } - - };/* class ExprDag::Scope */ - -};/* class ExprDag */ -}/* CVC4::expr namespace */ - ${getConst_instantiations} #line 939 "${template}" -namespace expr { - -/** - * Sets the default depth when pretty-printing a Expr to an ostream. - * Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::setdepth(n) << e << endl; - * - * The depth stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) { - sd.applyDepth(out); - return out; -} - -/** - * Sets the default print-types setting when pretty-printing an Expr - * to an ostream. Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::printtypes(true) << e << endl; - * - * The setting stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) { - pt.applyPrintTypes(out); - return out; -} - -/** - * Sets the default dag setting when pretty-printing a Expr to an ostream. - * Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::dag(true) << e << endl; - * - * The setting stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, ExprDag d) { - d.applyDag(out); - return out; -} - -}/* CVC4::expr namespace */ - inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { return (size_t) e.getId(); } |