diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-17 17:11:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-17 17:11:35 +0000 |
commit | 73d8c7a4f4896455fef39c44c80bf3df30a52d89 (patch) | |
tree | 9a515d8f3290f2842ab8ec4ae66433bbfb5c529e /src/expr/expr_manager.h | |
parent | 105503064be6a198dd864d1e95d6d79e1af51d25 (diff) |
from meeting
Diffstat (limited to 'src/expr/expr_manager.h')
-rw-r--r-- | src/expr/expr_manager.h | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h new file mode 100644 index 000000000..048250485 --- /dev/null +++ b/src/expr/expr_manager.h @@ -0,0 +1,58 @@ +/********************* -*- C++ -*- */ +/** expr_manager.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + **/ + +#ifndef __CVC4_EXPR_MANAGER_H +#define __CVC4_EXPR_MANAGER_H + +#include <vector> +#include "cvc4_expr.h" +#include "core/kind.h" + +namespace CVC4 { + +class ExprManager { + static __thread ExprManager* s_current; + +public: + static ExprManager* currentEM() { return s_current; } + + // general expression-builders + Expr mkExpr(Kind kind); + Expr mkExpr(Kind kind, Expr child1); + Expr mkExpr(Kind kind, Expr child1, Expr child2); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + // N-ary version + Expr mkExpr(Kind kind, std::vector<Expr> children); + + // TODO: these use the current EM (but must be renamed) + /* + static Expr mkExpr(Kind kind) + { currentEM()->mkExpr(kind); } + static Expr mkExpr(Kind kind, Expr child1); + { currentEM()->mkExpr(kind, child1); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2); + { currentEM()->mkExpr(kind, child1, child2); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + { currentEM()->mkExpr(kind, child1, child2, child3); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + { currentEM()->mkExpr(kind, child1, child2, child3, child4); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } + */ + + // do we want a varargs one? perhaps not.. +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4_EXPR_MANAGER_H */ |