Separate public-facing and internal-facing interfaces to Statistics.

The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).

The StatisticsRegistry is now internal-only.  However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).

This is part of the ongoing effort to clean up the public interface.

(this commit was certified error- and warning-free by the test-and-commit script.)

2 files changed, 74 insertions, 1 deletions

diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 836189991..2e1657777 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -4,7 +4,8 @@ CPLUSPLUS_TESTS = \
 	boilerplate \
 	ouroborous \
 	two_smt_engines \
-	smt2_compliance
+	smt2_compliance \
+	statistics
 
 if CVC4_BUILD_LIBCOMPAT
 CPLUSPLUS_TESTS += \
diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp
new file mode 100644
index 000000000..d4a958499
--- /dev/null
+++ b/test/system/statistics.cpp
@@ -0,0 +1,72 @@
+/*********************                                                        */
+/*! \file statistics.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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
+ **
+ ** \brief A simple statistics test for CVC4.
+ **
+ ** This simple test just makes sure that the statistics interface is
+ ** minimally functional.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+#include "util/statistics.h"
+
+using namespace CVC4;
+using namespace std;
+
+int main() {
+  ExprManager em;
+  Options opts;
+  SmtEngine smt(&em);
+  smt.setOption("incremental", SExpr("true"));
+  Expr x = em.mkVar("x", em.integerType());
+  Expr y = em.mkVar("y", em.integerType());
+  smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5))));
+  Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0)));
+  Result r = smt.query(q);
+
+  if(r != Result::INVALID) {
+    exit(1);
+  }
+
+  Statistics stats = smt.getStatistics();
+  for(Statistics::iterator i = stats.begin(); i != stats.end(); ++i) {
+    cout << "stat " << (*i).first << " is " << (*i).second << endl;
+  }
+
+  smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5))));
+  r = smt.query(q);
+  Statistics stats2 = smt.getStatistics();
+  bool different = false;
+  for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) {
+    cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl;
+    cout << "stat2 " << (*i).first << " is " << (*i).second << endl;
+    if(smt.getStatistic((*i).first) != (*i).second) {
+      cout << "SMT engine reports different value for statistic " << (*i).first << ": " << smt.getStatistic((*i).first) << endl;
+      exit(1);
+    }
+    different = different || stats.getStatistic((*i).first) != (*i).second;
+  }
+
+  if(!different) {
+    cout << "stats are the same!  bailing.." << endl;
+    exit(1);
+  }
+
+  return r == Result::VALID ? 0 : 1;
+}
+
+