Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Gereon Kremer, Aina Niemetz, Hans-Joerg Schurr
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Black box testing of cvc5::Stat and associated classes.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include <fcntl.h>
      17                 :            : 
      18                 :            : #include <ctime>
      19                 :            : #include <sstream>
      20                 :            : #include <string>
      21                 :            : #include <thread>
      22                 :            : 
      23                 :            : #include "lib/clock_gettime.h"
      24                 :            : #include "cvc5/cvc5_proof_rule.h"
      25                 :            : #include "test_env.h"
      26                 :            : #include "util/statistics_registry.h"
      27                 :            : #include "util/statistics_stats.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : 
      31                 :         10 : std::ostream& operator<<(std::ostream& os, const StatisticBaseValue* sbv)
      32                 :            : {
      33                 :         10 :   return os << *sbv;
      34                 :            : }
      35                 :         10 : bool operator==(const StatisticBaseValue* sbv, const std::string& s)
      36                 :            : {
      37                 :         10 :   std::stringstream ss;
      38                 :         10 :   ss << sbv;
      39                 :         20 :   return ss.str() == s;
      40                 :            : }
      41                 :            : 
      42                 :            : namespace test {
      43                 :            : 
      44                 :            : class TestUtilBlackStats : public TestEnv
      45                 :            : {
      46                 :            : };
      47                 :            : 
      48                 :          2 : TEST_F(TestUtilBlackStats, stats)
      49                 :            : {
      50                 :            : #ifdef CVC5_STATISTICS_ON
      51                 :          1 :   StatisticsRegistry reg(false, false, false);
      52                 :          2 :   std::string empty, bar = "bar", baz = "baz";
      53                 :            : 
      54                 :          1 :   AverageStat avg = reg.registerAverage("avg");
      55                 :          1 :   avg << 1.0 << 2.0;
      56                 :            : 
      57                 :          1 :   HistogramStat<int64_t> histInt = reg.registerHistogram<int64_t>("hist-int");
      58                 :          1 :   histInt << 15 << 16 << 15 << 14 << 16;
      59                 :            : 
      60                 :            :   HistogramStat<ProofRule> histProofRule =
      61                 :          1 :       reg.registerHistogram<ProofRule>("hist-pfrule");
      62                 :          1 :   histProofRule << ProofRule::ASSUME << ProofRule::SCOPE << ProofRule::ASSUME;
      63                 :            : 
      64                 :          1 :   IntStat intstat = reg.registerInt("int");
      65                 :          1 :   intstat = 5;
      66                 :          1 :   intstat++;
      67                 :            : 
      68                 :            :   ReferenceStat<std::string> refStr =
      69                 :          2 :       reg.registerReference<std::string>("strref1", empty);
      70                 :            :   ReferenceStat<std::string> refStr2 =
      71                 :          2 :       reg.registerReference<std::string>("strref2", bar);
      72                 :            : 
      73                 :          1 :   TimerStat timer = reg.registerTimer("timer");
      74                 :            :   {
      75                 :          1 :     CodeTimer ct(timer);
      76                 :          1 :     std::this_thread::sleep_for(std::chrono::milliseconds(50));
      77                 :            :   }
      78                 :            : 
      79                 :          1 :   ValueStat<std::string> valStr = reg.registerValue("backed", baz);
      80                 :          1 :   valStr.set("barz");
      81                 :          1 :   ValueStat<double> valD1 = reg.registerValue("backedDouble", 16.5);
      82                 :          1 :   valD1.set(3.5);
      83                 :          1 :   ValueStat<double> valD2 = reg.registerValue("backedNegDouble", -16.5);
      84                 :          1 :   valD2.set(-3.5);
      85                 :          1 :   ValueStat<double> valD3 = reg.registerValue("backedDoubleNoDec", 2.0);
      86                 :          1 :   valD3.set(17);
      87                 :            : 
      88         [ -  + ]:          1 :   ASSERT_EQ(reg.get("avg"), std::string("1.5"));
      89         [ -  + ]:          1 :   ASSERT_EQ(reg.get("hist-int"), std::string("{ 14: 1, 15: 2, 16: 2 }"));
      90         [ -  + ]:          1 :   ASSERT_EQ(reg.get("hist-pfrule"), std::string("{ ASSUME: 2, SCOPE: 1 }"));
      91         [ -  + ]:          1 :   ASSERT_EQ(reg.get("int"), std::string("6"));
      92         [ -  + ]:          1 :   ASSERT_EQ(reg.get("strref1"), std::string(""));
      93         [ -  + ]:          1 :   ASSERT_EQ(reg.get("strref2"), std::string("bar"));
      94         [ -  + ]:          1 :   ASSERT_EQ(reg.get("backed"), std::string("barz"));
      95         [ -  + ]:          1 :   ASSERT_EQ(reg.get("backedDouble"), std::string("3.5"));
      96         [ -  + ]:          1 :   ASSERT_EQ(reg.get("backedNegDouble"), std::string("-3.5"));
      97         [ -  + ]:          1 :   ASSERT_EQ(reg.get("backedDoubleNoDec"), std::string("17"));
      98                 :            : #endif
      99                 :            : }
     100                 :            : }  // namespace test
     101                 :            : }  // namespace cvc5::internal