-
Notifications
You must be signed in to change notification settings - Fork 1
/
resource-limits.html
160 lines (138 loc) · 11.7 KB
/
resource-limits.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
<!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>Resource limits — 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="Skolem Identifiers" href="skolem-ids.html" />
<link rel="prev" title="Proof format: DOT" href="proofs/output_dot.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 current"><a class="current reference internal" href="#">Resource limits</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#overall-time-limit-tlimit-option">Overall time limit (<span class="xref std std-ref">tlimit</span> option)</a></li>
<li class="toctree-l2"><a class="reference internal" href="#resource-manager-and-resource-spending">Resource manager and resource spending</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="skolem-ids.html">Skolem Identifiers</a></li>
<li class="toctree-l1"><a class="reference internal" href="statistics.html">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">Resource limits</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="resource-limits">
<h1>Resource limits<a class="headerlink" href="#resource-limits" title="Permalink to this heading"></a></h1>
<p>cvc5 supports limiting the time or <em>resources</em> it uses during solving via the options
<a class="reference internal" href="options.html#lbl-option-tlimit"><span class="std std-ref">tlimit</span></a>, <a class="reference internal" href="options.html#lbl-option-tlimit-per"><span class="std std-ref">tlimit-per</span></a>,
<a class="reference internal" href="options.html#lbl-option-rlimit"><span class="std std-ref">rlimit</span></a>, and <a class="reference internal" href="options.html#lbl-option-rlimit-per"><span class="std std-ref">rlimit-per</span></a>.
All these options take a single non-negative number as an argument where giving zero explicitly disables the respective limit. For time limits the number is interpreted as the number of milliseconds, and for resource limits it indicates the amount of <em>resources</em>.</p>
<p>The limits configured using <a class="reference internal" href="options.html#lbl-option-tlimit"><span class="std std-ref">tlimit</span></a> and <a class="reference internal" href="options.html#lbl-option-rlimit"><span class="std std-ref">rlimit</span></a> restrict time and resource usage over the whole lifetime of the <a class="reference internal" href="api/cpp/classes/solver.html#_CPPv4N4cvc56SolverE" title="cvc5::Solver"><code class="xref cpp cpp-class docutils literal notranslate"><span class="pre">solver</span></code></a> object, respectively.
In contrast to that, <a class="reference internal" href="options.html#lbl-option-tlimit-per"><span class="std std-ref">tlimit-per</span></a> and <a class="reference internal" href="options.html#lbl-option-rlimit-per"><span class="std std-ref">rlimit-per</span></a> apply to every check individually (<a class="reference internal" href="api/cpp/classes/solver.html#_CPPv4NK4cvc56Solver8checkSatEv" title="cvc5::Solver::checkSat"><code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">checkSat</span></code></a>, <a class="reference internal" href="api/cpp/classes/solver.html#_CPPv4NK4cvc56Solver16checkSatAssumingERK4Term" title="cvc5::Solver::checkSatAssuming"><code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">checkSatAssuming</span></code></a>, etc).</p>
<p>Except for the overall time limit (see below), the limits are checked by cvc5 itself. This means that the solver remains in a safe state after a limit has been reached.
Due to the way cvc5 checks these limits (see below), cvc5 may not precisely honor per-call time limits: if a subroutine requires a long time to finish without spending resources itself, cvc5 only realizes afterwards that the timeout has (long) passed.</p>
<section id="overall-time-limit-tlimit-option">
<h2>Overall time limit (<a class="reference internal" href="options.html#lbl-option-tlimit"><span class="std std-ref">tlimit</span></a> option)<a class="headerlink" href="#overall-time-limit-tlimit-option" title="Permalink to this heading"></a></h2>
<p>The <a class="reference internal" href="options.html#lbl-option-tlimit"><span class="std std-ref">tlimit</span></a> option limits the overall running time of the cvc5 solver binary.
It is implemented using an asynchronous interrupt that is usually managed by the operating system (using <code class="docutils literal notranslate"><span class="pre">setitimer</span></code>).
When this interrupt occurs, cvc5 outputs a corresponding message, prints the current statistics and immediately terminates its process. The same is done when an external resource limiting mechanism is in place, for example <code class="docutils literal notranslate"><span class="pre">ulimit</span></code>.</p>
<p>This mechanism is inherently unsuited when cvc5 is used within another application process via one of its APIs: therefore, it is only honored when running as a standalone binary.
Setting <a class="reference internal" href="options.html#lbl-option-tlimit"><span class="std std-ref">tlimit</span></a> via the API or the <code class="docutils literal notranslate"><span class="pre">(set-option)</span></code> SMT-LIB command has thus no effect.</p>
</section>
<section id="resource-manager-and-resource-spending">
<h2>Resource manager and resource spending<a class="headerlink" href="#resource-manager-and-resource-spending" title="Permalink to this heading"></a></h2>
<p>All other limits are enforced centrally by the resource manager as follows.
Whenever certain parts of the solver execute, they instruct the resource manager to <em>spend</em> a resource.
As soon as the resource manager realizes that some limit is exhausted (either the resource limit or the per-check time limit is reached), it asynchronously instructs the core solver to interrupt the check.
To not invalidate the internal state of the solver, and allow to use it again after an interrupt, the solver continues its work until it reaches a safe point in one of the core solving components.
Then, it returns <cite>unknown</cite> (with an <a class="reference internal" href="api/cpp/enums/unknownexplanation.html#_CPPv4N4cvc518UnknownExplanationE" title="cvc5::UnknownExplanation"><code class="xref cpp cpp-enum docutils literal notranslate"><span class="pre">explanation</span></code></a>).</p>
<p>The intention of a resource limit is to be a deterministic measure that grows (linearly, if possible) with actual running time.
Resources are spent when lemmas are generated and during a few select events like preprocessing, rewriting, decisions and restarts in the SAT solver, or theory checks.
In case the resource spending does not properly reflect the running time, the weights of the individual resources can be modified using the <a class="reference internal" href="options.html#lbl-option-rweight"><span class="std std-ref">rweight</span></a> option, for example with <code class="docutils literal notranslate"><span class="pre">--rweight=RestartStep=5</span></code>.</p>
</section>
</section>
</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="proofs/output_dot.html" class="btn btn-neutral float-left" title="Proof format: DOT" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="skolem-ids.html" class="btn btn-neutral float-right" title="Skolem Identifiers" 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>