summaryrefslogtreecommitdiff
path: root/src/expr/expr_manager_template.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-09-28 19:20:02 +0000
committerMorgan Deters <mdeters@gmail.com>2012-09-28 19:20:02 +0000
commitb5178b5e0e520c388d45918fed8cf874d1b61280 (patch)
tree4e6e7768064ef8f526107127fceda51b21aa0cae /src/expr/expr_manager_template.h
parent6a3a0b0a60fd29d67f013b2150ba47d401a3e39c (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/expr_manager_template.h')
-rw-r--r--src/expr/expr_manager_template.h11
1 files changed, 11 insertions, 0 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback