diff options
Diffstat (limited to 'src/expr/expr_manager.h')
-rw-r--r-- | src/expr/expr_manager.h | 39 |
1 files changed, 4 insertions, 35 deletions
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index ee18ddc01..d311445f3 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -32,41 +32,7 @@ class CVC4_PUBLIC ExprManager { typedef std::map<uint64_t, std::vector<Expr> > hash_t; hash_t d_hash; - Expr lookup(uint64_t hash, const Expr& e) { - hash_t::iterator i = d_hash.find(hash); - if(i == d_hash.end()) { - // insert - std::vector<Expr> v; - v.push_back(e); - d_hash.insert(std::make_pair(hash, v)); - return e; - } else { - for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) { - if(e.getKind() != j->getKind()) - continue; - - if(e.numChildren() != j->numChildren()) - continue; - - Expr::iterator c1 = e.begin(); - Expr::iterator c2 = j->begin(); - while(c1 != e.end() && c2 != j->end()) { - if(c1->d_ev != c2->d_ev) - break; - } - - if(c1 != e.end() || c2 != j->end()) - continue; - - return *j; - } - // didn't find it, insert - std::vector<Expr> v; - v.push_back(e); - d_hash.insert(std::make_pair(hash, v)); - return e; - } - } + Expr lookup(uint64_t hash, const Expr& e); public: static ExprManager* currentEM() { return s_current; } @@ -81,6 +47,9 @@ public: // N-ary version Expr mkExpr(Kind kind, std::vector<Expr> children); + // variables are special, because duplicates are permitted + Expr mkVar(); + // TODO: these use the current EM (but must be renamed) /* static Expr mkExpr(Kind kind) |