diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-15 22:11:11 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-15 22:11:11 +0000 |
| commit | e45de2ba8a8c34d3212327ed6f021462c149825c (patch) | |
| tree | eb82e6d1a3bc9b133d501ff89742384156a64b3b /src/expr/expr_manager_template.cpp | |
| parent | 225f4e77f3afdebdfa046834ef7c006b9b8ec77c (diff) | |
partial merge from portfolio branch, adding conversions (library-internal-only of course) between Exprs and Nodes, Types and TypeNodes, ExprManagers and NodeManagers.
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 5d34fb53c..6e8b6c63c 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -57,7 +57,7 @@ ${includes} } \ ++ *(d_exprStatisticsVars[type]); \ } -#else +#else #define INC_STAT(kind) #define INC_STAT_VAR(type) #endif @@ -70,8 +70,8 @@ namespace CVC4 { ExprManager::ExprManager() : d_ctxt(new Context), - d_nodeManager(new NodeManager(d_ctxt)) { -#ifdef CVC4_STATISTICS_ON + d_nodeManager(new NodeManager(d_ctxt, this)) { +#ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { d_exprStatistics[i] = NULL; } @@ -83,8 +83,8 @@ ExprManager::ExprManager() : ExprManager::ExprManager(const Options& options) : d_ctxt(new Context), - d_nodeManager(new NodeManager(d_ctxt, options)) { -#ifdef CVC4_STATISTICS_ON + d_nodeManager(new NodeManager(d_ctxt, this, options)) { +#ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i <= LAST_TYPE; ++ i) { d_exprStatisticsVars[i] = NULL; } @@ -95,7 +95,7 @@ ExprManager::ExprManager(const Options& options) : } ExprManager::~ExprManager() { -#ifdef CVC4_STATISTICS_ON +#ifdef CVC4_STATISTICS_ON NodeManagerScope nms(d_nodeManager); for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { if (d_exprStatistics[i] != NULL) { @@ -135,7 +135,7 @@ IntegerType ExprManager::integerType() const { } Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { - const unsigned n = 1; + const unsigned n = 1; CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", |