diff options
Diffstat (limited to 'src/core/expr_manager.cpp')
-rw-r--r-- | src/core/expr_manager.cpp | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/src/core/expr_manager.cpp b/src/core/expr_manager.cpp new file mode 100644 index 000000000..93903c3aa --- /dev/null +++ b/src/core/expr_manager.cpp @@ -0,0 +1,49 @@ +/********************* -*- C++ -*- */ +/** expr_manager.cpp + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#include <vector> +#include "expr.h" +#include "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); } + */ +}; + +} /* CVC4 namespace */ |