diff options
Diffstat (limited to 'src/util/statistics.cpp')
-rw-r--r-- | src/util/statistics.cpp | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index 368335f7e..73ea5b1b1 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -19,6 +19,7 @@ #include <typeinfo> +#include "util/safe_print.h" #include "util/statistics_registry.h" // for details about class Stat @@ -116,6 +117,20 @@ void StatisticsBase::flushInformation(std::ostream &out) const { #endif /* CVC4_STATISTICS_ON */ } +void StatisticsBase::safeFlushInformation(int fd) const { +#ifdef CVC4_STATISTICS_ON + for (StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { + Stat* s = *i; + if (d_prefix.size() != 0) { + safe_print(fd, d_prefix.c_str()); + safe_print(fd, s_regDelim.c_str()); + } + s->safeFlushStat(fd); + safe_print(fd, "\n"); + } +#endif /* CVC4_STATISTICS_ON */ +} + SExpr StatisticsBase::getStatistic(std::string name) const { SExpr value; IntStat s(name, 0); |