-
Notifications
You must be signed in to change notification settings - Fork 1
/
statistics.html
182 lines (160 loc) · 11.5 KB
/
statistics.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
<!DOCTYPE html>
<html class="writer-html5" lang="en">
<head>
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />
<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-ML12X2V35B"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag(){dataLayer.push(arguments);}
gtag('js', new Date());
gtag('config', 'G-ML12X2V35B');
</script>
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Statistics — cvc5 documentation</title>
<link rel="stylesheet" type="text/css" href="static/pygments.css?v=80d5e7a1" />
<link rel="stylesheet" type="text/css" href="static/css/theme.css?v=e59714d7" />
<link rel="stylesheet" type="text/css" href="static/custom.css?v=b9602cbe" />
<script src="static/jquery.js?v=5d32c60e"></script>
<script src="static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
<script data-url_root="./" id="documentation_options" src="static/documentation_options.js?v=b3ba4146"></script>
<script src="static/doctools.js?v=888ff710"></script>
<script src="static/sphinx_highlight.js?v=4825356b"></script>
<script src="static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="next" title="Examples" href="examples/examples.html" />
<link rel="prev" title="Skolem Identifiers" href="skolem-ids.html" />
</head>
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="index.html" class="icon icon-home">
cvc5
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="installation/installation.html">Installation</a></li>
<li class="toctree-l1"><a class="reference internal" href="binary/binary.html">Binary Documentation</a></li>
<li class="toctree-l1"><a class="reference internal" href="api/api.html">API Documentation</a></li>
<li class="toctree-l1"><a class="reference internal" href="options.html">Options</a></li>
<li class="toctree-l1"><a class="reference internal" href="output-tags.html">Output tags</a></li>
<li class="toctree-l1"><a class="reference internal" href="proofs/proofs.html">Proof Production</a></li>
<li class="toctree-l1"><a class="reference internal" href="resource-limits.html">Resource limits</a></li>
<li class="toctree-l1"><a class="reference internal" href="skolem-ids.html">Skolem Identifiers</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">Statistics</a></li>
<li class="toctree-l1"><a class="reference internal" href="examples/examples.html">Examples</a></li>
<li class="toctree-l1"><a class="reference internal" href="theories/theories.html">Theory References</a></li>
<li class="toctree-l1"><a class="reference internal" href="references.html">References</a></li>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="index.html">cvc5</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
<li class="breadcrumb-item active">Statistics</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<section id="statistics">
<h1>Statistics<a class="headerlink" href="#statistics" title="Permalink to this heading"></a></h1>
<p>cvc5 collects a wide variety of statistics that give some insight on how it solves a particular input.
The statistics can be inspected via the <a class="reference internal" href="api/cpp/classes/solver.html#_CPPv4NK4cvc56Solver13getStatisticsEv" title="cvc5::Solver::getStatistics"><code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">Solver::getStatistics()</span></code></a> API
function, or printed using the following options:</p>
<ul class="simple">
<li><p><a class="reference internal" href="options.html#lbl-option-stats"><span class="std std-ref">stats</span></a> prints public statistics with non-default values</p></li>
<li><p><a class="reference internal" href="options.html#lbl-option-stats-all"><span class="std std-ref">stats-all</span></a> also prints statistics with default values</p></li>
<li><p><a class="reference internal" href="options.html#lbl-option-stats-internal"><span class="std std-ref">stats-internal</span></a> also prints internal statistics</p></li>
<li><p><a class="reference internal" href="options.html#lbl-option-stats-every-query"><span class="std std-ref">stats-every-query</span></a> prints statistics after every (incremental) check</p></li>
</ul>
<p>Statistics collection is only available if the <code class="docutils literal notranslate"><span class="pre">ENABLE_STATISTICS</span></code> cmake option
is set to true, which is the case for all but competition builds.
Statistics, obtained via <a class="reference internal" href="api/cpp/classes/solver.html#_CPPv4NK4cvc56Solver13getStatisticsEv" title="cvc5::Solver::getStatistics"><code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">Solver::getStatistics()</span></code></a>,
are always a snapshot of the statistics values that is decoupled from the
solver object and will not change when the solver is used again or deallocated.
Individual statistics values can be obtained via the API either by iterating over the
<a class="reference internal" href="api/cpp/classes/statistics.html#_CPPv4N4cvc510StatisticsE" title="cvc5::Statistics"><code class="xref cpp cpp-class docutils literal notranslate"><span class="pre">Statistics</span></code></a> object or by querying it by name.</p>
<p>A statistic value (of type <a class="reference internal" href="api/cpp/classes/statistics.html#_CPPv4N4cvc54StatE" title="cvc5::Stat"><code class="xref cpp cpp-class docutils literal notranslate"><span class="pre">Stat</span></code></a>) has two general
properties, <a class="reference internal" href="api/cpp/classes/statistics.html#_CPPv4NK4cvc54Stat10isInternalEv" title="cvc5::Stat::isInternal"><code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">isInternal()</span></code></a> and
<a class="reference internal" href="api/cpp/classes/statistics.html#_CPPv4NK4cvc54Stat9isDefaultEv" title="cvc5::Stat::isDefault"><code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">isDefault()</span></code></a>.
<a class="reference internal" href="api/cpp/classes/statistics.html#_CPPv4NK4cvc54Stat10isInternalEv" title="cvc5::Stat::isInternal"><code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">isInternal()</span></code></a> indicates whether a
statistic is considered public or internal. Public statistics are considered to
be part of the public API and should therefore remain stable across different
minor versions of cvc5. There is no such guarantee for internal statistics.
<a class="reference internal" href="api/cpp/classes/statistics.html#_CPPv4NK4cvc54Stat9isDefaultEv" title="cvc5::Stat::isDefault"><code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">isDefault()</span></code></a> checks whether the
current value of a statistics is still the default value, or whether its value
was changed.</p>
<p>A statistic value can be any of the following types:</p>
<ul class="simple">
<li><p>integer, more specifically a signed 64-bit integer (<code class="docutils literal notranslate"><span class="pre">int64_t</span></code> in C++).</p></li>
<li><p>double, a 64-bit floating-point value (<code class="docutils literal notranslate"><span class="pre">double</span></code> in C++).</p></li>
<li><p>string, a character sequence (<code class="docutils literal notranslate"><span class="pre">std::string</span></code> in C++). Timer statistics are
exported as string values as well, given as <code class="docutils literal notranslate"><span class="pre">"<value>ms"</span></code>.</p></li>
<li><p>histogram, a mapping from some integral or enumeration type to their count.
The integral or enumeration types are exported as string representations
(<code class="docutils literal notranslate"><span class="pre">std::map<std::string,</span> <span class="pre">uint64_t></span></code> in C++).</p></li>
</ul>
<p>Printing statistics on the command line looks like this:</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>$ bin/cvc5 --stats ../test/regress/cli/regress0/auflia/bug336.smt2
unsat
driver::filename = ../test/regress/cli/regress0/auflia/bug336.smt2
global::totalTime = 3ms
theory::arith::inferencesLemma = { ARITH_SPLIT_DEQ: 1 }
theory::arrays::inferencesFact = { ARRAYS_READ_OVER_WRITE_1: 2 }
theory::arrays::inferencesLemma = { ARRAYS_EXT: 1, ARRAYS_READ_OVER_WRITE: 3 }
theory::builtin::inferencesLemma = { COMBINATION_SPLIT: 1 }
cvc5::CONSTANT = { UNKNOWN_TYPE_CONSTANT: 4, integer type: 4 }
cvc5::TERM = { AND: 1, APPLY_UF: 4, EQUAL: 4, NOT: 2, STORE: 2 }
cvc5::VARIABLE = { Boolean type: 5 }
</pre></div>
</div>
<p>Public statistics include some general information about the input file
(<code class="docutils literal notranslate"><span class="pre">driver::filename</span></code> and <code class="docutils literal notranslate"><span class="pre">*</span></code>), the overall runtime (<code class="docutils literal notranslate"><span class="pre">global::totalTime</span></code>)
and the lemmas each theory sent to the core solver (<code class="docutils literal notranslate"><span class="pre">theory::*</span></code>).</p>
</section>
</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="skolem-ids.html" class="btn btn-neutral float-left" title="Skolem Identifiers" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="examples/examples.html" class="btn btn-neutral float-right" title="Examples" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>
<hr/>
<div role="contentinfo">
<p>© Copyright 2024, the authors of cvc5.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</body>
</html>