diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-09 00:35:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-09 00:35:38 +0000 |
commit | 700689a4e4ed42b5198816611eac5bcc1278284d (patch) | |
tree | 0d6029f9bc4f46a721930a27a47ac487771c452e /src/expr/expr_template.h | |
parent | a0411d4baad389ce88d4bd26edc8ed811625887c (diff) |
Dagification of output expressions.
By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables.
This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N
times, it is dagified; a setting of 0 turns off dagification entirely.
If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior
with --default-expr-dag=0 and let me know of the problem.
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r-- | src/expr/expr_template.h | 119 |
1 files changed, 109 insertions, 10 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 7a6c0179d..6cd476a5f 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -79,6 +79,7 @@ namespace smt { namespace expr { class CVC4_PUBLIC ExprSetDepth; class CVC4_PUBLIC ExprPrintTypes; + class CVC4_PUBLIC ExprDag; class CVC4_PUBLIC ExprSetLanguage; NodeTemplate<true> exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); @@ -400,7 +401,7 @@ public: * debugging expressions) * @param language the language in which to output */ - void toStream(std::ostream& out, int toDepth = -1, bool types = false, + void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AST) const; /** @@ -493,6 +494,11 @@ public: typedef expr::ExprPrintTypes printtypes; /** + * IOStream manipulator to print expressions as a DAG (or not). + */ + typedef expr::ExprDag dag; + + /** * IOStream manipulator to set the output language for Exprs. */ typedef expr::ExprSetLanguage setlanguage; @@ -722,13 +728,13 @@ public: */ class CVC4_PUBLIC ExprPrintTypes { /** - * The allocated index in ios_base for our depth setting. + * The allocated index in ios_base for our setting. */ static const int s_iosIndex; /** - * The default depth to print, for ostreams that haven't yet had a - * setdepth() applied to them. + * The default printtypes setting, for ostreams that haven't yet had a + * printtypes() applied to them. */ static const int s_defaultPrintTypes = false; @@ -782,6 +788,85 @@ public: };/* 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. + */ + ExprDag(size_t dag) : d_dag(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) + l = 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 */ + +/** * IOStream manipulator to set the output language for Exprs. */ class CVC4_PUBLIC ExprSetLanguage { @@ -857,13 +942,13 @@ public: ${getConst_instantiations} -#line 861 "${template}" +#line 938 "${template}" namespace expr { /** - * Sets the default print-types setting when pretty-printing an Expr - * to an ostream. Use like this: + * 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; @@ -876,11 +961,11 @@ inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) { } /** - * Sets the default depth when pretty-printing a Expr to an ostream. - * Use like this: + * 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::setprinttypes(true) << e << endl; + * out << Expr::printtypes(true) << e << endl; * * The setting stays permanently (until set again) with the stream. */ @@ -890,6 +975,20 @@ inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) { } /** + * 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; +} + +/** * Sets the output language when pretty-printing a Expr to an ostream. * Use like this: * |