add --default-expr-depth=N command line parameter, expose setdepth() to public interface

2 files changed, 98 insertions, 78 deletions

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 73aa666e6..1723f0258 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -42,6 +42,10 @@ class NodeTemplate;
 
 class Expr;
 
+namespace expr {
+  class NodeSetDepth;
+}/* CVC4::expr namespace */
+
 /**
  * Exception thrown in the case of type-checking errors.
  */
@@ -245,6 +249,22 @@ public:
   ExprManager* getExprManager() const;
 
   /**
+   * 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 (...))"
+   */
+  typedef expr::NodeSetDepth setdepth;
+
+  /**
    * Very basic pretty printer for Expr.
    * This is equivalent to calling e.getNode().printAst(...)
    * @param out output stream to print to.
@@ -364,6 +384,84 @@ public:
 
 ${getConst_instantiations}
 
+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 */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_H */
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