summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-03-01 08:40:11 -0800
committerGitHub <noreply@github.com>2021-03-01 16:40:11 +0000
commit9b48d6e5abd3682ec64cd3f6c9b024fa2a7321aa (patch)
tree559b96a6015dda1646ccfc399b7cc66fd2e170e8 /test
parent4e69b8bb9cb9787963036343e08030283515ccc5 (diff)
google test: util: Migrate stats_black. (#6029)
Diffstat (limited to 'test')
-rw-r--r--test/unit/util/CMakeLists.txt2
-rw-r--r--test/unit/util/stats_black.cpp185
-rw-r--r--test/unit/util/stats_black.h196
3 files changed, 186 insertions, 197 deletions
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index e1a0e863b..82aa2e0a2 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -32,4 +32,4 @@ cvc4_add_unit_test_white(rational_white util)
if(CVC4_USE_POLY_IMP)
cvc4_add_unit_test_black(real_algebraic_number_black util)
endif()
-cvc4_add_cxx_unit_test_black(stats_black util)
+cvc4_add_unit_test_black(stats_black util)
diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp
new file mode 100644
index 000000000..2734b426d
--- /dev/null
+++ b/test/unit/util/stats_black.cpp
@@ -0,0 +1,185 @@
+/********************* */
+/*! \file stats_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli, Aina Niemetz, Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Black box testing of CVC4::Stat and associated classes
+ **
+ ** Black box testing of CVC4::Stat and associated classes.
+ **/
+
+#include <fcntl.h>
+
+#include <ctime>
+#include <sstream>
+#include <string>
+
+#include "expr/proof_rule.h"
+#include "lib/clock_gettime.h"
+#include "test.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace test {
+
+/**
+ * This is a duplicate of operator== in statistics_registry.h.
+ * This is duplicated here to try to avoid polluting top namepsace.
+ *
+ * If operator== is in the CVC4 namespace, there are some circumstances
+ * where clang does not find this operator.
+ */
+bool operator==(const timespec& a, const timespec& b)
+{
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
+}
+
+class TestUtilBlackStats : public TestInternal
+{
+};
+
+TEST_F(TestUtilBlackStats, stats)
+{
+#ifdef CVC4_STATISTICS_ON
+ std::string empty, bar = "bar", baz = "baz";
+ ReferenceStat<std::string> refStr("stat #1", empty);
+ ReferenceStat<std::string> refStr2("refStr2", bar);
+ BackedStat<std::string> backedStr("backed", baz);
+
+ BackedStat<double> backedDouble("backedDouble", 16.5);
+ BackedStat<double> backedNegDouble("backedNegDouble", -16.5);
+ BackedStat<double> backedDoubleNoDec("backedDoubleNoDec", 2.0);
+ BackedStat<bool> backedBool("backedBool", true);
+ BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF);
+ HistogramStat<int64_t> histStat("hist");
+ histStat << 5;
+ histStat << 6;
+ histStat << 5;
+ histStat << 10;
+ histStat << 10;
+ histStat << 0;
+ IntegralHistogramStat<std::int64_t> histIntStat("hist-int");
+ histIntStat << 15 << 16 << 15 << 14 << 16;
+ IntegralHistogramStat<CVC4::PfRule> histPfRuleStat("hist-pfrule");
+ histPfRuleStat << PfRule::ASSUME << PfRule::SCOPE << PfRule::ASSUME;
+
+ // A statistic with no safe_print support
+ BackedStat<std::string*> backedUnsupported("backedUnsupported", &bar);
+
+ IntStat sInt("my int", 10);
+ TimerStat sTimer("a timer ! for measuring time");
+
+ ASSERT_EQ(refStr.getName(), "stat #1");
+ ASSERT_EQ(refStr2.getName(), "refStr2");
+ ASSERT_EQ(backedStr.getName(), "backed");
+ ASSERT_EQ(sInt.getName(), "my int");
+ ASSERT_EQ(sTimer.getName(), "a timer ! for measuring time");
+ ASSERT_EQ(histIntStat.getName(), "hist-int");
+ ASSERT_EQ(histPfRuleStat.getName(), "hist-pfrule");
+
+ ASSERT_EQ(refStr.getData(), empty);
+ ASSERT_EQ(refStr2.getData(), bar);
+ empty = "a different string";
+ bar += " and with an addition";
+ ASSERT_EQ(refStr.getData(), empty);
+ ASSERT_EQ(refStr2.getData(), bar);
+
+ ASSERT_EQ(backedStr.getData(), "baz");
+ baz = "something else";
+ ASSERT_EQ(backedStr.getData(), "baz");
+
+ ASSERT_EQ(sInt.getData(), 10);
+ sInt.setData(100);
+ ASSERT_EQ(sInt.getData(), 100);
+
+ ASSERT_TRUE(sTimer.getData() == timespec());
+
+ std::stringstream sstr;
+
+ refStr.flushInformation(sstr);
+ ASSERT_EQ(sstr.str(), empty);
+ sstr.str("");
+ refStr2.flushInformation(sstr);
+ ASSERT_EQ(sstr.str(), bar);
+ sstr.str("");
+ backedStr.flushInformation(sstr);
+ ASSERT_EQ(sstr.str(), "baz");
+ sstr.str("");
+ sInt.flushInformation(sstr);
+ ASSERT_EQ(sstr.str(), "100");
+ sstr.str("");
+ sTimer.flushInformation(sstr);
+ ASSERT_EQ(sstr.str(), "0.000000000");
+
+ // Test safeFlushInformation (and safe_print functions)
+ char tmp_filename[] = "testXXXXXX";
+ int fd = mkstemp(tmp_filename);
+ ASSERT_NE(fd, -1);
+ refStr.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ refStr2.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedStr.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ sInt.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ sTimer.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedDouble.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedNegDouble.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedDoubleNoDec.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedAddr.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedBool.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ histStat.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ histIntStat.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ histPfRuleStat.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedUnsupported.safeFlushInformation(fd);
+ off_t file_size = lseek(fd, 0, SEEK_CUR);
+ close(fd);
+
+ char* buf = new char[file_size];
+ fd = open(tmp_filename, O_RDONLY);
+ ASSERT_NE(fd, -1);
+ ssize_t n_read = pread(fd, buf, file_size, 0);
+ ASSERT_EQ(n_read, file_size);
+ close(fd);
+
+ const char* expected =
+ "a different string\n"
+ "bar and with an addition\n"
+ "baz\n"
+ "100\n"
+ "0.000000000\n"
+ "16.5\n"
+ "-16.5\n"
+ "2.0\n"
+ "0xdeadbeef\n"
+ "true\n"
+ "[(0 : 1), (5 : 2), (6 : 1), (10 : 2)]\n"
+ "[(14 : 1), (15 : 2), (16 : 2)]\n"
+ "[(ASSUME : 2), (SCOPE : 1)]\n"
+ "<unsupported>";
+ ASSERT_EQ(strncmp(expected, buf, file_size), 0);
+ delete[] buf;
+
+ int ret = remove(tmp_filename);
+ ASSERT_EQ(ret, 0);
+#endif
+}
+} // namespace test
+} // namespace CVC4
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
deleted file mode 100644
index 370b1d65d..000000000
--- a/test/unit/util/stats_black.h
+++ /dev/null
@@ -1,196 +0,0 @@
-/********************* */
-/*! \file stats_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andres Noetzli, Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Black box testing of CVC4::Stat and associated classes
- **
- ** Black box testing of CVC4::Stat and associated classes.
- **/
-
-#include <cxxtest/TestSuite.h>
-#include <fcntl.h>
-#include <ctime>
-#include <sstream>
-#include <string>
-
-#include "lib/clock_gettime.h"
-#include "expr/proof_rule.h"
-#include "util/statistics_registry.h"
-
-using namespace CVC4;
-using namespace std;
-
-/**
- * This is a duplicate of operator== in statistics_registry.h.
- * This is duplicated here to try to avoid polluting top namepsace.
- *
- * If operator== is in the CVC4 namespace, there are some circumstances
- * where clang does not find this operator.
- */
-bool operator==(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
-}
-
-class StatsBlack : public CxxTest::TestSuite {
-public:
-
- void testStats() {
-#ifdef CVC4_STATISTICS_ON
- // StatisticsRegistry
- //static void flushStatistics(std::ostream& out);
-
- // static inline void registerStat(Stat* s);
- // static inline void unregisterStat(Stat* s);
-
- string empty, bar = "bar", baz = "baz";
- ReferenceStat<string> refStr("stat #1", empty);
- ReferenceStat<string> refStr2("refStr2", bar);
- // setData
- // getData
-
- // flushInformation
- // flushStat
-
- BackedStat<string> backedStr("backed", baz);
- // setData
- // getData
- // operator=
-
- BackedStat<double> backedDouble("backedDouble", 16.5);
- BackedStat<double> backedNegDouble("backedNegDouble", -16.5);
- BackedStat<double> backedDoubleNoDec("backedDoubleNoDec", 2.0);
- BackedStat<bool> backedBool("backedBool", true);
- BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF);
- HistogramStat<int64_t> histStat("hist");
- histStat << 5;
- histStat << 6;
- histStat << 5;
- histStat << 10;
- histStat << 10;
- histStat << 0;
- IntegralHistogramStat<std::int64_t> histIntStat("hist-int");
- histIntStat << 15 << 16 << 15 << 14 << 16;
- IntegralHistogramStat<CVC4::PfRule> histPfRuleStat("hist-pfrule");
- histPfRuleStat << PfRule::ASSUME << PfRule::SCOPE << PfRule::ASSUME;
-
- // A statistic with no safe_print support
- BackedStat<string*> backedUnsupported("backedUnsupported", &bar);
-
- IntStat sInt("my int", 10);
- TimerStat sTimer("a timer ! for measuring time");
-
- TS_ASSERT_EQUALS(refStr.getName(), "stat #1");
- TS_ASSERT_EQUALS(refStr2.getName(), "refStr2");
- TS_ASSERT_EQUALS(backedStr.getName(), "backed");
- TS_ASSERT_EQUALS(sInt.getName(), "my int");
- TS_ASSERT_EQUALS(sTimer.getName(), "a timer ! for measuring time");
- TS_ASSERT_EQUALS(histIntStat.getName(), "hist-int");
- TS_ASSERT_EQUALS(histPfRuleStat.getName(), "hist-pfrule");
-
- TS_ASSERT_EQUALS(refStr.getData(), empty);
- TS_ASSERT_EQUALS(refStr2.getData(), bar);
- empty = "a different string";
- bar += " and with an addition";
- TS_ASSERT_EQUALS(refStr.getData(), empty);
- TS_ASSERT_EQUALS(refStr2.getData(), bar);
-
- TS_ASSERT_EQUALS(backedStr.getData(), "baz");
- baz = "something else";
- TS_ASSERT_EQUALS(backedStr.getData(), "baz");
-
- TS_ASSERT_EQUALS(sInt.getData(), 10);
- sInt.setData(100);
- TS_ASSERT_EQUALS(sInt.getData(), 100);
-
- TS_ASSERT_EQUALS(sTimer.getData(), timespec());
-
- stringstream sstr;
-
- refStr.flushInformation(sstr);
- TS_ASSERT_EQUALS(sstr.str(), empty);
- sstr.str("");
- refStr2.flushInformation(sstr);
- TS_ASSERT_EQUALS(sstr.str(), bar);
- sstr.str("");
- backedStr.flushInformation(sstr);
- TS_ASSERT_EQUALS(sstr.str(), "baz");
- sstr.str("");
- sInt.flushInformation(sstr);
- TS_ASSERT_EQUALS(sstr.str(), "100");
- sstr.str("");
- sTimer.flushInformation(sstr);
- TS_ASSERT_EQUALS(sstr.str(), "0.000000000");
-
- // Test safeFlushInformation (and safe_print functions)
- char tmp_filename[] = "testXXXXXX";
- int fd = mkstemp(tmp_filename);
- TS_ASSERT_DIFFERS(fd, -1);
- refStr.safeFlushInformation(fd);
- safe_print(fd, "\n");
- refStr2.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedStr.safeFlushInformation(fd);
- safe_print(fd, "\n");
- sInt.safeFlushInformation(fd);
- safe_print(fd, "\n");
- sTimer.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedDouble.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedNegDouble.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedDoubleNoDec.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedAddr.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedBool.safeFlushInformation(fd);
- safe_print(fd, "\n");
- histStat.safeFlushInformation(fd);
- safe_print(fd, "\n");
- histIntStat.safeFlushInformation(fd);
- safe_print(fd, "\n");
- histPfRuleStat.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedUnsupported.safeFlushInformation(fd);
- off_t file_size = lseek(fd, 0, SEEK_CUR);
- close(fd);
-
- char* buf = new char[file_size];
- fd = open(tmp_filename, O_RDONLY);
- TS_ASSERT_DIFFERS(fd, -1);
- ssize_t n_read = pread(fd, buf, file_size, 0);
- TS_ASSERT_EQUALS(n_read, file_size);
- close(fd);
-
- const char* expected =
- "a different string\n"
- "bar and with an addition\n"
- "baz\n"
- "100\n"
- "0.000000000\n"
- "16.5\n"
- "-16.5\n"
- "2.0\n"
- "0xdeadbeef\n"
- "true\n"
- "[(0 : 1), (5 : 2), (6 : 1), (10 : 2)]\n"
- "[(14 : 1), (15 : 2), (16 : 2)]\n"
- "[(ASSUME : 2), (SCOPE : 1)]\n"
- "<unsupported>";
- TS_ASSERT(strncmp(expected, buf, file_size) == 0);
- delete[] buf;
-
- int ret = remove(tmp_filename);
- TS_ASSERT_EQUALS(ret, 0);
-#endif /* CVC4_STATISTICS_ON */
- }
-
-};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback