diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
commit | 83a143b1dd78e5d7f07666fbec1362dd60348116 (patch) | |
tree | 08400222d94f4760c7155fea787ac7e78b7b0dfc /src/expr/expr_template.h | |
parent | a8566c313e9b5eb8248eaeea642a9c72c803dcfa (diff) |
* Added white-box TheoryEngine test that tests the rewriter
* Added regression documentation to test/regress/README
* Added ability to print types of vars in expr printouts
with iomanipulator Node::printtypes(true)... for example,
Warning() << Node::printtypes(true) << n << std::endl;
* Types-printing can be specified on the command line with
--print-expr-types
* Improved type handling facilities and theoryOf().
For now, SORT_TYPE moved from builtin theory to UF theory
to match old behavior.
* Additional gdb debug functionality. Now we have:
debugPrintNode(Node) debugPrintRawNode(Node)
debugPrintTNode(TNode) debugPrintRawTNode(TNode)
debugPrintTypeNode(TypeNode) debugPrintRawTypeNode(TypeNode)
debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)
they all print a {Node,TNode,NodeValue*} from the debugger.
The "Raw" versions print a very low-level AST-like form.
The regular versions do the same as operator<<, but force
full printing on (no depth-limiting).
* Other trivial fixes
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r-- | src/expr/expr_template.h | 105 |
1 files changed, 88 insertions, 17 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 1749971a5..34d4a1a9e 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -44,6 +44,7 @@ class Expr; namespace expr { class CVC4_PUBLIC ExprSetDepth; + class CVC4_PUBLIC ExprPrintTypes; }/* CVC4::expr namespace */ /** @@ -70,8 +71,8 @@ public: ~TypeCheckingException() throw (); /** - * Get the Node that caused the type-checking to fail. - * @return the node + * Get the Expr that caused the type-checking to fail. + * @return the expr */ Expr getExpression() const; @@ -205,7 +206,7 @@ public: * Outputs the string representation of the expression to the stream. * @param out the output stream */ - void toStream(std::ostream& out) const; + void toStream(std::ostream& out, int depth = -1, bool types = false) const; /** * Check if this is a null expression. @@ -249,22 +250,33 @@ public: ExprManager* getExprManager() const; /** - * IOStream manipulator to set the maximum depth of Nodes when + * IOStream manipulator to set the maximum depth of Exprs 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; + * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) + * out << setdepth(3) << e; * * gives "(OR a b (AND c (NOT d)))", but * - * out << setdepth(1) << [same node as above] + * out << setdepth(1) << [same expr as above] * * gives "(OR a b (...))" */ typedef expr::ExprSetDepth setdepth; /** + * IOStream manipulator to print type ascriptions or not. + * + * // let a, b, c, and d be variables of sort U + * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) + * out << e; + * + * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but + */ + typedef expr::ExprPrintTypes printtypes; + + /** * Very basic pretty printer for Expr. * This is equivalent to calling e.getNode().printAst(...) * @param out output stream to print to. @@ -290,7 +302,7 @@ protected: */ NodeTemplate<true> getNode() const; - // Friend to access the actual internal node information and private methods + // Friend to access the actual internal expr information and private methods friend class SmtEngine; friend class ExprManager; }; @@ -385,16 +397,16 @@ public: namespace expr { /** - * IOStream manipulator to set the maximum depth of Nodes when + * IOStream manipulator to set the maximum depth of Exprs 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; + * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) + * out << setdepth(3) << e; * * gives "(OR a b (AND c (NOT d)))", but * - * out << setdepth(1) << [same node as above] + * out << setdepth(1) << [same expr as above] * * gives "(OR a b (...))". * @@ -416,7 +428,7 @@ class CVC4_PUBLIC ExprSetDepth { static const int s_defaultPrintDepth = 3; /** - * When this manipulator is + * When this manipulator is used, the depth is stored here. */ long d_depth; @@ -444,6 +456,51 @@ public: } }; +/** + * IOStream manipulator to print type ascriptions or not. + * + * // let a, b, c, and d be variables of sort U + * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) + * out << e; + * + * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but + */ +class CVC4_PUBLIC ExprPrintTypes { + /** + * 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_defaultPrintTypes = false; + + /** + * When this manipulator is used, the setting is stored here. + */ + bool d_printTypes; + +public: + /** + * Construct a ExprPrintTypes with the given setting. + */ + ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {} + + inline void applyPrintTypes(std::ostream& out) { + out.iword(s_iosIndex) = d_printTypes; + } + + static inline bool getPrintTypes(std::ostream& out) { + return out.iword(s_iosIndex); + } + + static inline void setPrintTypes(std::ostream& out, bool printTypes) { + out.iword(s_iosIndex) = printTypes; + } +}; + }/* CVC4::expr namespace */ ${getConst_instantiations} @@ -453,11 +510,11 @@ ${getConst_instantiations} namespace expr { /** - * Sets the default depth when pretty-printing a Node to an ostream. - * Use like this: + * Sets the default print-types setting when pretty-printing an Expr + * to an ostream. Use like this: * - * // let out be an ostream, n a Node - * out << Node::setdepth(n) << n << endl; + * // let out be an ostream, e an Expr + * out << Expr::setdepth(n) << e << endl; * * The depth stays permanently (until set again) with the stream. */ @@ -466,6 +523,20 @@ inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) { return out; } +/** + * Sets the default depth when pretty-printing a Expr to an ostream. + * Use like this: + * + * // let out be an ostream, e an Expr + * out << Expr::setprinttypes(true) << e << endl; + * + * The setting stays permanently (until set again) with the stream. + */ +inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) { + pt.applyPrintTypes(out); + return out; +} + }/* CVC4::expr namespace */ }/* CVC4 namespace */ |