summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_template.h98
-rw-r--r--src/expr/node.h78
-rw-r--r--src/main/getopt.cpp16
-rw-r--r--src/main/usage.h4
-rw-r--r--src/util/output.h8
5 files changed, 124 insertions, 80 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
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback