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.cpp | |
parent | 105503064be6a198dd864d1e95d6d79e1af51d25 (diff) |
from meeting
Diffstat (limited to 'src/expr/expr_manager.cpp')
-rw-r--r-- | src/expr/expr_manager.cpp | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp new file mode 100644 index 000000000..90f10d8f7 --- /dev/null +++ b/src/expr/expr_manager.cpp @@ -0,0 +1,52 @@ +/********************* -*- C++ -*- */ +/** expr_manager.cpp + ** 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. + ** + ** Expression manager implementation. + **/ + +#include "core/expr_builder.h" +#include "core/expr_manager.h" +#include "core/cvc4_expr.h" + +namespace CVC4 { + +__thread ExprManager* ExprManager::s_current = 0; + +// general expression-builders + +Expr ExprManager::mkExpr(Kind kind) { + return ExprBuilder(this, kind); +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1) { + return ExprBuilder(this, kind) << child1; +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { + return ExprBuilder(this, kind) << child1 << child2; +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) { + return ExprBuilder(this, kind) << child1 << child2 << child3; +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4) { + return ExprBuilder(this, kind) << child1 << child2 << child3 << child4; +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) { + return ExprBuilder(this, kind) << child1 << child2 << child3 << child4 << child5; +} + +// N-ary version +Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) { + return ExprBuilder(this, kind).append(children); +} + +} /* CVC4 namespace */ |