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 | |
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')
-rw-r--r-- | src/expr/command.cpp | 5 | ||||
-rw-r--r-- | src/expr/command.h | 2 | ||||
-rw-r--r-- | src/expr/expr.i | 1 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 5 | ||||
-rw-r--r-- | src/expr/expr_template.h | 119 | ||||
-rw-r--r-- | src/expr/node.h | 30 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_value.h | 14 | ||||
-rw-r--r-- | src/expr/type_node.h | 15 |
9 files changed, 172 insertions, 23 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 78d04f000..ae24f4984 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -43,6 +43,7 @@ std::ostream& operator<<(std::ostream& out, const Command& c) throw() { c.toStream(out, Node::setdepth::getDepth(out), Node::printtypes::getPrintTypes(out), + Node::dag::getDag(out), Node::setlanguage::getLanguage(out)); return out; } @@ -101,9 +102,9 @@ std::string Command::toString() const throw() { return ss.str(); } -void Command::toStream(std::ostream& out, int toDepth, bool types, +void Command::toStream(std::ostream& out, int toDepth, bool types, size_t dag, OutputLanguage language) const throw() { - Printer::getPrinter(language)->toStream(out, this, toDepth, types); + Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag); } void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() { diff --git a/src/expr/command.h b/src/expr/command.h index 19d1f16e7..98046c242 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -205,7 +205,7 @@ public: virtual void invoke(SmtEngine* smtEngine) throw() = 0; virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); - virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, + virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AST) const throw(); std::string toString() const throw(); diff --git a/src/expr/expr.i b/src/expr/expr.i index 6ed7f2d25..9b6c55703 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -9,6 +9,7 @@ %ignore CVC4::expr::operator<<(std::ostream&, ExprSetDepth); %ignore CVC4::expr::operator<<(std::ostream&, ExprPrintTypes); +%ignore CVC4::expr::operator<<(std::ostream&, ExprDag); %ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage); %rename(assign) CVC4::Expr::operator=(const Expr&); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index d0f5fde9e..c70fed889 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -45,6 +45,7 @@ namespace expr { const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc(); +const int ExprDag::s_iosIndex = std::ios_base::xalloc(); const int ExprSetLanguage::s_iosIndex = std::ios_base::xalloc(); }/* CVC4::expr namespace */ @@ -416,10 +417,10 @@ bool Expr::isConst() const { return d_node->isConst(); } -void Expr::toStream(std::ostream& out, int depth, bool types, +void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag, OutputLanguage language) const { ExprManagerScope ems(*this); - d_node->toStream(out, depth, types, language); + d_node->toStream(out, depth, types, dag, language); } Node Expr::getNode() const throw() { 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: * diff --git a/src/expr/node.h b/src/expr/node.h index 3532116bc..a61944433 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -803,10 +803,10 @@ public: * (might break language compliance, but good for debugging expressions) * @param language the language in which to output */ - inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, + inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AST) const { assertTNodeNotExpired(); - d_nv->toStream(out, toDepth, types, language); + d_nv->toStream(out, toDepth, types, dag, language); } /** @@ -837,6 +837,11 @@ public: typedef expr::ExprPrintTypes printtypes; /** + * IOStream manipulator to print expressions as DAGs (or not). + */ + typedef expr::ExprDag dag; + + /** * IOStream manipulator to set the output language for Exprs. */ typedef expr::ExprSetLanguage setlanguage; @@ -885,6 +890,7 @@ inline std::ostream& operator<<(std::ostream& out, TNode n) { n.toStream(out, Node::setdepth::getDepth(out), Node::printtypes::getPrintTypes(out), + Node::dag::getDag(out), Node::setlanguage::getLanguage(out)); return out; } @@ -1468,6 +1474,16 @@ bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) con */ static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) { Warning() << Node::setdepth(-1) + << Node::printtypes(false) + << Node::dag(true) + << Node::setlanguage(language::output::LANG_AST) + << n << std::endl; + Warning().flush(); +} +static void __attribute__((used)) debugPrintNodeNoDag(const NodeTemplate<true>& n) { + Warning() << Node::setdepth(-1) + << Node::printtypes(false) + << Node::dag(false) << Node::setlanguage(language::output::LANG_AST) << n << std::endl; Warning().flush(); @@ -1479,6 +1495,16 @@ static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) { Warning() << Node::setdepth(-1) + << Node::printtypes(false) + << Node::dag(true) + << Node::setlanguage(language::output::LANG_AST) + << n << std::endl; + Warning().flush(); +} +static void __attribute__((used)) debugPrintTNodeNoDag(const NodeTemplate<false>& n) { + Warning() << Node::setdepth(-1) + << Node::printtypes(false) + << Node::dag(false) << Node::setlanguage(language::output::LANG_AST) << n << std::endl; Warning().flush(); diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 970d2e0fc..dbf706c45 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -45,14 +45,14 @@ string NodeValue::toString() const { return ss.str(); } -void NodeValue::toStream(std::ostream& out, int toDepth, bool types, +void NodeValue::toStream(std::ostream& out, int toDepth, bool types, size_t dag, OutputLanguage language) const { // Ensure that this node value is live for the length of this call. // It really breaks things badly if we don't have a nonzero ref // count, even just for printing. RefCountGuard guard(this); - Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types); + Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types, dag); } void NodeValue::printAst(std::ostream& out, int ind) const { diff --git a/src/expr/node_value.h b/src/expr/node_value.h index e5ecfbc48..657fabeb5 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -267,7 +267,7 @@ public: } std::string toString() const; - 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::output::LANG_AST) const; static inline unsigned kindToDKind(Kind k) { @@ -487,6 +487,7 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) { nv.toStream(out, Node::setdepth::getDepth(out), Node::printtypes::getPrintTypes(out), + Node::dag::getDag(out), Node::setlanguage::getLanguage(out)); return out; } @@ -501,11 +502,20 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) { */ static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) { Warning() << Node::setdepth(-1) + << Node::printtypes(false) + << Node::dag(true) + << Node::setlanguage(language::output::LANG_AST) + << *nv << std::endl; + Warning().flush(); +} +static void __attribute__((used)) debugPrintNodeValueNoDag(const expr::NodeValue* nv) { + Warning() << Node::setdepth(-1) + << Node::printtypes(false) + << Node::dag(false) << Node::setlanguage(language::output::LANG_AST) << *nv << std::endl; Warning().flush(); } - static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) { nv->printAst(Warning(), 0); Warning().flush(); diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 482da2814..bfbedde88 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -389,9 +389,9 @@ public: * (might break language compliance, but good for debugging expressions) * @param language the language in which to output */ - inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, + inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AST) const { - d_nv->toStream(out, toDepth, types, language); + d_nv->toStream(out, toDepth, types, dag, language); } /** @@ -636,6 +636,7 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { n.toStream(out, Node::setdepth::getDepth(out), Node::printtypes::getPrintTypes(out), + Node::dag::getDag(out), Node::setlanguage::getLanguage(out)); return out; } @@ -980,6 +981,16 @@ inline const SubrangeBounds& TypeNode::getSubrangeBounds() const { */ static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) { Warning() << Node::setdepth(-1) + << Node::printtypes(false) + << Node::dag(true) + << Node::setlanguage(language::output::LANG_AST) + << n << std::endl; + Warning().flush(); +} +static void __attribute__((used)) debugPrintTypeNodeNoDag(const TypeNode& n) { + Warning() << Node::setdepth(-1) + << Node::printtypes(false) + << Node::dag(false) << Node::setlanguage(language::output::LANG_AST) << n << std::endl; Warning().flush(); |