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                 :            :  * Finite fields statistics
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/ff/stats.h"
      14                 :            : 
      15                 :            : #include "base/output.h"
      16                 :            : #include "util/statistics_registry.h"
      17                 :            : 
      18                 :            : namespace cvc5::internal {
      19                 :            : namespace theory {
      20                 :            : namespace ff {
      21                 :            : 
      22                 :      51241 : FfStatistics::FfStatistics(StatisticsRegistry& reg, const std::string& prefix)
      23                 :      51241 :     : d_numGbRuns(reg.registerInt(prefix + "num_gb_runs")),
      24                 :      51241 :       d_timeGbRuns(reg.registerTimer(prefix + "time_gb_runs")),
      25                 :      51241 :       d_numTrivialUnsat(reg.registerInt(prefix + "num_trivial_unsat")),
      26                 :            :       d_modelConstructionTime(
      27                 :      51241 :           reg.registerTimer(prefix + "model_construction_time")),
      28                 :            :       d_numConstructionErrors(
      29                 :      51241 :           reg.registerInt(prefix + "num_construction_errors")),
      30                 :      51241 :       d_idealMinPoly(reg.registerInt(prefix + "num_ideal_min_poly")),
      31                 :      51241 :       d_idealPosDim(reg.registerInt(prefix + "num_ideal_pos_dim"))
      32                 :            : {
      33         [ +  - ]:      51241 :   Trace("ff::stats") << "ff registered stats" << std::endl;
      34                 :      51241 : }
      35                 :            : 
      36                 :            : }  // namespace ff
      37                 :            : }  // namespace theory
      38                 :            : }  // namespace cvc5::internal