From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 29 Jun 2010 22:42:40 +0000 (+0000)
Subject: add --default-expr-depth=N command line parameter, expose setdepth() to public interface
X-Git-Tag: cvc5-1.0.0~8972
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4206a75e7a1635d04bb69084404a75670e164b62;p=cvc5.git

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

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.
  */
@@ -244,6 +248,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(...)
@@ -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
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index c3c57cf94..2a1b1d0fc 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -31,6 +31,7 @@
 #include "util/output.h"
 #include "util/options.h"
 #include "parser/parser_options.h"
+#include "expr/expr.h"
 
 #include "cvc4autoconfig.h"
 #include "main.h"
@@ -66,7 +67,8 @@ enum OptionValue {
   NO_CHECKING,
   USE_MMAP,
   SHOW_CONFIG,
-  STRICT_PARSING
+  STRICT_PARSING,
+  DEFAULT_EXPR_DEPTH
 };/* enum OptionValue */
 
 /**
@@ -110,6 +112,7 @@ static struct option cmdlineOptions[] = {
   { "parse-only" , no_argument      , NULL, PARSE_ONLY  },
   { "mmap",        no_argument      , NULL, USE_MMAP    },
   { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
+  { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
 };/* if you add things to the above, please remember to update usage.h! */
 
 /** Full argv[0] */
@@ -219,6 +222,17 @@ throw(OptionException) {
       opts->strictParsing = true;
       break;
 
+    case DEFAULT_EXPR_DEPTH: {
+        int depth = atoi(optarg);
+        Debug.getStream() << Expr::setdepth(depth);
+        Trace.getStream() << Expr::setdepth(depth);
+        Notice.getStream() << Expr::setdepth(depth);
+        Chat.getStream() << Expr::setdepth(depth);
+        Message.getStream() << Expr::setdepth(depth);
+        Warning.getStream() << Expr::setdepth(depth);
+      }
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/main/usage.h b/src/main/usage.h
index 4da37749b..982dd240e 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -47,7 +47,9 @@ CVC4 options:\n\
    --quiet | -q    decrease verbosity (repeatable)\n\
    --trace | -t    tracing for something (e.g. --trace pushpop)\n\
    --debug | -d    debugging for something (e.g. --debug arith), implies -t\n\
-   --stats         give statistics on exit\n"
+   --stats         give statistics on exit\n\
+   --strict-parsing FIXME\n\
+   --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n"
 #endif
 ;
 
diff --git a/src/util/output.h b/src/util/output.h
index f27ec24da..651f6b607 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -116,6 +116,7 @@ public:
   bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Debug */
 
 /** The debug output singleton */
@@ -141,6 +142,7 @@ public:
   std::ostream& operator()() { return *d_os; }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Warning */
 
 /** The warning output singleton */
@@ -162,6 +164,7 @@ public:
   std::ostream& operator()() { return *d_os; }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Message */
 
 /** The message output singleton */
@@ -183,6 +186,7 @@ public:
   std::ostream& operator()() { return *d_os; }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Notice */
 
 /** The notice output singleton */
@@ -204,6 +208,7 @@ public:
   std::ostream& operator()() { return *d_os; }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Chat */
 
 /** The chat output singleton */
@@ -270,6 +275,7 @@ public:
   bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
 
   void setStream(std::ostream& os) { d_os = &os; }
+  std::ostream& getStream() { return *d_os; }
 };/* class Trace */
 
 /** The trace output singleton */
@@ -321,6 +327,7 @@ public:
   bool isOn(std::string tag) { return false; }
 
   void setStream(std::ostream& os) {}
+  std::ostream& getStream() { return null_os; }
 };/* class NullDebugC */
 
 /**
@@ -341,6 +348,7 @@ public:
   std::ostream& operator()() { return null_os; }
 
   void setStream(std::ostream& os) {}
+  std::ostream& getStream() { return null_os; }
 };/* class NullC */
 
 extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC;