src/expr/expr_manager.h

   1 /*********************                                           -*- C++ -*-  */
   2 /** expr_manager.h
   3  ** This file is part of the CVC4 prototype.
   4  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
   5  ** Courant Institute of Mathematical Sciences
   6  ** New York University
   7  ** See the file COPYING in the top-level source directory for licensing
   8  ** information.
   9  **
  10  **/
  11
  12 #ifndef __CVC4__EXPR_MANAGER_H
  13 #define __CVC4__EXPR_MANAGER_H
  14
  15 #include <vector>
  16 #include <map>
  17
  18 #include "expr/expr.h"
  19 #include "kind.h"
  20
  21 namespace CVC4 {
  22
  23 namespace expr {
  24   class ExprBuilder;
  25 }/* CVC4::expr namespace */
  26
  27 class CVC4_PUBLIC ExprManager {
  28   static __thread ExprManager* s_current;
  29
  30   friend class CVC4::ExprBuilder;
  31
  32   typedef std::map<uint64_t, std::vector<Expr> > hash_t;
  33   hash_t d_hash;
  34
  35   Expr lookup(uint64_t hash, const Expr& e) {
  36     hash_t::iterator i = d_hash.find(hash);
  37     if(i == d_hash.end()) {
  38       // insert
  39       std::vector<Expr> v;
  40       v.push_back(e);
  41       d_hash.insert(std::make_pair(hash, v));
  42       return e;
  43     } else {
  44       for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
  45         if(e.getKind() != j->getKind())
  46           continue;
  47
  48         if(e.numChildren() != j->numChildren())
  49           continue;
  50
  51         Expr::iterator c1 = e.begin();
  52         Expr::iterator c2 = j->begin();
  53         while(c1 != e.end() && c2 != j->end()) {
  54           if(c1->d_ev != c2->d_ev)
  55             break;
  56         }
  57
  58         if(c1 != e.end() || c2 != j->end())
  59           continue;
  60
  61         return *j;
  62       }
  63       // didn't find it, insert
  64       std::vector<Expr> v;
  65       v.push_back(e);
  66       d_hash.insert(std::make_pair(hash, v));
  67       return e;
  68     }
  69   }
  70
  71 public:
  72   static ExprManager* currentEM() { return s_current; }
  73
  74   // general expression-builders
  75   Expr mkExpr(Kind kind);
  76   Expr mkExpr(Kind kind, Expr child1);
  77   Expr mkExpr(Kind kind, Expr child1, Expr child2);
  78   Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
  79   Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
  80   Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
  81   // N-ary version
  82   Expr mkExpr(Kind kind, std::vector<Expr> children);
  83
  84   // TODO: these use the current EM (but must be renamed)
  85   /*
  86   static Expr mkExpr(Kind kind)
  87   { currentEM()->mkExpr(kind); }
  88   static Expr mkExpr(Kind kind, Expr child1);
  89   { currentEM()->mkExpr(kind, child1); }
  90   static Expr mkExpr(Kind kind, Expr child1, Expr child2);
  91   { currentEM()->mkExpr(kind, child1, child2); }
  92   static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
  93   { currentEM()->mkExpr(kind, child1, child2, child3); }
  94   static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
  95   { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
  96   static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
  97   { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
  98   */
  99
 100   // do we want a varargs one?  perhaps not..
 101 };
 102
 103 }/* CVC4 namespace */
 104
 105 #endif /* __CVC4__EXPR_MANAGER_H */