From 4206a75e7a1635d04bb69084404a75670e164b62 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 29 Jun 2010 22:42:40 +0000 Subject: [PATCH] add --default-expr-depth=N command line parameter, expose setdepth() to public interface --- src/expr/expr_template.h | 98 ++++++++++++++++++++++++++++++++++++++++ src/expr/node.h | 78 -------------------------------- src/main/getopt.cpp | 16 ++++++- src/main/usage.h | 4 +- src/util/output.h | 8 ++++ 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. */ @@ -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 */ -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; -- 2.30.2