diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-06-29 22:42:40 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-06-29 22:42:40 +0000 |
commit | 4206a75e7a1635d04bb69084404a75670e164b62 (patch) | |
tree | 2aeafc38957feec648c30f556eee1792935304ef /src/expr/node.h | |
parent | b1200db566d19132a3f0861eeef35f3c0aaa0a08 (diff) |
add --default-expr-depth=N command line parameter, expose setdepth() to public interface
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 78 |
1 files changed, 0 insertions, 78 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index cfaab142d..8618bce4d 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -511,84 +511,6 @@ private: };/* class NodeTemplate<ref_count> */ -namespace expr { - -/** - * IOStream manipulator to set the maximum depth of Nodes when - * pretty-printing. -1 means print to any depth. E.g.: - * - * // let a, b, c, and d be VARIABLEs - * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d))) - * out << setdepth(3) << n; - * - * gives "(OR a b (AND c (NOT d)))", but - * - * out << setdepth(1) << [same node 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 NodeSetDepth { - /** - * 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 = 3; - - /** - * When this manipulator is - */ - long d_depth; - -public: - /** - * Construct a NodeSetDepth with the given depth. - */ - NodeSetDepth(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 - l = s_defaultPrintDepth; - } - return l; - } - - static inline void setDepth(std::ostream& out, long depth) { - out.iword(s_iosIndex) = depth; - } -}; - -/** - * Sets the default depth when pretty-printing a Node to an ostream. - * Use like this: - * - * // let out be an ostream, n a Node - * out << Node::setdepth(n) << n << endl; - * - * The depth stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, NodeSetDepth sd) { - sd.applyDepth(out); - return out; -} - -}/* CVC4::expr namespace */ - /** * Serializes a given node to the given stream. * @param out the output stream to use |