1 /********************* -*- C++ -*- */
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
7 ** See the file COPYING in the top-level source directory for licensing
12 #ifndef __CVC4__EXPR_MANAGER_H
13 #define __CVC4__EXPR_MANAGER_H
18 #include "expr/expr.h"
25 }/* CVC4::expr namespace */
27 class CVC4_PUBLIC ExprManager
{
28 static __thread ExprManager
* s_current
;
30 friend class CVC4::ExprBuilder
;
32 typedef std::map
<uint64_t, std::vector
<Expr
> > hash_t
;
35 Expr
lookup(uint64_t hash
, const Expr
& e
) {
36 hash_t::iterator i
= d_hash
.find(hash
);
37 if(i
== d_hash
.end()) {
41 d_hash
.insert(std::make_pair(hash
, v
));
44 for(std::vector
<Expr
>::iterator j
= i
->second
.begin(); j
!= i
->second
.end(); ++j
) {
45 if(e
.getKind() != j
->getKind())
48 if(e
.numChildren() != j
->numChildren())
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
)
58 if(c1
!= e
.end() || c2
!= j
->end())
63 // didn't find it, insert
66 d_hash
.insert(std::make_pair(hash
, v
));
72 static ExprManager
* currentEM() { return s_current
; }
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
);
82 Expr
mkExpr(Kind kind
, std::vector
<Expr
> children
);
84 // TODO: these use the current EM (but must be renamed)
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); }
100 // do we want a varargs one? perhaps not..
103 }/* CVC4 namespace */
105 #endif /* __CVC4__EXPR_MANAGER_H */