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 | |
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')
-rw-r--r-- | src/expr/expr_template.cpp | 5 | ||||
-rw-r--r-- | src/expr/expr_template.h | 105 | ||||
-rw-r--r-- | src/expr/node.h | 70 | ||||
-rw-r--r-- | src/expr/node_builder.h | 9 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 3 | ||||
-rw-r--r-- | src/expr/node_manager.h | 3 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 39 | ||||
-rw-r--r-- | src/expr/node_value.h | 40 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 2 | ||||
-rw-r--r-- | src/expr/type_node.h | 41 |
10 files changed, 240 insertions, 77 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 05d31499d..c3191ab48 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -39,6 +39,7 @@ namespace CVC4 { namespace expr { const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); +const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc(); }/* CVC4::expr namespace */ @@ -198,9 +199,9 @@ bool Expr::isConst() const { return d_node->isConst(); } -void Expr::toStream(std::ostream& out) const { +void Expr::toStream(std::ostream& out, int depth, bool types) const { ExprManagerScope ems(*this); - d_node->toStream(out); + d_node->toStream(out, depth, types); } Node Expr::getNode() const { 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 */ diff --git a/src/expr/node.h b/src/expr/node.h index e3fb42ead..09a1ad8bc 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -455,12 +455,13 @@ public: * given stream * @param out the sream to serialise this node to */ - inline void toStream(std::ostream& out, int toDepth = -1) const { + inline void toStream(std::ostream& out, int toDepth = -1, + bool types = false) const { if(!ref_count) { Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); } - d_nv->toStream(out, toDepth); + d_nv->toStream(out, toDepth, types); } /** @@ -480,11 +481,22 @@ public: typedef expr::ExprSetDepth setdepth; /** + * IOStream manipulator to print type ascriptions or not. + * + * // let a, b, c, and d be variables of sort U + * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d))) + * out << n; + * + * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but + */ + typedef expr::ExprPrintTypes printtypes; + + /** * Very basic pretty printer for Node. * @param o output stream to print to. * @param indent number of spaces to indent the formula by. */ - void printAst(std::ostream & o, int indent = 0) const; + inline void printAst(std::ostream& out, int indent = 0) const; NodeTemplate<true> eqNode(const NodeTemplate& right) const; @@ -497,19 +509,6 @@ public: NodeTemplate<true> impNode(const NodeTemplate& right) const; NodeTemplate<true> xorNode(const NodeTemplate& right) const; -private: - - /** - * Indents the given stream a given amount of spaces. - * @param out the stream to indent - * @param indent the numer of spaces - */ - static void indent(std::ostream& out, int indent) { - for(int i = 0; i < indent; i++) { - out << ' '; - } - } - };/* class NodeTemplate<ref_count> */ /** @@ -519,7 +518,9 @@ private: * @return the changed stream. */ inline std::ostream& operator<<(std::ostream& out, TNode n) { - n.toStream(out, Node::setdepth::getDepth(out)); + n.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out)); return out; } @@ -805,30 +806,9 @@ NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count>& right) const { } template <bool ref_count> -void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const { - indent(out, ind); - out << '('; - out << getKind(); - if(getMetaKind() == kind::metakind::VARIABLE) { - out << ' ' << getId(); - } else if(getMetaKind() == kind::metakind::CONSTANT) { - out << ' '; - kind::metakind::NodeValueConstPrinter::toStream(out, d_nv); - } else { - if(hasOperator()) { - out << std::endl; - getOperator().printAst(out, ind + 1); - } - if(getNumChildren() >= 1) { - for(const_iterator child = begin(); child != end(); ++child) { - out << std::endl; - (*child).printAst(out, ind + 1); - } - out << std::endl; - indent(out, ind); - } - } - out << ')'; +inline void +NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const { + d_nv->printAst(out, indent); } /** @@ -910,11 +890,19 @@ TypeNode NodeTemplate<ref_count>::getType() const * to meet. A cleaner solution is welcomed. */ static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) { + Warning() << Node::setdepth(-1) << n << std::endl; + Warning().flush(); +} +static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) { n.printAst(Warning(), 0); Warning().flush(); } static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) { + Warning() << Node::setdepth(-1) << n << std::endl; + Warning().flush(); +} +static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& n) { n.printAst(Warning(), 0); Warning().flush(); } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 0cb9ed026..402116842 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -661,10 +661,11 @@ public: operator Node(); operator Node() const; - inline void toStream(std::ostream& out, int depth = -1) const { + inline void toStream(std::ostream& out, int depth = -1, + bool types = false) const { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - d_nv->toStream(out, depth); + d_nv->toStream(out, depth, types); } NodeBuilder<nchild_thresh>& operator&=(TNode); @@ -1211,7 +1212,9 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { template <unsigned nchild_thresh> inline std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& b) { - b.toStream(out, Node::setdepth::getDepth(out)); + b.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out)); return out; } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 8f7196e0c..2e45fe9d0 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -190,6 +190,9 @@ TypeNode NodeManager::getType(TNode n) if(!hasType) { // Infer the type switch(n.getKind()) { + case kind::SORT_TYPE: + typeNode = kindType(); + break; case kind::EQUAL: typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n); break; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 3586440d4..4d796d81c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -745,8 +745,7 @@ inline bool NodeManager::hasOperator(Kind k) { } inline TypeNode NodeManager::mkSort() { - TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode(); - return type; + return NodeBuilder<0>(this, kind::SORT_TYPE).constructTypeNode(); } inline TypeNode NodeManager::mkSort(const std::string& name) { diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index c64a608fb..8add462e0 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -41,27 +41,34 @@ string NodeValue::toString() const { return ss.str(); } -void NodeValue::toStream(std::ostream& out, int toDepth) const { +void NodeValue::toStream(std::ostream& out, int toDepth, bool types) const { using namespace CVC4::kind; using namespace CVC4; if(getKind() == kind::NULL_EXPR) { out << "null"; } else if(getMetaKind() == kind::metakind::VARIABLE) { - if(getKind() != kind::VARIABLE) { + if(getKind() != kind::VARIABLE && + getKind() != kind::SORT_TYPE) { out << getKind() << ':'; } string s; + NodeManager* nm = NodeManager::currentNM(); // conceptually "this" is const, and hasAttribute() doesn't change // its argument, but it requires a non-const key arg (for now) - if(NodeManager::currentNM()->getAttribute(const_cast<NodeValue*>(this), - VarNameAttr(), s)) { + if(nm->getAttribute(const_cast<NodeValue*>(this), + VarNameAttr(), s)) { out << s; } else { out << "var_" << d_id; } + if(types) { + // print the whole type, but not *its* type + out << ":"; + nm->getType(TNode(this)).toStream(out, -1, false); + } } else { out << '(' << Kind(d_kind); if(getMetaKind() == kind::metakind::CONSTANT) { @@ -73,7 +80,7 @@ void NodeValue::toStream(std::ostream& out, int toDepth) const { out << ' '; } if(toDepth != 0) { - (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1); + (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1, types); } else { out << "(...)"; } @@ -83,5 +90,27 @@ void NodeValue::toStream(std::ostream& out, int toDepth) const { } } +void NodeValue::printAst(std::ostream& out, int ind) const { + indent(out, ind); + out << '('; + out << getKind(); + if(getMetaKind() == kind::metakind::VARIABLE) { + out << ' ' << getId(); + } else if(getMetaKind() == kind::metakind::CONSTANT) { + out << ' '; + kind::metakind::NodeValueConstPrinter::toStream(out, this); + } else { + if(nv_begin() != nv_end()) { + for(const_nv_iterator child = nv_begin(); child != nv_end(); ++child) { + out << std::endl; + (*child)->printAst(out, ind + 1); + } + out << std::endl; + indent(out, ind); + } + } + out << ')'; +} + }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 8b2056560..9f8a8f45b 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -213,7 +213,7 @@ public: } std::string toString() const; - void toStream(std::ostream& out, int toDepth = -1) const; + void toStream(std::ostream& out, int toDepth = -1, bool types = false) const; static inline unsigned kindToDKind(Kind k) { return ((unsigned) k) & kindMask; @@ -235,6 +235,21 @@ public: NodeValue* getChild(int i) const; + void printAst(std::ostream& out, int indent = 0) const; + +private: + + /** + * Indents the given stream a given amount of spaces. + * @param out the stream to indent + * @param indent the numer of spaces + */ + static inline void indent(std::ostream& out, int indent) { + for(int i = 0; i < indent; i++) { + out << ' '; + } + } + };/* class NodeValue */ /** @@ -264,6 +279,7 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv); }/* CVC4 namespace */ #include "expr/node_manager.h" +#include "expr/type_node.h" namespace CVC4 { namespace expr { @@ -363,11 +379,31 @@ inline T NodeValue::iterator<T>::operator*() { } inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) { - nv.toStream(out, Node::setdepth::getDepth(out)); + nv.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out)); return out; } }/* CVC4::expr namespace */ + +#ifdef CVC4_DEBUG +/** + * Pretty printer for use within gdb. This is not intended to be used + * outside of gdb. This writes to the Warning() stream and immediately + * flushes the stream. + */ +static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) { + Warning() << Node::setdepth(-1) << *nv << std::endl; + Warning().flush(); +} + +static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) { + nv->printAst(Warning(), 0); + Warning().flush(); +} +#endif /* CVC4_DEBUG */ + }/* CVC4 namespace */ #endif /* __CVC4__EXPR__NODE_VALUE_H */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 6f8911280..43d3c761e 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -77,7 +77,7 @@ TypeNode TypeNode::getRangeType() const { /** Is this a sort kind */ bool TypeNode::isSort() const { - return getKind() == kind::VARIABLE; + return getKind() == kind::SORT_TYPE; } /** Is this a kind type (i.e., the type of a type)? */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index da277a382..a58d9dc89 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -280,8 +280,9 @@ public: * given stream * @param out the sream to serialise this node to */ - inline void toStream(std::ostream& out, int toDepth = -1) const { - d_nv->toStream(out, toDepth); + inline void toStream(std::ostream& out, int toDepth = -1, + bool types = false) const { + d_nv->toStream(out, toDepth, types); } /** @@ -289,7 +290,7 @@ public: * @param o output stream to print to. * @param indent number of spaces to indent the formula by. */ - void printAst(std::ostream & o, int indent = 0) const; + void printAst(std::ostream& out, int indent = 0) const; /** * Returns true if this type is a null type. @@ -369,7 +370,9 @@ private: * @return the changed stream. */ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { - n.toStream(out, Node::setdepth::getDepth(out)); + n.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out)); return out; } @@ -465,6 +468,36 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value); } +inline void TypeNode::printAst(std::ostream& out, int indent) const { + d_nv->printAst(out, indent); +} + +#ifdef CVC4_DEBUG +/** + * Pretty printer for use within gdb. This is not intended to be used + * outside of gdb. This writes to the Warning() stream and immediately + * flushes the stream. + * + * Note that this function cannot be a template, since the compiler + * won't instantiate it. Even if we explicitly instantiate. (Odd?) + * So we implement twice. We mark as __attribute__((used)) so that + * GCC emits code for it even though static analysis indicates it's + * never called. + * + * Tim's Note: I moved this into the node.h file because this allows gdb + * to find the symbol, and use it, which is the first standard this code needs + * to meet. A cleaner solution is welcomed. + */ +static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) { + Warning() << Node::setdepth(-1) << n << std::endl; + Warning().flush(); +} +static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) { + n.printAst(Warning(), 0); + Warning().flush(); +} +#endif /* CVC4_DEBUG */ + }/* CVC4 namespace */ #endif /* __CVC4__NODE_H */ |