From: Dejan Jovanović Date: Fri, 12 Feb 2010 01:07:22 +0000 (+0000) Subject: Changes to hashing that solve the xinetd boolean benchmark in 14s (from ~25min).... X-Git-Tag: cvc5-1.0.0~9258 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8316697801a73a14a2fe3845e0d0f5add63a18be;p=cvc5.git Changes to hashing that solve the xinetd boolean benchmark in 14s (from ~25min). Switched to standard hash_set, hash_map, new hash for the vector of node values (from boost), changed the hash for nodes to be over id's, all the hash values are now size_t. The parser is down from 11s to 10s on the benchmark, so most of the solve time is parsing and we need to figure this out. --- diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 283467fa8..0170296be 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -77,7 +77,7 @@ bool Expr::operator<(const Expr& e) const { 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()); } diff --git a/src/expr/expr.h b/src/expr/expr.h index 6e4a43d21..0943c13e4 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -92,7 +92,7 @@ public: * 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 ...). diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 6f1c525ca..f3115b17e 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -96,11 +96,6 @@ Node& Node::operator=(const Node& e) { 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); } diff --git a/src/expr/node.h b/src/expr/node.h index 3b0cb8abb..39eb3bcd7 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -119,7 +119,7 @@ public: 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; diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 765a2f493..ce56fc08c 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -192,7 +192,6 @@ public: 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; @@ -587,7 +586,9 @@ NodeBuilder::operator Node() {// not const // 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(); @@ -595,20 +596,19 @@ NodeBuilder::operator Node() {// not const 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; @@ -630,12 +630,9 @@ NodeBuilder::operator Node() {// not const 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; } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e9fdc69a8..3561f2119 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -22,88 +22,25 @@ namespace CVC4 { __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 v; - Node e(ev); - v.push_back(e); - d_hash.insert(std::make_pair(hash, v)); - return e; - } else { - for(std::vector::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::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) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 090398ce8..0abd86130 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -17,11 +17,21 @@ #define __CVC4__NODE_MANAGER_H #include -#include +#include #include "node.h" #include "kind.h" +namespace __gnu_cxx { +template<> + struct hash { + size_t operator()(const CVC4::NodeValue* nv) const { + return (size_t)nv->hash(); + } + }; +} /* __gnu_cxx namespace */ + + namespace CVC4 { class NodeManager { @@ -29,16 +39,18 @@ class NodeManager { template friend class CVC4::NodeBuilder; - typedef std::map > hash_t; - hash_t d_hash; + typedef __gnu_cxx::hash_set, 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 diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 575ab7d37..f8bf33b5c 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -40,10 +40,6 @@ NodeValue::~NodeValue() { } } -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 )) { diff --git a/src/expr/node_value.h b/src/expr/node_value.h index bb224e3b1..d86822b8d 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -88,29 +88,6 @@ class NodeValue { /** 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 - 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; @@ -153,12 +130,8 @@ class NodeValue { 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; @@ -168,6 +141,44 @@ public: 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; } diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index dbc9e1a21..4ecac0418 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -117,7 +117,7 @@ benchAttribute returns [Command* smt_command = 0] annotatedFormula returns [CVC4::Expr formula] { Debug("parser") << "annotated formula: " << LT(1)->getText() << endl; - Kind kind; + Kind kind = UNDEFINED_KIND; vector args; } : /* a built-in operator application */