GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/smt_engine_stats.cpp Lines: 34 34 100.0 %
Date: 2021-03-23 Branches: 60 120 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
9621
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
      d_driverFilename("driver::filename", ""),
35
      d_driverResult("driver::sat/unsat", ""),
36
9621
      d_driverTotalTime("driver::totalTime", 0.0)
37
{
38
9621
  smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
39
9621
  smtStatisticsRegistry()->registerStat(&d_numConstantProps);
40
9621
  smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
41
9621
  smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
42
9621
  smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
43
9621
  smtStatisticsRegistry()->registerStat(&d_checkModelTime);
44
9621
  smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
45
9621
  smtStatisticsRegistry()->registerStat(&d_solveTime);
46
9621
  smtStatisticsRegistry()->registerStat(&d_pushPopTime);
47
9621
  smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
48
9621
  smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
49
9621
  smtStatisticsRegistry()->registerStat(&d_driverFilename);
50
9621
  smtStatisticsRegistry()->registerStat(&d_driverResult);
51
9621
  smtStatisticsRegistry()->registerStat(&d_driverTotalTime);
52
9621
}
53
54
19200
SmtEngineStatistics::~SmtEngineStatistics()
55
{
56
9600
  smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
57
9600
  smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
58
9600
  smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
59
9600
  smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
60
9600
  smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
61
9600
  smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
62
9600
  smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
63
9600
  smtStatisticsRegistry()->unregisterStat(&d_solveTime);
64
9600
  smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
65
9600
  smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
66
9600
  smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
67
9600
  smtStatisticsRegistry()->unregisterStat(&d_driverFilename);
68
9600
  smtStatisticsRegistry()->unregisterStat(&d_driverResult);
69
9600
  smtStatisticsRegistry()->unregisterStat(&d_driverTotalTime);
70
9600
}
71
72
}  // namespace smt
73
26685
}  // namespace CVC4