diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 19:20:02 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 19:20:02 +0000 |
commit | b5178b5e0e520c388d45918fed8cf874d1b61280 (patch) | |
tree | 4e6e7768064ef8f526107127fceda51b21aa0cae /src/expr | |
parent | 6a3a0b0a60fd29d67f013b2150ba47d401a3e39c (diff) |
some fixes to build system
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 11 |
2 files changed, 15 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 516930bcd..be2804fd5 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -126,6 +126,10 @@ ExprManager::~ExprManager() throw() { } } +StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() { + return d_nodeManager->getStatisticsRegistry(); +} + const Options& ExprManager::getOptions() const { return d_nodeManager->getOptions(); } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 460e3f1dc..d883cd725 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -46,6 +46,7 @@ class NodeManager; class Options; class IntStat; class ExprManagerMapCollection; +class StatisticsRegistry; namespace expr { namespace pickle { @@ -57,6 +58,10 @@ namespace context { class Context; }/* CVC4::context namespace */ +namespace stats { + StatisticsRegistry* getStatisticsRegistry(ExprManager*); +}/* CVC4::stats namespace */ + class CVC4_PUBLIC ExprManager { private: /** The context */ @@ -98,6 +103,12 @@ private: /** NodeManager reaches in to get the NodeManager */ friend class NodeManager; + /** Statistics reach in to get the StatisticsRegistry */ + friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*); + + /** Get the underlying statistics registry. */ + StatisticsRegistry* getStatisticsRegistry() throw(); + // undefined, private copy constructor and assignment op (disallow copy) ExprManager(const ExprManager&) CVC4_UNDEFINED; ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED; |