diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-22 23:01:16 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-22 23:01:16 +0000 |
commit | 1ca8427a5c79e2e0425a55bc83fe8572055e1660 (patch) | |
tree | c9431983b76c3884a4e34a95c7a94476b95efc51 /src/expr/node.h | |
parent | c5872ac197a68ea0686c90f3a8bd1e7cc993532d (diff) |
Merging from branch branches/Liana r241
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 509 |
1 files changed, 385 insertions, 124 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 77f9141f1..280c85fb3 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -30,7 +30,10 @@ namespace CVC4 { -class Node; +template<bool ref_count> + class NodeTemplate; +typedef NodeTemplate<true> Node; +typedef NodeTemplate<false> TNode; inline std::ostream& operator<<(std::ostream&, const Node&); @@ -38,7 +41,7 @@ class NodeManager; class Type; namespace expr { - class NodeValue; +class NodeValue; }/* CVC4::expr namespace */ using CVC4::expr::NodeValue; @@ -47,127 +50,168 @@ using CVC4::expr::NodeValue; * Encapsulation of an NodeValue pointer. The reference count is * maintained in the NodeValue. */ -class Node { +template<bool ref_count> + class NodeTemplate { friend class NodeValue; - /** A convenient null-valued encapsulated pointer */ - static Node s_null; - - /** The referenced NodeValue */ - NodeValue* d_ev; - - /** This constructor is reserved for use by the Node package; one - * must construct an Node using one of the build mechanisms of the - * Node package. - * - * Increments the reference count. - * - * FIXME: there's a type-system escape here to cast away the const, - * since the refcount needs to be updated. But conceptually Nodes - * don't change their arguments, and it's nice to have - * const_iterators over them. See notes in .cpp file for - * details. */ - // this really does needs to be explicit to avoid hard to track - // errors with Nodes implicitly wrapping NodeValues - explicit Node(const NodeValue*); - - template <unsigned> friend class NodeBuilder; - friend class NodeManager; + /** A convenient null-valued encapsulated pointer */ + static NodeTemplate s_null; - /** - * Assigns the expression value and does reference counting. No assumptions - * are made on the expression, and should only be used if we know what we are - * doing. - * - * @param ev the expression value to assign - */ - void assignNodeValue(NodeValue* ev); + /** The referenced NodeValue */ + NodeValue* d_ev; + + bool d_count_ref; + + /** This constructor is reserved for use by the NodeTemplate package; one + * must construct an NodeTemplate using one of the build mechanisms of the + * NodeTemplate package. + * + * Increments the reference count. + * + * FIXME: there's a type-system escape here to cast away the const, + * since the refcount needs to be updated. But conceptually Nodes + * don't change their arguments, and it's nice to have + * const_iterators over them. See notes in .cpp file for + * details. */ + // this really does needs to be explicit to avoid hard to track + // errors with Nodes implicitly wrapping NodeValues + explicit NodeTemplate(const NodeValue*); - typedef NodeValue::ev_iterator ev_iterator; - typedef NodeValue::const_ev_iterator const_ev_iterator; + template<unsigned> + friend class NodeBuilder; - inline ev_iterator ev_begin(); - inline ev_iterator ev_end(); - inline const_ev_iterator ev_begin() const; - inline const_ev_iterator ev_end() const; + friend class NodeTemplate<true>; + friend class NodeTemplate<false>; -public: + friend class NodeManager; - /** Default constructor, makes a null expression. */ - Node(); + /** + * Assigns the expression value and does reference counting. No assumptions + * are made on the expression, and should only be used if we know what we are + * doing. + * + * @param ev the expression value to assign + */ + void assignNodeValue(NodeValue* ev); - Node(const Node&); + typedef NodeValue::ev_iterator ev_iterator; + typedef NodeValue::const_ev_iterator const_ev_iterator; - /** Destructor. Decrements the reference count and, if zero, - * collects the NodeValue. */ - ~Node(); + inline ev_iterator ev_begin(); + inline ev_iterator ev_end(); + inline const_ev_iterator ev_begin() const; + inline const_ev_iterator ev_end() const; - bool operator==(const Node& e) const { return d_ev == e.d_ev; } - bool operator!=(const Node& e) const { return d_ev != e.d_ev; } + public: + /** Default constructor, makes a null expression. */ + NodeTemplate(); + +<<<<<<< .working Node operator[](int i) const { Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren); return Node(d_ev->d_children[i]); } +======= + template <bool ref_count_1> + NodeTemplate(const NodeTemplate<ref_count_1>&); +>>>>>>> .merge-right.r241 - /** - * We compare by expression ids so, keeping things deterministic and having - * that subexpressions have to be smaller than the enclosing expressions. - */ - inline bool operator<(const Node& e) const; + /** Destructor. Decrements the reference count and, if zero, + * collects the NodeValue. */ + ~NodeTemplate(); - Node& operator=(const Node&); + bool operator==(const NodeTemplate& e) const { + return d_ev == e.d_ev; + } + bool operator!=(const NodeTemplate& e) const { + return d_ev != e.d_ev; + } - size_t hash() const { return d_ev->getId(); } - uint64_t getId() const { return d_ev->getId(); } + NodeTemplate operator[](int i) const { + Assert(i >= 0 && i < d_ev->d_nchildren); + return NodeTemplate(d_ev->d_children[i]); + } - Node eqExpr(const Node& right) const; - Node notExpr() const; - Node andExpr(const Node& right) const; - Node orExpr(const Node& right) const; - Node iteExpr(const Node& thenpart, const Node& elsepart) const; - Node iffExpr(const Node& right) const; - Node impExpr(const Node& right) const; - Node xorExpr(const Node& right) const; + /** + * We compare by expression ids so, keeping things deterministic and having + * that subexpressions have to be smaller than the enclosing expressions. + */ + inline bool operator<(const NodeTemplate& e) const; +<<<<<<< .working /* Node plusExpr(const Node& right) const; Node uMinusExpr() const; Node multExpr(const Node& right) const; +======= + NodeTemplate& operator=(const NodeTemplate&); +>>>>>>> .merge-right.r241 */ - inline Kind getKind() const; + size_t hash() const { + return d_ev->getId(); + } - inline size_t getNumChildren() const; + uint64_t getId() const { + return d_ev->getId(); + } const Type* getType() const; - static Node null(); + const Type* getType() const; - typedef NodeValue::node_iterator iterator; - typedef NodeValue::node_iterator const_iterator; + NodeTemplate eqExpr(const NodeTemplate& right) const; + NodeTemplate notExpr() const; + NodeTemplate andExpr(const NodeTemplate& right) const; + NodeTemplate orExpr(const NodeTemplate& right) const; + NodeTemplate iteExpr(const NodeTemplate& thenpart, + const NodeTemplate& elsepart) const; + NodeTemplate iffExpr(const NodeTemplate& right) const; + NodeTemplate impExpr(const NodeTemplate& right) const; + NodeTemplate xorExpr(const NodeTemplate& right) const; - inline iterator begin(); - inline iterator end(); - inline const_iterator begin() const; - inline const_iterator end() const; + NodeTemplate plusExpr(const NodeTemplate& right) const; + NodeTemplate uMinusExpr() const; + NodeTemplate multExpr(const NodeTemplate& right) const; - inline std::string toString() const; - inline void toStream(std::ostream&) const; + inline Kind getKind() const; - bool isNull() const; - bool isAtomic() const; + inline size_t getNumChildren() const; +<<<<<<< .working template <class AttrKind> inline typename AttrKind::value_type getAttribute(const AttrKind&) const; +======= + static NodeTemplate null(); +>>>>>>> .merge-right.r241 +<<<<<<< .working template <class AttrKind> inline bool hasAttribute(const AttrKind&, typename AttrKind::value_type* = NULL) const; +======= + typedef typename NodeValue::iterator<ref_count> iterator; + typedef typename NodeValue::iterator<ref_count> const_iterator; +>>>>>>> .merge-right.r241 - template <class AttrKind> - inline void setAttribute(const AttrKind&, - const typename AttrKind::value_type& value); + inline iterator begin(); + inline iterator end(); + inline const_iterator begin() const; + inline const_iterator end() const; + + template <class AttrKind> + inline typename AttrKind::value_type getAttribute(const AttrKind&) const; + + template <class AttrKind> + inline bool hasAttribute(const AttrKind&, typename AttrKind::value_type* = NULL) const; + + inline std::string toString() const; + inline void toStream(std::ostream&) const; + + + bool isNull() const; + bool isAtomic() const; /** * Very basic pretty printer for Node. @@ -186,7 +230,16 @@ private: */ void debugPrint(); -};/* class Node */ + template<class AttrKind> + inline void setAttribute( + const AttrKind&, const typename AttrKind::value_type& value); + + static void indent(std::ostream & o, int indent) { + for(int i = 0; i < indent; i++) + o << ' '; + } + + };/* class NodeTemplate */ }/* CVC4 namespace */ @@ -194,10 +247,10 @@ private: // for hashtables namespace __gnu_cxx { - template <> +template<> struct hash<CVC4::Node> { size_t operator()(const CVC4::Node& node) const { - return (size_t)node.hash(); + return (size_t) node.hash(); } }; }/* __gnu_cxx namespace */ @@ -207,84 +260,121 @@ namespace __gnu_cxx { namespace CVC4 { -inline bool Node::operator<(const Node& e) const { - return d_ev->d_id < e.d_ev->d_id; -} +template<bool ref_count> + inline bool NodeTemplate<ref_count>::operator<(const NodeTemplate& e) const { + return d_ev->d_id < e.d_ev->d_id; + } inline std::ostream& operator<<(std::ostream& out, const Node& e) { e.toStream(out); return out; } -inline Kind Node::getKind() const { - return Kind(d_ev->d_kind); -} +template<bool ref_count> + inline Kind NodeTemplate<ref_count>::getKind() const { + return Kind(d_ev->d_kind); + } -inline std::string Node::toString() const { - return d_ev->toString(); -} +template<bool ref_count> + inline std::string NodeTemplate<ref_count>::toString() const { + return d_ev->toString(); + } -inline void Node::toStream(std::ostream& out) const { - d_ev->toStream(out); -} +template<bool ref_count> + inline void NodeTemplate<ref_count>::toStream(std::ostream& out) const { + d_ev->toStream(out); + } -inline Node::ev_iterator Node::ev_begin() { - return d_ev->ev_begin(); -} +template<bool ref_count> + inline typename NodeTemplate<ref_count>::ev_iterator NodeTemplate<ref_count>::ev_begin() { + return d_ev->ev_begin(); + } -inline Node::ev_iterator Node::ev_end() { - return d_ev->ev_end(); -} +template<bool ref_count> + inline typename NodeTemplate<ref_count>::ev_iterator NodeTemplate<ref_count>::ev_end() { + return d_ev->ev_end(); + } -inline Node::const_ev_iterator Node::ev_begin() const { - return d_ev->ev_begin(); -} +template<bool ref_count> + inline typename NodeTemplate<ref_count>::const_ev_iterator NodeTemplate< + ref_count>::ev_begin() const { + return d_ev->ev_begin(); + } -inline Node::const_ev_iterator Node::ev_end() const { - return d_ev->ev_end(); -} +template<bool ref_count> + inline typename NodeTemplate<ref_count>::const_ev_iterator NodeTemplate< + ref_count>::ev_end() const { + return d_ev->ev_end(); + } -inline Node::iterator Node::begin() { - return d_ev->begin(); -} +template<bool ref_count> + inline typename NodeTemplate<ref_count>::iterator NodeTemplate<ref_count>::begin() { + return d_ev->begin<ref_count> (); + } -inline Node::iterator Node::end() { - return d_ev->end(); -} +template<bool ref_count> + inline typename NodeTemplate<ref_count>::iterator NodeTemplate<ref_count>::end() { + return d_ev->end<ref_count> (); + } -inline Node::const_iterator Node::begin() const { - return d_ev->begin(); -} +template<bool ref_count> + inline typename NodeTemplate<ref_count>::const_iterator NodeTemplate< + ref_count>::begin() const { + return d_ev->begin<ref_count> (); + } -inline Node::const_iterator Node::end() const { - return d_ev->end(); -} +template<bool ref_count> + inline typename NodeTemplate<ref_count>::const_iterator NodeTemplate< + ref_count>::end() const { + return d_ev->end<ref_count> (); + } -inline size_t Node::getNumChildren() const { - return d_ev->d_nchildren; -} +template<bool ref_count> + inline size_t NodeTemplate<ref_count>::getNumChildren() const { + return d_ev->d_nchildren; + } +template <bool ref_count> template <class AttrKind> +<<<<<<< .working inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); +======= +inline typename AttrKind::value_type NodeTemplate<ref_count>::getAttribute(const AttrKind&) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + +>>>>>>> .merge-right.r241 return NodeManager::currentNM()->getAttribute(*this, AttrKind()); } +template <bool ref_count> template <class AttrKind> +<<<<<<< .working inline bool Node::hasAttribute(const AttrKind&, typename AttrKind::value_type* ret) const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); +======= +inline bool NodeTemplate<ref_count>::hasAttribute(const AttrKind&, + typename AttrKind::value_type* ret) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + +>>>>>>> .merge-right.r241 return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret); } +template <bool ref_count> template <class AttrKind> -inline void Node::setAttribute(const AttrKind&, +inline void NodeTemplate<ref_count>::setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" @@ -293,6 +383,177 @@ inline void Node::setAttribute(const AttrKind&, NodeManager::currentNM()->setAttribute(*this, AttrKind(), value); } +template<bool ref_count> + NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&NodeValue::s_null); + +template<bool ref_count> + NodeTemplate<ref_count> NodeTemplate<ref_count>::null() { + return s_null; + } + +template<bool ref_count> + bool NodeTemplate<ref_count>::isNull() const { + return d_ev == &NodeValue::s_null; + } + +////FIXME: This function is a major hack! Should be changed ASAP +////TODO: Should use positive definition, i.e. what kinds are atomic. +template<bool ref_count> + bool NodeTemplate<ref_count>::isAtomic() const { + switch(getKind()) { + case NOT: + case XOR: + case ITE: + case IFF: + case IMPLIES: + case OR: + case AND: + return false; + default: + return true; + } + } + +template<bool ref_count> + NodeTemplate<ref_count>::NodeTemplate() : + d_ev(&NodeValue::s_null) { + // No refcount needed + } + +// FIXME: escape from type system convenient but is there a better +// way? Nodes conceptually don't change their expr values but of +// course they do modify the refcount. But it's nice to be able to +// support node_iterators over const NodeValue*. So.... hm. +template<bool ref_count> + NodeTemplate<ref_count>::NodeTemplate(const NodeValue* ev) : + d_ev(const_cast<NodeValue*> (ev)) { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + if(ref_count) + d_ev->inc(); + } + +template<bool ref_count> +template<bool ref_count_1> + NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count_1>& e) { + Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!"); + d_ev = e.d_ev; + if(ref_count) + d_ev->inc(); + } + +template<bool ref_count> + NodeTemplate<ref_count>::~NodeTemplate() { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + if(ref_count) + d_ev->dec(); + Assert(ref_count || d_ev->d_rc > 0, + "Temporary node pointing to an expired node"); + } + +template<bool ref_count> + void NodeTemplate<ref_count>::assignNodeValue(NodeValue* ev) { + d_ev = ev; + if(ref_count) + d_ev->inc(); + } + +template<bool ref_count> + NodeTemplate<ref_count>& NodeTemplate<ref_count>::operator= + (const NodeTemplate<ref_count>& e) { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + Assert(e.d_ev != NULL, "Expecting a non-NULL expression value on RHS!"); + if(EXPECT_TRUE( d_ev != e.d_ev )) { + if(ref_count) + d_ev->dec(); + d_ev = e.d_ev; + if(ref_count) + d_ev->inc(); + } + return *this; + } + +template<bool ref_count> + NodeTemplate<ref_count> NodeTemplate<ref_count>::eqExpr(const NodeTemplate< + ref_count>& right) const { + return NodeManager::currentNM()->mkNode(EQUAL, *this, right); + } + +template<bool ref_count> + NodeTemplate<ref_count> NodeTemplate<ref_count>::notExpr() const { + return NodeManager::currentNM()->mkNode(NOT, *this); + } + +template<bool ref_count> + NodeTemplate<ref_count> NodeTemplate<ref_count>::andExpr( + const NodeTemplate<ref_count>& right) const { + return NodeManager::currentNM()->mkNode(AND, *this, right); + } + +template<bool ref_count> + NodeTemplate<ref_count> NodeTemplate<ref_count>::orExpr( + const NodeTemplate<ref_count>& right) const { + return NodeManager::currentNM()->mkNode(OR, *this, right); + } + +template<bool ref_count> + NodeTemplate<ref_count> NodeTemplate<ref_count>::iteExpr( + const NodeTemplate<ref_count>& thenpart, + const NodeTemplate<ref_count>& elsepart) const { + return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart); + } + +template<bool ref_count> + NodeTemplate<ref_count> NodeTemplate<ref_count>::iffExpr( + const NodeTemplate<ref_count>& right) const { + return NodeManager::currentNM()->mkNode(IFF, *this, right); + } + +template<bool ref_count> + NodeTemplate<ref_count> NodeTemplate<ref_count>::impExpr( + const NodeTemplate<ref_count>& right) const { + return NodeManager::currentNM()->mkNode(IMPLIES, *this, right); + } + +template<bool ref_count> + NodeTemplate<ref_count> NodeTemplate<ref_count>::xorExpr( + const NodeTemplate<ref_count>& right) const { + return NodeManager::currentNM()->mkNode(XOR, *this, right); + } + + +template<bool ref_count> + void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const { + indent(out, ind); + out << '('; + out << getKind(); + if(getKind() == VARIABLE) { + out << ' ' << getId(); + + } else if(getNumChildren() >= 1) { + for(const_iterator child = begin(); child != end(); ++child) { + out << std::endl; + NodeTemplate((*child)).printAst(out, ind + 1); + } + out << std::endl; + indent(out, ind); + } + out << ')'; + } + +template<bool ref_count> + void NodeTemplate<ref_count>::debugPrint() { + printAst(Warning(), 0); + Warning().flush(); + } + +template<bool ref_count> +const Type* NodeTemplate<ref_count>::getType() const { + 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()->getType(*this); +} + }/* CVC4 namespace */ #endif /* __CVC4__NODE_H */ |