From e112de2be02760f66505a09e76269cca272dc988 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 18 Dec 2009 19:47:42 +0000 Subject: [PATCH] numerous fixes to nodes; more coming --- src/expr/node.cpp | 5 --- src/expr/node.h | 14 ++++----- src/expr/node_builder.h | 64 ++++++++++++++++++++++++++++----------- src/expr/node_manager.cpp | 20 ++++++------ src/expr/node_value.cpp | 4 +-- src/expr/node_value.h | 12 +++++--- 6 files changed, 73 insertions(+), 46 deletions(-) diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 9c73b982c..b87acb1f2 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -79,11 +79,6 @@ Node& Node::operator=(const Node& e) { return *this; } -NodeValue const* Node::operator->() const { - Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); - return d_ev; -} - uint64_t Node::hash() const { Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); return d_ev->hash(); diff --git a/src/expr/node.h b/src/expr/node.h index 9bb138b21..fd2603ffa 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -67,15 +67,13 @@ class Node { * 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; - /** Access to the encapsulated expression. - * @return the encapsulated expression. */ - NodeValue const* operator->() const; - /** * 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 @@ -85,8 +83,8 @@ class Node { */ void assignNodeValue(NodeValue* ev); - typedef NodeValue::iterator ev_iterator; - typedef NodeValue::const_iterator const_ev_iterator; + typedef NodeValue::ev_iterator ev_iterator; + typedef NodeValue::const_ev_iterator const_ev_iterator; inline ev_iterator ev_begin(); inline ev_iterator ev_end(); @@ -161,7 +159,9 @@ inline bool Node::operator<(const Node& e) const { return d_ev->d_id < e.d_ev->d_id; } -inline std::ostream& operator<<(std::ostream& out, const Node& e) { +inline std::ostream& + +operator<<(std::ostream& out, const Node& e) { e.toStream(out); return out; } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index b974ecc67..1dee91735 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -32,6 +32,7 @@ namespace CVC4 { #include "expr/kind.h" #include "util/Assert.h" #include "expr/node_value.h" +#include "util/output.h" namespace CVC4 { @@ -82,6 +83,15 @@ class NodeBuilder { } } + void crop() { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + if(EXPECT_FALSE( evIsAllocated() ) && EXPECT_TRUE( d_size > d_ev->d_nchildren )) { + d_ev = (NodeValue*) + std::realloc(d_ev, sizeof(NodeValue) + + ( sizeof(NodeValue*) * (d_size = d_ev->d_nchildren) )); + } + } + public: inline NodeBuilder(); @@ -95,10 +105,22 @@ public: typedef NodeValue::ev_iterator iterator; typedef NodeValue::const_ev_iterator const_iterator; - iterator begin() { return d_ev->ev_begin(); } - iterator end() { return d_ev->ev_end(); } - const_iterator begin() const { return d_ev->ev_begin(); } - const_iterator end() const { return d_ev->ev_end(); } + iterator begin() { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + return d_ev->ev_begin(); + } + iterator end() { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + return d_ev->ev_end(); + } + const_iterator begin() const { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + return d_ev->ev_begin(); + } + const_iterator end() const { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + return d_ev->ev_end(); + } // Compound expression constructors /* @@ -127,21 +149,25 @@ public: // "Stream" expression constructor syntax NodeBuilder& operator<<(const Kind& k) { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); Assert(d_ev->d_kind == UNDEFINED_KIND); d_ev->d_kind = k; return *this; } NodeBuilder& operator<<(const Node& n) { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); return append(n); } // For pushing sequences of children NodeBuilder& append(const std::vector& children) { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); return append(children.begin(), children.end()); } NodeBuilder& append(const Node& n) { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); allocateEvIfNecessaryForAppend(); NodeValue* ev = n.d_ev; d_hash = NodeValue::computeHash(d_hash, ev); @@ -152,20 +178,13 @@ public: template NodeBuilder& append(const Iterator& begin, const Iterator& end) { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); for(Iterator i = begin; i != end; ++i) { append(*i); } return *this; } - void crop() { - if(EXPECT_FALSE( evIsAllocated() ) && d_size > d_ev->d_nchildren) { - d_ev = (NodeValue*) - std::realloc(d_ev, sizeof(NodeValue) + - ( sizeof(NodeValue*) * (d_size = d_ev->d_nchildren) )); - } - } - // not const operator Node(); @@ -356,6 +375,7 @@ inline NodeBuilder::NodeBuilder(Kind k) : d_inlineEv(0), d_childrenStorage(0) { + Message() << "kind " << k << std::endl; d_inlineEv.d_kind = k; } @@ -412,19 +432,25 @@ inline NodeBuilder::NodeBuilder(NodeManager* nm, Kind k) : d_inlineEv(0), d_childrenStorage() { + Message() << "kind " << k << std::endl; d_inlineEv.d_kind = k; } template inline NodeBuilder::~NodeBuilder() { - for(iterator i = begin(); - i != end(); + Assert(d_used, "NodeBuilder unused at destruction"); + + return; + /* + for(iterator i = d_ev->ev_begin(); + i != d_ev->ev_end(); ++i) { (*i)->dec(); } if(evIsAllocated()) { free(d_ev); } + */ } template @@ -472,33 +498,35 @@ void NodeBuilder::realloc(size_t toSize, bool copy) { template NodeBuilder::operator Node() {// not const + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); Assert(d_ev->d_kind != UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); - Assert(! d_used, "This NodeBuilder has already been used!"); // implementation differs depending on whether the expression value // was malloc'ed or not if(EXPECT_FALSE( evIsAllocated() )) { NodeValue *ev = d_nm->lookupNoInsert(d_hash, d_ev); - if(ev != d_ev) { + if(ev != NULL) { // expression already exists in node manager + d_used = true; return Node(ev); } // otherwise create the canonical expression value for this node crop(); - d_used = true; ev = d_ev; d_ev = NULL; // this inserts into the NodeManager; // return the result of lookup() in case another thread beat us to it + d_used = true; return d_nm->lookup(d_hash, ev); } NodeValue *ev = d_nm->lookupNoInsert(d_hash, &d_inlineEv); - if(ev != &d_inlineEv) { + if(ev != NULL) { // expression already exists in node manager + d_used = true; return Node(ev); } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index d752db88f..eba8c4d18 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -16,6 +16,7 @@ #include "node_builder.h" #include "node_manager.h" #include "expr/node.h" +#include "util/output.h" namespace CVC4 { @@ -43,15 +44,15 @@ Node NodeManager::lookup(uint64_t hash, NodeValue* ev) { continue; } - NodeValue::const_iterator c1 = ev->ev_begin(); - NodeValue::iterator c2 = j->d_ev->ev_begin(); + NodeValue::const_ev_iterator c1 = ev->ev_begin(); + NodeValue::ev_iterator c2 = j->d_ev->ev_begin(); for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) { - if((*c1).d_ev != (*c2).d_ev) { + if(*c1 != *c2) { break; } } - if(c1 != ev->ev_end() || c2 != j->end()) { + if(c1 != ev->ev_end() || c2 != j->d_ev->ev_end()) { continue; } @@ -83,21 +84,22 @@ NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) { continue; } - NodeValue::const_iterator c1 = ev->ev_begin(); - NodeValue::iterator c2 = j->d_ev->ev_begin(); + NodeValue::const_ev_iterator c1 = ev->ev_begin(); + NodeValue::ev_iterator c2 = j->d_ev->ev_begin(); for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) { - if((*c1).d_ev != (*c2).d_ev) { + Debug("expr") << "comparing " << c1 << " and " << c2 << std::endl; + if(*c1 != *c2) { break; } } - if(c1 != ev->ev_end() || c2 != j->end()) { + if(c1 != ev->ev_end() || c2 != j->d_ev->ev_end()) { continue; } return j->d_ev; } - // didn't find it + // didn't find it, don't insert return 0; } } diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 6724b0771..554655573 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -104,8 +104,8 @@ void NodeValue::toStream(std::ostream& out) const { if(d_kind == VARIABLE) { out << ":" << this; } else { - for(const_iterator i = begin(); i != end(); ++i) { - if(i != end()) { + for(const_ev_iterator i = ev_begin(); i != ev_end(); ++i) { + if(i != ev_end()) { out << " "; } out << *i; diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 352be7d27..954fe0aaa 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -97,7 +97,8 @@ class NodeValue { * @return the hash value */ template - static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) { + static uint64_t computeHash(uint64_t hash, const_iterator_type begin, + const_iterator_type end) { for(const_iterator_type i = begin; i != end; ++i) { hash = computeHash(hash, *i); } @@ -105,7 +106,8 @@ class NodeValue { } static uint64_t computeHash(uint64_t hash, const NodeValue* ev) { - return ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId(); + return + ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId(); } typedef NodeValue** ev_iterator; @@ -120,7 +122,7 @@ class NodeValue { class node_iterator { const_ev_iterator d_i; public: - node_iterator(const_ev_iterator i) : d_i(i) {} + explicit node_iterator(const_ev_iterator i) : d_i(i) {} inline Node operator*(); @@ -132,7 +134,7 @@ class NodeValue { return d_i != i.d_i; } - node_iterator& operator++() { + node_iterator operator++() { ++d_i; return *this; } @@ -175,7 +177,7 @@ namespace CVC4 { namespace expr { inline Node NodeValue::node_iterator::operator*() { - return Node(*d_i); + return Node((NodeValue*) d_i); } }/* CVC4::expr namespace */ -- 2.30.2