1 files changed, 66 insertions, 40 deletions

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 4f2c356e8..1206a3e4a 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -47,6 +47,7 @@
 
 #include "base/exception.h"
 #include "lib/clock_gettime.h"
+#include "util/safe_print.h"
 #include "util/statistics.h"
 
 namespace CVC4 {
@@ -109,6 +110,13 @@ public:
   virtual void flushInformation(std::ostream& out) const = 0;
 
   /**
+   * Flush the value of this statistic to a file descriptor. Should finish the
+   * output with an end-of-line character. Should be safe to use in a signal
+   * handler.
+   */
+  virtual void safeFlushInformation(int fd) const = 0;
+
+  /**
    * Flush the name,value pair of this statistic to an output stream.
    * Uses the statistic delimiter string between name and value.
    *
@@ -121,6 +129,20 @@ public:
     }
   }
 
+  /**
+   * Flush the name,value pair of this statistic to a file descriptor. Uses the
+   * statistic delimiter string between name and value.
+   *
+   * May be redefined by a child class
+   */
+  virtual void safeFlushStat(int fd) const {
+    if (__CVC4_USE_STATISTICS) {
+      safe_print(fd, d_name.c_str());
+      safe_print(fd, ", ");
+      safeFlushInformation(fd);
+    }
+  }
+
   /** Get the name of this statistic. */
   const std::string& getName() const {
     return d_name;
@@ -210,6 +232,12 @@ public:
     }
   }
 
+  virtual void safeFlushInformation(int fd) const {
+    if (__CVC4_USE_STATISTICS) {
+      safe_print<T>(fd, getData());
+    }
+  }
+
   SExpr getValue() const {
     return mkSExpr(getData());
   }
@@ -298,7 +326,6 @@ public:
 
 };/* class ReferenceStat<T> */
 
-
 /**
  * A data statistic that keeps a T and sets it with setData().
  *
@@ -340,7 +367,6 @@ public:
 
 };/* class BackedStat<T> */
 
-
 /**
  * A wrapper Stat for another Stat.
  *
@@ -455,6 +481,10 @@ public:
     out << d_sized.size();
   }
 
+  void safeFlushInformation(int fd) const {
+    safe_print<uint64_t>(fd, d_sized.size());
+  }
+
   SExpr getValue() const {
     return SExpr(Integer(d_sized.size()));
   }
@@ -522,6 +552,12 @@ public:
     out << d_data << std::endl;
   }
 
+  virtual void safeFlushInformation(int fd) const {
+    // SExprStat is only used in statistics.cpp in copyFrom, which we cannot
+    // do in a signal handler anyway.
+    safe_print(fd, "<unsupported>");
+  }
+
   SExpr getValue() const {
     return d_data;
   }
@@ -529,44 +565,6 @@ public:
 };/* class SExprStat */
 
 template <class T>
-class ListStat : public Stat {
-private:
-  typedef std::vector<T> List;
-  List d_list;
-public:
-
-  /**
-   * Construct an integer-valued statistic with the given name and
-   * initial value.
-   */
-  ListStat(const std::string& name) : Stat(name) {}
-  ~ListStat() {}
-
-  void flushInformation(std::ostream& out) const{
-    if(__CVC4_USE_STATISTICS) {
-      typename List::const_iterator i = d_list.begin(), end =  d_list.end();
-      out << "[";
-      if(i != end){
-        out << *i;
-        ++i;
-        for(; i != end; ++i){
-          out << ", " << *i;
-        }
-      }
-      out << "]";
-    }
-  }
-
-  ListStat& operator<<(const T& val){
-    if(__CVC4_USE_STATISTICS) {
-      d_list.push_back(val);
-    }
-    return (*this);
-  }
-
-};/* class ListStat */
-
-template <class T>
 class HistogramStat : public Stat {
 private:
   typedef std::map<T, unsigned int> Histogram;
@@ -595,6 +593,28 @@ public:
     }
   }
 
+  virtual void safeFlushInformation(int fd) const {
+    if (__CVC4_USE_STATISTICS) {
+      typename Histogram::const_iterator i = d_hist.begin();
+      typename Histogram::const_iterator end = d_hist.end();
+      safe_print(fd, "[");
+      while (i != end) {
+        const T& key = (*i).first;
+        unsigned int count = (*i).second;
+        safe_print(fd, "(");
+        safe_print<T>(fd, key);
+        safe_print(fd, " : ");
+        safe_print<uint64_t>(fd, count);
+        safe_print(fd, ")");
+        ++i;
+        if (i != end) {
+          safe_print(fd, ", ");
+        }
+      }
+      safe_print(fd, "]");
+    }
+  }
+
   HistogramStat& operator<<(const T& val){
     if(__CVC4_USE_STATISTICS) {
       if(d_hist.find(val) == d_hist.end()){
@@ -643,6 +663,8 @@ public:
 
   virtual void flushInformation(std::ostream& out) const;
 
+  virtual void safeFlushInformation(int fd) const;
+
   SExpr getValue() const {
     std::vector<SExpr> v;
     for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
@@ -708,6 +730,10 @@ public:
 
   timespec getData() const;
 
+  virtual void safeFlushInformation(int fd) const {
+    safe_print<timespec>(fd, d_data);
+  }
+
   SExpr getValue() const;
 
 };/* class TimerStat */