diff options
| -rw-r--r-- | src/expr/expr.h | 9 | ||||
| -rw-r--r-- | src/expr/node.cpp | 3 | ||||
| -rw-r--r-- | src/expr/node.h | 509 | ||||
| -rw-r--r-- | src/expr/node_builder.cpp | 6 | ||||
| -rw-r--r-- | src/expr/node_value.cpp | 18 | ||||
| -rw-r--r-- | src/expr/node_value.h | 47 | ||||
| -rw-r--r-- | src/prop/cnf_stream.cpp | 44 | ||||
| -rw-r--r-- | src/prop/cnf_stream.h | 30 |
8 files changed, 454 insertions, 212 deletions
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 <bool count_ref> +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<true>* node); /** The internal expression representation */ - Node* d_node; + NodeTemplate<true>* 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<true> 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<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 */ 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 <bool ref_count> class NodeTemplate; template <unsigned> class NodeBuilder; class NodeManager; @@ -76,7 +76,7 @@ class NodeValue { // todo add exprMgr ref in debug case - friend class CVC4::Node; + template <bool> friend class CVC4::NodeTemplate; template <unsigned> 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 <bool ref_count> + 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<ref_count> 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 <bool ref_count> + iterator<ref_count> begin() const { + return iterator<ref_count>(d_children); + } - const_iterator begin() const; - const_iterator end() const; + template <bool ref_count> + iterator<ref_count> end() const { + return iterator<ref_count>(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 <bool ref_count> +inline CVC4::NodeTemplate<ref_count> NodeValue::iterator<ref_count>::operator*() { + return NodeTemplate<ref_count>(*d_i); } }/* CVC4::expr namespace */ diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index a96d499b6..a66e36a07 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -59,27 +59,27 @@ void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) { assertClause(clause); } -bool CnfStream::isCached(const Node& n) const { +bool CnfStream::isCached(const TNode& n) const { return d_translationCache.find(n) != d_translationCache.end(); } -SatLiteral CnfStream::lookupInCache(const Node& n) const { +SatLiteral CnfStream::lookupInCache(const TNode& n) const { Assert(isCached(n), "Node is not in CNF translation cache"); return d_translationCache.find(n)->second; } -void CnfStream::cacheTranslation(const Node& node, SatLiteral lit) { +void CnfStream::cacheTranslation(const TNode& node, SatLiteral lit) { Debug("cnf") << "caching translation " << node << " to " << lit << endl; - d_translationCache.insert(make_pair(node, lit)); + d_translationCache[node] = lit; } -SatLiteral CnfStream::newLiteral(const Node& node) { +SatLiteral CnfStream::newLiteral(const TNode& node) { SatLiteral lit = SatLiteral(d_satSolver->newVar()); cacheTranslation(node, lit); return lit; } -SatLiteral TseitinCnfStream::handleAtom(const Node& node) { +SatLiteral TseitinCnfStream::handleAtom(const TNode& node) { Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom"); Assert(!isCached(node), "atom already mapped!"); @@ -101,7 +101,7 @@ SatLiteral TseitinCnfStream::handleAtom(const Node& node) { return lit; } -SatLiteral TseitinCnfStream::handleXor(const Node& xorNode) { +SatLiteral TseitinCnfStream::handleXor(const TNode& xorNode) { Assert(!isCached(xorNode), "Atom already mapped!"); Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!"); Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!"); @@ -119,7 +119,7 @@ SatLiteral TseitinCnfStream::handleXor(const Node& xorNode) { return xorLit; } -SatLiteral TseitinCnfStream::handleOr(const Node& orNode) { +SatLiteral TseitinCnfStream::handleOr(const TNode& orNode) { Assert(!isCached(orNode), "Atom already mapped!"); Assert(orNode.getKind() == OR, "Expecting an OR expression!"); Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!"); @@ -128,8 +128,8 @@ SatLiteral TseitinCnfStream::handleOr(const Node& orNode) { unsigned n_children = orNode.getNumChildren(); // Transform all the children first - Node::iterator node_it = orNode.begin(); - Node::iterator node_it_end = orNode.end(); + TNode::const_iterator node_it = orNode.begin(); + TNode::const_iterator node_it_end = orNode.end(); SatClause clause(n_children + 1); for(int i = 0; node_it != node_it_end; ++node_it, ++i) { clause[i] = toCNF(*node_it); @@ -155,7 +155,7 @@ SatLiteral TseitinCnfStream::handleOr(const Node& orNode) { return orLit; } -SatLiteral TseitinCnfStream::handleAnd(const Node& andNode) { +SatLiteral TseitinCnfStream::handleAnd(const TNode& andNode) { Assert(!isCached(andNode), "Atom already mapped!"); Assert(andNode.getKind() == AND, "Expecting an AND expression!"); Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!"); @@ -164,8 +164,8 @@ SatLiteral TseitinCnfStream::handleAnd(const Node& andNode) { unsigned n_children = andNode.getNumChildren(); // Transform all the children first (remembering the negation) - Node::iterator node_it = andNode.begin(); - Node::iterator node_it_end = andNode.end(); + TNode::const_iterator node_it = andNode.begin(); + TNode::const_iterator node_it_end = andNode.end(); SatClause clause(n_children + 1); for(int i = 0; node_it != node_it_end; ++node_it, ++i) { clause[i] = ~toCNF(*node_it); @@ -190,7 +190,7 @@ SatLiteral TseitinCnfStream::handleAnd(const Node& andNode) { return andLit; } -SatLiteral TseitinCnfStream::handleImplies(const Node& impliesNode) { +SatLiteral TseitinCnfStream::handleImplies(const TNode& impliesNode) { Assert(!isCached(impliesNode), "Atom already mapped!"); Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!"); Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!"); @@ -215,7 +215,7 @@ SatLiteral TseitinCnfStream::handleImplies(const Node& impliesNode) { } -SatLiteral TseitinCnfStream::handleIff(const Node& iffNode) { +SatLiteral TseitinCnfStream::handleIff(const TNode& iffNode) { Assert(!isCached(iffNode), "Atom already mapped!"); Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!"); Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!"); @@ -245,7 +245,7 @@ SatLiteral TseitinCnfStream::handleIff(const Node& iffNode) { } -SatLiteral TseitinCnfStream::handleNot(const Node& notNode) { +SatLiteral TseitinCnfStream::handleNot(const TNode& notNode) { Assert(!isCached(notNode), "Atom already mapped!"); Assert(notNode.getKind() == NOT, "Expecting a NOT expression!"); Assert(notNode.getNumChildren() == 1, "Expecting exactly 2 children!"); @@ -258,7 +258,7 @@ SatLiteral TseitinCnfStream::handleNot(const Node& notNode) { return notLit; } -SatLiteral TseitinCnfStream::handleIte(const Node& iteNode) { +SatLiteral TseitinCnfStream::handleIte(const TNode& iteNode) { Assert(iteNode.getKind() == ITE); Assert(iteNode.getNumChildren() == 3); @@ -283,7 +283,7 @@ SatLiteral TseitinCnfStream::handleIte(const Node& iteNode) { return iteLit; } -SatLiteral TseitinCnfStream::toCNF(const Node& node) { +SatLiteral TseitinCnfStream::toCNF(const TNode& node) { // If the node has already been translated, return the previous translation if(isCached(node)) { @@ -316,12 +316,12 @@ SatLiteral TseitinCnfStream::toCNF(const Node& node) { } } -void TseitinCnfStream::convertAndAssert(const Node& node) { +void TseitinCnfStream::convertAndAssert(const TNode& node) { Debug("cnf") << "convertAndAssert(" << node << ")" << endl; // If the node is a conjuntion, we handle each conjunct separatelu if (node.getKind() == AND) { - Node::iterator conjunct = node.begin(); - Node::iterator node_end = node.end(); + TNode::const_iterator conjunct = node.begin(); + TNode::const_iterator node_end = node.end(); while (conjunct != node_end) { convertAndAssert(*conjunct); ++ conjunct; @@ -332,7 +332,7 @@ void TseitinCnfStream::convertAndAssert(const Node& node) { if (node.getKind() == OR) { int nChildren = node.getNumChildren(); SatClause clause(nChildren); - Node::iterator disjunct = node.begin(); + TNode::const_iterator disjunct = node.begin(); for (int i = 0; i < nChildren; ++ disjunct, ++ i) { clause[i] = toCNF(*disjunct); } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index d7bb3c265..83a6aa68f 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -81,14 +81,14 @@ protected: * @param node the node * @return true if the node has been cached */ - bool isCached(const Node& node) const; + bool isCached(const TNode& node) const; /** * Returns the cashed literal corresponding to the given node. * @param node the node to lookup * @return returns the corresponding literal */ - SatLiteral lookupInCache(const Node& n) const; + SatLiteral lookupInCache(const TNode& n) const; /** * Caches the pair of the node and the literal corresponding to the @@ -96,7 +96,7 @@ protected: * @param node node * @param lit */ - void cacheTranslation(const Node& node, SatLiteral lit); + void cacheTranslation(const TNode& node, SatLiteral lit); /** * Acquires a new variable from the SAT solver to represent the node and @@ -104,7 +104,7 @@ protected: * @param node a formula * @return the literal corresponding to the formula */ - SatLiteral newLiteral(const Node& node); + SatLiteral newLiteral(const TNode& node); public: @@ -128,7 +128,7 @@ public: * @param node node to convert and assert * @param whether the sat solver can choose to remove this clause */ - virtual void convertAndAssert(const Node& node) = 0; + virtual void convertAndAssert(const TNode& node) = 0; }; /* class CnfStream */ @@ -150,7 +150,7 @@ public: * Convert a given formula to CNF and assert it to the SAT solver. * @param node the formula to assert */ - void convertAndAssert(const Node& node); + void convertAndAssert(const TNode& node); /** * Constructs the stream to use the given sat solver. @@ -170,21 +170,21 @@ private: // - returning l // // handleX( n ) can assume that n is not in d_translationCache - SatLiteral handleAtom(const Node& node); - SatLiteral handleNot(const Node& node); - SatLiteral handleXor(const Node& node); - SatLiteral handleImplies(const Node& node); - SatLiteral handleIff(const Node& node); - SatLiteral handleIte(const Node& node); - SatLiteral handleAnd(const Node& node); - SatLiteral handleOr(const Node& node); + SatLiteral handleAtom(const TNode& node); + SatLiteral handleNot(const TNode& node); + SatLiteral handleXor(const TNode& node); + SatLiteral handleImplies(const TNode& node); + SatLiteral handleIff(const TNode& node); + SatLiteral handleIte(const TNode& node); + SatLiteral handleAnd(const TNode& node); + SatLiteral handleOr(const TNode& node); /** * Transforms the node into CNF recursively. * @param node the formula to transform * @return the literal representing the root of the formula */ - SatLiteral toCNF(const Node& node); + SatLiteral toCNF(const TNode& node); }; /* class TseitinCnfStream */ |