From 09279d722aa6e62e86eb4b34583397db1093051e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 22 Feb 2010 19:24:43 +0000 Subject: Re-committing revision 232 properly: * Add virtual destructors to CnfStream, Theory, OutputChannel, and ExplainOutputChannel. Safer and stops a compiler warning. * node attributes: fix compiler warnings on 64-bit. * Node: add asserts to make sure the current NodeManager is non-NULL when it's needed. This can happen when public-facing functions don't properly set the node manager, and it can look like a bug in another part of the library. Also some code format cleanup. * configure.ac, config/cvc4.m4: added --enable-static-binary (see discussion on bug 33), fixed bad configure lines (bug 19), added documentation for some things. * config.h.in: removed; it's auto-generated. --- src/expr/node.h | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) (limited to 'src/expr/node.h') diff --git a/src/expr/node.h b/src/expr/node.h index 463ff8144..a39dc5b7e 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -48,7 +48,6 @@ using CVC4::expr::NodeValue; class Node { friend class NodeValue; - friend class SoftNode; /** A convenient null-valued encapsulated pointer */ static Node s_null; @@ -106,7 +105,7 @@ public: bool operator!=(const Node& e) const { return d_ev != e.d_ev; } Node operator[](int i) const { - Assert(i >= 0 && i < d_ev->d_nchildren); + Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren); return Node(d_ev->d_children[i]); } @@ -130,9 +129,11 @@ public: Node impExpr(const Node& right) const; Node xorExpr(const Node& right) const; + /* Node plusExpr(const Node& right) const; Node uMinusExpr() const; Node multExpr(const Node& right) const; + */ inline Kind getKind() const; @@ -171,9 +172,9 @@ public: * @param indent number of spaces to indent the formula by. */ void printAst(std::ostream & o, int indent = 0) const; - + private: - + /** * Pretty printer for use within gdb * This is not intended to be used outside of gdb. @@ -262,18 +263,30 @@ inline size_t Node::getNumChildren() const { template inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->getAttribute(*this, AttrKind()); } template inline bool Node::hasAttribute(const AttrKind&, typename AttrKind::value_type* ret) { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret); } template inline void Node::setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + NodeManager::currentNM()->setAttribute(*this, AttrKind(), value); } -- cgit v1.2.3