summaryrefslogtreecommitdiff
path: root/src/util/stats.cpp
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2010-06-18 22:24:59 +0000
committerTim King <taking@cs.nyu.edu>2010-06-18 22:24:59 +0000
commitfd6af9181e763cd9564245114cfa47f3952484db (patch)
tree0b058ad4e0624f1bf11ed9c65d63a4cfbdbdc66e /src/util/stats.cpp
parent968f250b473d97db537aa7628bf111d15a2db299 (diff)
Merging the statistics branch into the main trunk. I'll go over how to use this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating.
Diffstat (limited to 'src/util/stats.cpp')
-rw-r--r--src/util/stats.cpp39
1 files changed, 39 insertions, 0 deletions
diff --git a/src/util/stats.cpp b/src/util/stats.cpp
new file mode 100644
index 000000000..cf7b3ad51
--- /dev/null
+++ b/src/util/stats.cpp
@@ -0,0 +1,39 @@
+/********************* */
+/*! \file stats.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** rief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "util/stats.h"
+
+using namespace CVC4;
+
+StatisticsRegistry::StatSet StatisticsRegistry::d_registeredStats;
+
+std::string Stat::s_delim(",");
+
+
+
+
+void StatisticsRegistry::flushStatistics(std::ostream& out){
+#ifdef CVC4_STATISTICS_ON
+ for(StatSet::iterator i=d_registeredStats.begin();i != d_registeredStats.end();++i){
+ Stat* s = *i;
+ s->flushStat(out);
+ out << std::endl;
+ }
+#endif
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback