From b5178b5e0e520c388d45918fed8cf874d1b61280 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 28 Sep 2012 19:20:02 +0000
Subject: some fixes to build system

(this commit was certified error- and warning-free by the test-and-commit script.)
---
 src/util/exception.h             |  4 ++--
 src/util/statistics_registry.cpp | 13 +++++++++----
 2 files changed, 11 insertions(+), 6 deletions(-)

(limited to 'src/util')

diff --git a/src/util/exception.h b/src/util/exception.h
index 89e42b6d1..4241fb1f1 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -130,9 +130,9 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
 
 }/* CVC4 namespace */
 
-#if defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)
+#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
 #  include "util/Assert.h"
-#endif /* __BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST */
+#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && !__BUILDING_STATISTICS_FOR_EXPORT */
 
 namespace CVC4 {
 
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 48e1355ec..6194145a8 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -18,13 +18,14 @@
  **/
 
 #include "util/statistics_registry.h"
-#include "expr/node_manager.h"
-#include "expr/expr_manager_scope.h"
 #include "expr/expr_manager.h"
 #include "lib/clock_gettime.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_engine.h"
 
+#ifndef __BUILDING_STATISTICS_FOR_EXPORT
+#  include "smt/smt_engine_scope.h"
+#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */
+
 #ifdef CVC4_STATISTICS_ON
 #  define __CVC4_USE_STATISTICS true
 #else
@@ -42,6 +43,10 @@ inline StatisticsRegistry* getStatisticsRegistry(SmtEngine* smt) {
   return smt->d_statisticsRegistry;
 }
 
+inline StatisticsRegistry* getStatisticsRegistry(ExprManager* em) {
+  return em->getStatisticsRegistry();
+}
+
 }/* CVC4::stats namespace */
 
 #ifndef __BUILDING_STATISTICS_FOR_EXPORT
@@ -117,7 +122,7 @@ void TimerStat::stop() {
 }/* TimerStat::stop() */
 
 RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
-  d_reg(NodeManager::fromExprManager(&em)->getStatisticsRegistry()),
+  d_reg(stats::getStatisticsRegistry(&em)),
   d_stat(stat) {
   d_reg->registerStat_(d_stat);
 }
-- 
cgit v1.2.3