From 1ca8427a5c79e2e0425a55bc83fe8572055e1660 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Mon, 22 Feb 2010 23:01:16 +0000 Subject: Merging from branch branches/Liana r241 --- src/expr/expr.h | 9 +- src/expr/node.cpp | 3 + src/expr/node.h | 509 +++++++++++++++++++++++++++++++++++----------- src/expr/node_builder.cpp | 6 - src/expr/node_value.cpp | 18 +- src/expr/node_value.h | 47 ++--- 6 files changed, 417 insertions(+), 175 deletions(-) (limited to 'src/expr') diff --git a/src/expr/expr.h b/src/expr/expr.h index 27b7846db..6c615d391 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -28,7 +28,8 @@ namespace CVC4 { // The internal expression representation -class Node; +template +class NodeTemplate; /** * Class encapsulating CVC4 expressions and methods for constructing new @@ -161,10 +162,10 @@ protected: * @param em the expression manager that handles this expression * @param node the actual expression node pointer */ - Expr(ExprManager* em, Node* node); + Expr(ExprManager* em, NodeTemplate* node); /** The internal expression representation */ - Node* d_node; + NodeTemplate* d_node; /** The responsible expression manager */ ExprManager* d_exprManager; @@ -173,7 +174,7 @@ protected: * Returns the actual internal node. * @return the internal node */ - Node getNode() const; + NodeTemplate getNode() const; // Friend to access the actual internal node information and private methods friend class SmtEngine; diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 080623e21..b9d3d13bb 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,3 +1,4 @@ +<<<<<<< .working /********************* */ /** node.cpp ** Original author: mdeters @@ -198,3 +199,5 @@ void Node::debugPrint() { } }/* CVC4 namespace */ +======= +>>>>>>> .merge-right.r241 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 + class NodeTemplate; +typedef NodeTemplate Node; +typedef NodeTemplate 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 + 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 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 + 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; + friend class NodeTemplate; -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 + NodeTemplate(const NodeTemplate&); +>>>>>>> .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 inline typename AttrKind::value_type getAttribute(const AttrKind&) const; +======= + static NodeTemplate null(); +>>>>>>> .merge-right.r241 +<<<<<<< .working template inline bool hasAttribute(const AttrKind&, typename AttrKind::value_type* = NULL) const; +======= + typedef typename NodeValue::iterator iterator; + typedef typename NodeValue::iterator const_iterator; +>>>>>>> .merge-right.r241 - template - 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 + inline typename AttrKind::value_type getAttribute(const AttrKind&) const; + + template + 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 + 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 { 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 + inline bool NodeTemplate::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 + inline Kind NodeTemplate::getKind() const { + return Kind(d_ev->d_kind); + } -inline std::string Node::toString() const { - return d_ev->toString(); -} +template + inline std::string NodeTemplate::toString() const { + return d_ev->toString(); + } -inline void Node::toStream(std::ostream& out) const { - d_ev->toStream(out); -} +template + inline void NodeTemplate::toStream(std::ostream& out) const { + d_ev->toStream(out); + } -inline Node::ev_iterator Node::ev_begin() { - return d_ev->ev_begin(); -} +template + inline typename NodeTemplate::ev_iterator NodeTemplate::ev_begin() { + return d_ev->ev_begin(); + } -inline Node::ev_iterator Node::ev_end() { - return d_ev->ev_end(); -} +template + inline typename NodeTemplate::ev_iterator NodeTemplate::ev_end() { + return d_ev->ev_end(); + } -inline Node::const_ev_iterator Node::ev_begin() const { - return d_ev->ev_begin(); -} +template + inline typename NodeTemplate::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 + inline typename NodeTemplate::const_ev_iterator NodeTemplate< + ref_count>::ev_end() const { + return d_ev->ev_end(); + } -inline Node::iterator Node::begin() { - return d_ev->begin(); -} +template + inline typename NodeTemplate::iterator NodeTemplate::begin() { + return d_ev->begin (); + } -inline Node::iterator Node::end() { - return d_ev->end(); -} +template + inline typename NodeTemplate::iterator NodeTemplate::end() { + return d_ev->end (); + } -inline Node::const_iterator Node::begin() const { - return d_ev->begin(); -} +template + inline typename NodeTemplate::const_iterator NodeTemplate< + ref_count>::begin() const { + return d_ev->begin (); + } -inline Node::const_iterator Node::end() const { - return d_ev->end(); -} +template + inline typename NodeTemplate::const_iterator NodeTemplate< + ref_count>::end() const { + return d_ev->end (); + } -inline size_t Node::getNumChildren() const { - return d_ev->d_nchildren; -} +template + inline size_t NodeTemplate::getNumChildren() const { + return d_ev->d_nchildren; + } +template template +<<<<<<< .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::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 template +<<<<<<< .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::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 template -inline void Node::setAttribute(const AttrKind&, +inline void NodeTemplate::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 + NodeTemplate NodeTemplate::s_null(&NodeValue::s_null); + +template + NodeTemplate NodeTemplate::null() { + return s_null; + } + +template + bool NodeTemplate::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 NodeTemplate::isAtomic() const { + switch(getKind()) { + case NOT: + case XOR: + case ITE: + case IFF: + case IMPLIES: + case OR: + case AND: + return false; + default: + return true; + } + } + +template + NodeTemplate::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 + NodeTemplate::NodeTemplate(const NodeValue* ev) : + d_ev(const_cast (ev)) { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + if(ref_count) + d_ev->inc(); + } + +template +template + NodeTemplate::NodeTemplate(const NodeTemplate& e) { + Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!"); + d_ev = e.d_ev; + if(ref_count) + d_ev->inc(); + } + +template + NodeTemplate::~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 + void NodeTemplate::assignNodeValue(NodeValue* ev) { + d_ev = ev; + if(ref_count) + d_ev->inc(); + } + +template + NodeTemplate& NodeTemplate::operator= + (const NodeTemplate& 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 + NodeTemplate NodeTemplate::eqExpr(const NodeTemplate< + ref_count>& right) const { + return NodeManager::currentNM()->mkNode(EQUAL, *this, right); + } + +template + NodeTemplate NodeTemplate::notExpr() const { + return NodeManager::currentNM()->mkNode(NOT, *this); + } + +template + NodeTemplate NodeTemplate::andExpr( + const NodeTemplate& right) const { + return NodeManager::currentNM()->mkNode(AND, *this, right); + } + +template + NodeTemplate NodeTemplate::orExpr( + const NodeTemplate& right) const { + return NodeManager::currentNM()->mkNode(OR, *this, right); + } + +template + NodeTemplate NodeTemplate::iteExpr( + const NodeTemplate& thenpart, + const NodeTemplate& elsepart) const { + return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart); + } + +template + NodeTemplate NodeTemplate::iffExpr( + const NodeTemplate& right) const { + return NodeManager::currentNM()->mkNode(IFF, *this, right); + } + +template + NodeTemplate NodeTemplate::impExpr( + const NodeTemplate& right) const { + return NodeManager::currentNM()->mkNode(IMPLIES, *this, right); + } + +template + NodeTemplate NodeTemplate::xorExpr( + const NodeTemplate& right) const { + return NodeManager::currentNM()->mkNode(XOR, *this, right); + } + + +template + void NodeTemplate::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 + void NodeTemplate::debugPrint() { + printAst(Warning(), 0); + Warning().flush(); + } + +template +const Type* NodeTemplate::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 */ diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp index 7b78093c9..a7bc5f67d 100644 --- a/src/expr/node_builder.cpp +++ b/src/expr/node_builder.cpp @@ -12,9 +12,3 @@ ** **/ -#include "expr/node_builder.h" -#include "expr/node_manager.h" -#include "expr/node_value.h" -#include "util/output.h" - -using namespace std; diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 36d634b8b..52e995bf4 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -27,6 +27,8 @@ namespace CVC4 { size_t NodeValue::next_id = 1; +NodeValue NodeValue::s_null; + NodeValue::NodeValue() : d_id(0), d_rc(MAX_RC), @@ -64,22 +66,6 @@ void NodeValue::dec() { } } -NodeValue::iterator NodeValue::begin() { - return node_iterator(d_children); -} - -NodeValue::iterator NodeValue::end() { - return node_iterator(d_children + d_nchildren); -} - -NodeValue::const_iterator NodeValue::begin() const { - return const_node_iterator(d_children); -} - -NodeValue::const_iterator NodeValue::end() const { - return const_node_iterator(d_children + d_nchildren); -} - NodeValue::ev_iterator NodeValue::ev_begin() { return d_children; } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 2d84967c6..73418b06d 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -33,7 +33,7 @@ namespace CVC4 { -class Node; +template class NodeTemplate; template class NodeBuilder; class NodeManager; @@ -76,7 +76,7 @@ class NodeValue { // todo add exprMgr ref in debug case - friend class CVC4::Node; + template friend class CVC4::NodeTemplate; template friend class CVC4::NodeBuilder; friend class CVC4::NodeManager; @@ -103,49 +103,45 @@ class NodeValue { const_ev_iterator ev_begin() const; const_ev_iterator ev_end() const; - class node_iterator { + template + class iterator { const_ev_iterator d_i; public: - explicit node_iterator(const_ev_iterator i) : d_i(i) {} + explicit iterator(const_ev_iterator i) : d_i(i) {} - inline Node operator*(); + inline CVC4::NodeTemplate operator*(); - bool operator==(const node_iterator& i) { + bool operator==(const iterator& i) { return d_i == i.d_i; } - bool operator!=(const node_iterator& i) { + bool operator!=(const iterator& i) { return d_i != i.d_i; } - node_iterator operator++() { + iterator operator++() { ++d_i; return *this; } - node_iterator operator++(int) { - return node_iterator(d_i++); + iterator operator++(int) { + return iterator(d_i++); } typedef std::input_iterator_tag iterator_category; - typedef Node value_type; - typedef ptrdiff_t difference_type; - typedef Node* pointer; - typedef Node& reference; }; - typedef node_iterator const_node_iterator; public: - // Iterator support - typedef node_iterator iterator; - typedef node_iterator const_iterator; - - iterator begin(); - iterator end(); + template + iterator begin() const { + return iterator(d_children); + } - const_iterator begin() const; - const_iterator end() const; + template + iterator end() const { + return iterator(d_children + d_nchildren); + } /** * Hash this expression. @@ -207,8 +203,9 @@ public: namespace CVC4 { namespace expr { -inline Node NodeValue::node_iterator::operator*() { - return Node(*d_i); +template +inline CVC4::NodeTemplate NodeValue::iterator::operator*() { + return NodeTemplate(*d_i); } }/* CVC4::expr namespace */ -- cgit v1.2.3