src/smt/smt_engine_stats.cpp

   1 /*********************                                                        */
   2 /*! \file smt_engine_stats.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Andrew Reynolds, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief Implementation of statistics for SMT engine
  13  **/
  14
  15 #include "smt/smt_engine_stats.h"
  16
  17 #include "smt/smt_statistics_registry.h"
  18
  19 namespace CVC4 {
  20 namespace smt {
  21
  22 SmtEngineStatistics::SmtEngineStatistics()
  23     : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
  24       d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
  25       d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
  26       d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
  27       d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
  28       d_checkModelTime("smt::SmtEngine::checkModelTime"),
  29       d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
  30       d_solveTime("smt::SmtEngine::solveTime"),
  31       d_pushPopTime("smt::SmtEngine::pushPopTime"),
  32       d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
  33       d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
  34 {
  35   smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
  36   smtStatisticsRegistry()->registerStat(&d_numConstantProps);
  37   smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
  38   smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
  39   smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
  40   smtStatisticsRegistry()->registerStat(&d_checkModelTime);
  41   smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
  42   smtStatisticsRegistry()->registerStat(&d_solveTime);
  43   smtStatisticsRegistry()->registerStat(&d_pushPopTime);
  44   smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
  45   smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
  46 }
  47
  48 SmtEngineStatistics::~SmtEngineStatistics()
  49 {
  50   smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
  51   smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
  52   smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
  53   smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
  54   smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
  55   smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
  56   smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
  57   smtStatisticsRegistry()->unregisterStat(&d_solveTime);
  58   smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
  59   smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
  60   smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
  61 }
  62
  63 }  // namespace smt
  64 }  // namespace CVC4