return *d_node < *e.d_node;
}
-uint64_t Expr::hash() const {
+size_t Expr::hash() const {
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
return (d_node->isNull());
}
* Returns the hash value of the expression. Equal expression will have the
* same hash value.
*/
- uint64_t hash() const;
+ size_t hash() const;
/**
* Returns the kind of the expression (AND, PLUS ...).
return *this;
}
-uint64_t Node::hash() const {
- Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
- return d_ev->hash();
-}
-
Node Node::eqExpr(const Node& right) const {
return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
}
Node& operator=(const Node&);
- uint64_t hash() const;
+ size_t hash() const { return d_ev->getId(); }
uint64_t getId() const { return d_ev->getId(); }
Node eqExpr(const Node& right) const;
Debug("prop") << "append: " << this << " " << n << "[" << n.d_ev << "]" << std::endl;
allocateEvIfNecessaryForAppend();
NodeValue* ev = n.d_ev;
- d_hash = NodeValue::computeHash(d_hash, ev);
ev->inc();
d_ev->d_children[d_ev->d_nchildren++] = ev;
return *this;
// was malloc'ed or not
if(EXPECT_FALSE( evIsAllocated() )) {
- NodeValue *ev = d_nm->lookupNoInsert(d_hash, d_ev);
+ // Lookup the expression value in the pool we already have (with insert)
+ NodeValue* ev = d_nm->poolLookup(d_ev);
+ // If something else is there, we reuse it
if(ev != NULL) {
// expression already exists in node manager
dealloc();
Debug("prop") << "result: " << Node(ev) << std::endl;
return Node(ev);
}
-
- // otherwise create the canonical expression value for this node
+ // Otherwise crop and set the expression value to the allocate one
crop();
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;
- Node n = d_nm->lookup(d_hash, ev);
+ d_nm->poolInsert(ev);
+ Node n(ev);
Debug("prop") << "result: " << n << std::endl;
return n;
}
- NodeValue *ev = d_nm->lookupNoInsert(d_hash, &d_inlineEv);
+ // Lookup the expression value in the pool we already have
+ NodeValue* ev = d_nm->poolLookup(&d_inlineEv);
if(ev != NULL) {
// expression already exists in node manager
d_used = true;
d_used = true;
d_ev = NULL;
- // this inserts into the NodeManager;
- // return the result of lookup() in case another thread beat us to it
- if(ev->getNumChildren()) {
- Debug("prop") << "ev first child: " << *ev->ev_begin() << std::endl;
- }
- Node n = d_nm->lookup(d_hash, ev);
+ // Make the new expression
+ d_nm->poolInsert(ev);
+ Node n(ev);
Debug("prop") << "result: " << n << std::endl;
return n;
}
__thread NodeManager* NodeManager::s_current = 0;
-Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
- Assert(this != NULL, "Whoops, we have a bad expression manager!");
- Assert(ev != NULL, "lookup() expects a non-NULL NodeValue!");
-
- hash_t::iterator i = d_hash.find(hash);
- if(i == d_hash.end()) {
- // insert
- std::vector<Node> v;
- Node e(ev);
- v.push_back(e);
- d_hash.insert(std::make_pair(hash, v));
- return e;
- } else {
- for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
- if(ev->getKind() != j->getKind()) {
- continue;
- }
-
- if(ev->getNumChildren() != j->getNumChildren()) {
- continue;
- }
-
- 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 != *c2) {
- break;
- }
- }
-
- if(c1 != ev->ev_end() || c2 != j->d_ev->ev_end()) {
- continue;
- }
-
- return *j;
- }
-
- // didn't find it, insert
- Node e(ev);
- i->second.push_back(e);
- return e;
- }
+NodeManager::NodeManager() {
+ poolInsert(&NodeValue::s_null);
}
-NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
- Assert(this != NULL, "Whoops, we have a bad expression manager!");
- Assert(ev != NULL, "lookupNoInsert() expects a non-NULL NodeValue!");
-
- hash_t::iterator i = d_hash.find(hash);
- if(i == d_hash.end()) {
+NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
+ NodeValueSet::const_iterator find = d_nodeValueSet.find(nv);
+ if (find == d_nodeValueSet.end()) {
return NULL;
} else {
- for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
- if(ev->getKind() != j->getKind()) {
- continue;
- }
-
- if(ev->getNumChildren() != j->getNumChildren()) {
- continue;
- }
-
- 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) {
- Debug("expr") << "comparing " << c1 << " and " << c2 << std::endl;
- if(*c1 != *c2) {
- break;
- }
- }
-
- if(c1 != ev->ev_end() || c2 != j->d_ev->ev_end()) {
- continue;
- }
-
- return j->d_ev;
- }
-
- // didn't find it, don't insert
- return 0;
+ return *find;
}
}
+void NodeManager::poolInsert(NodeValue* nv) {
+ Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in"
+ "the pool!");
+ d_nodeValueSet.insert(nv);
+}
+
// general expression-builders
Node NodeManager::mkNode(Kind kind) {
#define __CVC4__NODE_MANAGER_H
#include <vector>
-#include <map>
+#include <ext/hash_set>
#include "node.h"
#include "kind.h"
+namespace __gnu_cxx {
+template<>
+ struct hash<CVC4::NodeValue*> {
+ size_t operator()(const CVC4::NodeValue* nv) const {
+ return (size_t)nv->hash();
+ }
+ };
+} /* __gnu_cxx namespace */
+
+
namespace CVC4 {
class NodeManager {
template <unsigned> friend class CVC4::NodeBuilder;
- typedef std::map<uint64_t, std::vector<Node> > hash_t;
- hash_t d_hash;
+ typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet;
+ NodeValueSet d_nodeValueSet;
- Node lookup(uint64_t hash, const Node& e) { return lookup(hash, e.d_ev); }
- Node lookup(uint64_t hash, NodeValue* e);
- NodeValue* lookupNoInsert(uint64_t hash, NodeValue* e);
+ NodeValue* poolLookup(NodeValue* nv) const;
+ void poolInsert(NodeValue* nv);
friend class NodeManagerScope;
public:
+
+ NodeManager();
+
static NodeManager* currentNM() { return s_current; }
// general expression-builders
}
}
-uint64_t NodeValue::hash() const {
- return computeHash(d_kind, ev_begin(), ev_end());
-}
-
void NodeValue::inc() {
// FIXME multithreading
if(EXPECT_TRUE( d_rc < MAX_RC )) {
/** Destructor decrements the ref counts of its children */
~NodeValue();
- /**
- * Computes the hash over the given iterator span of children, and the
- * root hash. The iterator should be either over a range of Node or pointers
- * to NodeValue.
- * @param hash the initial value for the hash
- * @param begin the begining of the range
- * @param end the end of the range
- * @return the hash value
- */
- template<typename const_iterator_type>
- 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);
- }
- return hash;
- }
-
- static uint64_t computeHash(uint64_t hash, const NodeValue* ev) {
- return
- ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId();
- }
-
typedef NodeValue** ev_iterator;
typedef NodeValue const* const* const_ev_iterator;
typedef node_iterator const_node_iterator;
public:
- /** Hash this expression.
- * @return the hash value of this expression. */
- uint64_t hash() const;
// Iterator support
-
typedef node_iterator iterator;
typedef node_iterator const_iterator;
const_iterator begin() const;
const_iterator end() const;
+ /**
+ * Hash this expression.
+ * @return the hash value of this expression.
+ */
+ size_t hash() const {
+ size_t hash = d_kind;
+ const_ev_iterator i = ev_begin();
+ const_ev_iterator i_end = ev_end();
+ while (i != i_end) {
+ hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
+ ++ i;
+ }
+ return hash;
+ }
+
+ inline bool compareTo(const NodeValue* nv) const {
+ if(d_kind != nv->d_kind)
+ return false;
+ if(d_nchildren != nv->d_nchildren)
+ return false;
+ const_ev_iterator i = ev_begin();
+ const_ev_iterator j = nv->ev_begin();
+ const_ev_iterator i_end = ev_end();
+ while(i != i_end) {
+ if ((*i) != (*j)) return false;
+ ++i; ++j;
+ }
+ return true;
+ }
+
+ // Comparison predicate
+ struct NodeValueEq {
+ bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
+ return nv1->compareTo(nv2);
+ }
+ };
+
+
unsigned getId() const { return d_id; }
Kind getKind() const { return (Kind) d_kind; }
unsigned getNumChildren() const { return d_nchildren; }
annotatedFormula returns [CVC4::Expr formula]
{
Debug("parser") << "annotated formula: " << LT(1)->getText() << endl;
- Kind kind;
+ Kind kind = UNDEFINED_KIND;
vector<Expr> args;
}
: /* a built-in operator application */
projects / cvc5.git / commitdiff