diff options
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 76 |
1 files changed, 58 insertions, 18 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 8da87c9eb..ab52b9f40 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr_manager.cpp +/** node_manager.cpp ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -18,76 +18,116 @@ namespace CVC4 { __thread NodeManager* NodeManager::s_current = 0; -Node NodeManager::lookup(uint64_t hash, const Node& e) { - Assert(this != NULL, "Woops, we have a bad expression manager!"); +Node NodeManager::lookup(uint64_t hash, NodeValue* ev) { + Assert(this != NULL, "Whoops, we have a bad expression manager!"); 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(e.getKind() != j->getKind()) + if(ev->getKind() != j->getKind()) { continue; + } - if(e.numChildren() != j->numChildren()) + if(ev->numChildren() != j->numChildren()) { continue; + } - Node::const_iterator c1 = e.begin(); - Node::iterator c2 = j->begin(); - for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) { - if(c1->d_ev != c2->d_ev) + NodeValue::const_iterator c1 = ev->ev_begin(); + NodeValue::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) { break; + } } - if(c1 != e.end() || c2 != j->end()) + if(c1 != ev->ev_end() || c2 != j->end()) { continue; + } return *j; } // didn't find it, insert std::vector<Node> v; + Node e(ev); v.push_back(e); d_hash.insert(std::make_pair(hash, v)); return e; } } +NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) { + Assert(this != NULL, "Whoops, we have a bad expression manager!"); + hash_t::iterator i = d_hash.find(hash); + if(i == d_hash.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->numChildren() != j->numChildren()) { + continue; + } + + NodeValue::const_iterator c1 = ev->ev_begin(); + NodeValue::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) { + break; + } + } + + if(c1 != ev->ev_end() || c2 != j->end()) { + continue; + } + + return j->d_ev; + } + // didn't find it + return 0; + } +} + // general expression-builders Node NodeManager::mkExpr(Kind kind) { - return NodeBuilder(this, kind); + return NodeBuilder<>(this, kind); } Node NodeManager::mkExpr(Kind kind, const Node& child1) { - return NodeBuilder(this, kind) << child1; + return NodeBuilder<>(this, kind) << child1; } Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) { - return NodeBuilder(this, kind) << child1 << child2; + return NodeBuilder<>(this, kind) << child1 << child2; } Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) { - return NodeBuilder(this, kind) << child1 << child2 << child3; + return NodeBuilder<>(this, kind) << child1 << child2 << child3; } Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) { - return NodeBuilder(this, kind) << child1 << child2 << child3 << child4; + return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4; } Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) { - return NodeBuilder(this, kind) << child1 << child2 << child3 << child4 << child5; + return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5; } // N-ary version Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) { - return NodeBuilder(this, kind).append(children); + return NodeBuilder<>(this, kind).append(children); } Node NodeManager::mkVar() { - return NodeBuilder(this, VARIABLE); + return NodeBuilder<>(this, VARIABLE); } }/* CVC4 namespace */ |