GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/smt_engine_stats.cpp Lines: 28 28 100.0 %
Date: 2021-03-22 Branches: 46 92 50.0 %

Line Exec Source
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-2021 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
9619
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
9619
      d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
34
{
35
9619
  smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
36
9619
  smtStatisticsRegistry()->registerStat(&d_numConstantProps);
37
9619
  smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
38
9619
  smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
39
9619
  smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
40
9619
  smtStatisticsRegistry()->registerStat(&d_checkModelTime);
41
9619
  smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
42
9619
  smtStatisticsRegistry()->registerStat(&d_solveTime);
43
9619
  smtStatisticsRegistry()->registerStat(&d_pushPopTime);
44
9619
  smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
45
9619
  smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
46
9619
}
47
48
19196
SmtEngineStatistics::~SmtEngineStatistics()
49
{
50
9598
  smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
51
9598
  smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
52
9598
  smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
53
9598
  smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
54
9598
  smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
55
9598
  smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
56
9598
  smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
57
9598
  smtStatisticsRegistry()->unregisterStat(&d_solveTime);
58
9598
  smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
59
9598
  smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
60
9598
  smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
61
9598
}
62
63
}  // namespace smt
64
26676
}  // namespace CVC4