work on propositional layer, expression builder support for large expressions, output classes, and minisat

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 */