diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
commit | 2163539a8b839acf98bda0e1a65f1fcca5232fb2 (patch) | |
tree | 207a09896626f678172ec774459defa6690b0200 /src/expr/expr_manager.cpp | |
parent | abe5fb451ae66a4bedc88d870e99f76de4eb323c (diff) |
work on propositional layer, expression builder support for large expressions, output classes, and minisat
Diffstat (limited to 'src/expr/expr_manager.cpp')
-rw-r--r-- | src/expr/expr_manager.cpp | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 3aeab8049..9b7697e4f 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -18,6 +18,42 @@ namespace CVC4 { __thread ExprManager* ExprManager::s_current = 0; +Expr ExprManager::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(); + for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) { + 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; + } +} + // general expression-builders Expr ExprManager::mkExpr(Kind kind) { @@ -49,4 +85,8 @@ Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) { return ExprBuilder(this, kind).append(children); } +Expr ExprManager::mkVar() { + return ExprBuilder(this, VARIABLE); +} + }/* CVC4 namespace */ |