-
Notifications
You must be signed in to change notification settings - Fork 8
/
index.html
187 lines (166 loc) · 11.1 KB
/
index.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
183
184
185
186
187
<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<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>Satisfiability Modulo Theories: A Beginner’s Tutorial — Satisfiability Modulo Theories: A Beginner's Tutorial 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=19f00094" />
<link rel="stylesheet" type="text/css" href="static/copybutton.css?v=76b2166b" />
<link rel="stylesheet" type="text/css" href="static/tabs.css?v=a5c4661c" />
<link rel="stylesheet" type="text/css" href="static/custom.css?v=b9602cbe" />
<!--[if lt IE 9]>
<script src="static/js/html5shiv.min.js"></script>
<![endif]-->
<script src="static/jquery.js?v=5d32c60e"></script>
<script src="static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
<script src="static/documentation_options.js?v=5929fcd5"></script>
<script src="static/doctools.js?v=9a2dae69"></script>
<script src="static/sphinx_highlight.js?v=dc90522c"></script>
<script src="static/clipboard.min.js?v=a7894cd8"></script>
<script src="static/copybutton.js?v=f281be69"></script>
<script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></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="Introduction" href="introduction.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="#" class="icon icon-home">
Satisfiability Modulo Theories: A Beginner's Tutorial
</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>
<li class="toctree-l1"><a class="reference internal" href="introduction.html">Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="overview.html">Overview</a></li>
<li class="toctree-l1"><a class="reference internal" href="formal.html">Formal Foundations</a></li>
<li class="toctree-l1"><a class="reference internal" href="theories.html">SMT Theories</a></li>
<li class="toctree-l1"><a class="reference internal" href="outputs.html">SMT Solver Outputs</a></li>
<li class="toctree-l1"><a class="reference internal" href="conclusion.html">Conclusion</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="solutions.html">Solutions to Exercises</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="#">Satisfiability Modulo Theories: A Beginner's Tutorial</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="#" class="icon icon-home" aria-label="Home"></a></li>
<li class="breadcrumb-item active">Satisfiability Modulo Theories: A Beginner’s Tutorial</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="satisfiability-modulo-theories-a-beginner-s-tutorial">
<h1>Satisfiability Modulo Theories: A Beginner’s Tutorial<a class="headerlink" href="#satisfiability-modulo-theories-a-beginner-s-tutorial" title="Link to this heading"></a></h1>
<p>Great minds have long dreamed of creating machines that can function as
general-purpose problem solvers. Satisfiability modulo theories (SMT) has
emerged as one pragmatic realization of this dream, providing significant
expressive power and automation. This tutorial is a beginner’s guide to SMT. It
includes an overview of SMT and its formal foundations, a catalog of the main
theories used in SMT solvers, and illustrations of how to obtain models and
proofs. Throughout the tutorial, examples and exercises are provided as
hands-on activities for the reader. They can be run using either Python or the
SMT-LIB language, using either the cvc5 or the z3 SMT solver.</p>
<div class="toctree-wrapper compound">
<ul>
<li class="toctree-l1"><a class="reference internal" href="introduction.html">Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="overview.html">Overview</a></li>
<li class="toctree-l1"><a class="reference internal" href="formal.html">Formal Foundations</a><ul>
<li class="toctree-l2"><a class="reference internal" href="formal.html#syntax">Syntax</a></li>
<li class="toctree-l2"><a class="reference internal" href="formal.html#semantics">Semantics</a></li>
<li class="toctree-l2"><a class="reference internal" href="formal.html#theories">Theories</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="theories.html">SMT Theories</a><ul>
<li class="toctree-l2"><a class="reference internal" href="theories.html#core-theory-and-uninterpreted-symbols">Core Theory and Uninterpreted Symbols</a></li>
<li class="toctree-l2"><a class="reference internal" href="theories.html#arithmetic">Arithmetic</a></li>
<li class="toctree-l2"><a class="reference internal" href="theories.html#arrays">Arrays</a></li>
<li class="toctree-l2"><a class="reference internal" href="theories.html#bit-vectors">Bit-vectors</a></li>
<li class="toctree-l2"><a class="reference internal" href="theories.html#datatypes">Datatypes</a></li>
<li class="toctree-l2"><a class="reference internal" href="theories.html#floating-point-arithmetic">Floating-Point Arithmetic</a></li>
<li class="toctree-l2"><a class="reference internal" href="theories.html#strings">Strings</a></li>
<li class="toctree-l2"><a class="reference internal" href="theories.html#quantifiers">Quantifiers</a></li>
<li class="toctree-l2"><a class="reference internal" href="theories.html#non-standard-theories">Non-standard Theories</a></li>
<li class="toctree-l2"><a class="reference internal" href="theories.html#combinations-of-theories">Combinations of Theories</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="outputs.html">SMT Solver Outputs</a><ul>
<li class="toctree-l2"><a class="reference internal" href="outputs.html#satisfiable-queries">Satisfiable Queries</a></li>
<li class="toctree-l2"><a class="reference internal" href="outputs.html#unsatisfiable-queries">Unsatisfiable Queries</a></li>
<li class="toctree-l2"><a class="reference internal" href="outputs.html#unknown-queries">Unknown Queries</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="conclusion.html">Conclusion</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="solutions.html">Solutions to Exercises</a><ul>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-1">Solution to <span class="xref std std-ref">Exercise 1</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-2">Solution to <span class="xref std std-ref">Exercise 2</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-3">Solution to <span class="xref std std-ref">Exercise 3</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-4">Solution to <span class="xref std std-ref">Exercise 4</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-5">Solution to <span class="xref std std-ref">Exercise 5</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-6">Solution to <span class="xref std std-ref">Exercise 6</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-7">Solution to <span class="xref std std-ref">Exercise 7</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-8">Solution to <span class="xref std std-ref">Exercise 8</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-9">Solution to <span class="xref std std-ref">Exercise 9</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-10">Solution to <span class="xref std std-ref">Exercise 10</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-11">Solution to <span class="xref std std-ref">Exercise 11</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-12">Solution to <span class="xref std std-ref">Exercise 12</span></a></li>
<li class="toctree-l2"><a class="reference internal" href="solutions.html#solution-to-exercise-13">Solution to <span class="xref std std-ref">Exercise 13</span></a></li>
</ul>
</li>
</ul>
</div>
</section>
</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="introduction.html" class="btn btn-neutral float-right" title="Introduction" 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, Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar.</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>