Branch data     Line data    Source code

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