New statistics registry (#6210)

This PR adds the next part of the new statistics setup: the registry.
The new statistics registry owns the actual data and only issues proxy objects that can be used to modify the internally stored data.
Once we replace the old statistics setup, the files should be renamed from statistics_reg.* to statistics_registry.*.

1 files changed, 33 insertions, 0 deletions

diff --git a/src/util/statistics_public.h b/src/util/statistics_public.h
new file mode 100644
index 000000000..c2d054f00
--- /dev/null
+++ b/src/util/statistics_public.h
@@ -0,0 +1,33 @@
+/*********************                                                        */
+/*! \file statistics_public.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Registration of public statistics
+ **
+ ** Registration and documentation for all public statistics.
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef CVC4__UTIL__STATISTICS_PUBLIC_H
+#define CVC4__UTIL__STATISTICS_PUBLIC_H
+
+namespace cvc5 {
+
+class StatisticsRegistry;
+
+/**
+ * Preregisters all public (non-expert) statistics.
+ */
+void registerPublicStatistics(StatisticsRegistry& reg);
+
+}  // namespace cvc5
+
+#endif