Skip to content

Commit

Permalink
[beginner's tutorial] Fix minor errors, add copy button for code, mak…
Browse files Browse the repository at this point in the history
…e logics link to SMT-LIB logic website, add first 4 solutions
  • Loading branch information
barrettcw committed Jul 18, 2024
1 parent 5790f8a commit 98998df
Show file tree
Hide file tree
Showing 25 changed files with 1,186 additions and 298 deletions.
2 changes: 1 addition & 1 deletion tutorials/beginners/.buildinfo
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Sphinx build info version 1
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
config: c216775dea20697632ffbcc17d79731f
config: 1e6a6a921061c558b28971484082c548
tags: 645f666f9bcd5a90fca523b33c5a78b7
2 changes: 2 additions & 0 deletions tutorials/beginners/_sources/index.rst.txt
Original file line number Diff line number Diff line change
Expand Up @@ -35,3 +35,5 @@ SMT-LIB language, using either the cvc5 or the z3 SMT solver.
* :ref:`genindex`
* :ref:`search`
.. TODO: Add analytics
7 changes: 3 additions & 4 deletions tutorials/beginners/_sources/introduction.rst.txt
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Hilbert in 1928, who called it the “Entscheidungsproblem” (decision problem)
[R24]_. In 1936, both Church and Turing showed that, in general, this is
impossible—the problem is undecidable [R13]_, [R42]_. Undeterred, researchers in
automated reasoning have searched for ways to solve either special cases of the
problem that are decid- able or to find heuristics that work well in
problem that are decidable or to find heuristics that work well in
practice. Satisfiability modulo theories (SMT) has emerged as an approach that
seems to fill a sweet spot in this search space. SMT leverages a rich
collection of decidable theories to provide considerable expressive power
Expand All @@ -25,8 +25,7 @@ problems are suitable for SMT solvers, describe the capabilities of modern
solvers, and provide guidance on how to encode problems as SMT queries.

Throughout the tutorial, we provide examples and exercises to illustrate the
concepts being explained. Unless otherwise stated, the exercises can be com-
pleted using either the |cvcv| [R3]_ or the |ziii| SMT solver [R32]_, through either
concepts being explained. Unless otherwise stated, the exercises can be completed using either the |cvcv| [R3]_ or the |ziii| SMT solver [R32]_, through either
their Python interface or their textual interface based on the SMT-LIB 2 format
[R8]_. The |cvcv| website at `cvc5.github.io <http://cvc5.github.io>`_ contains
documentation that can be used as a reference to supplement the material in
Expand All @@ -49,7 +48,7 @@ A. To use a Python API for SMT, first create a virtual environment.
python3 -m pip install z3-solver
|cvcv| is distributed under the BSD 3-clause license. Some features, however,
such as its finite field solver (see [finite-fields]_), are only available in an
such as its finite field solver (see :ref:`finite-fields`), are only available in an
extended version of |cvcv| distributed under the GNU General Public License
(GPL). [#]_
Since GPL is a problem for some users, the GPL version is not built
Expand Down
28 changes: 14 additions & 14 deletions tutorials/beginners/_sources/macros.rst.txt
Original file line number Diff line number Diff line change
Expand Up @@ -30,30 +30,30 @@

.. Logics
.. TODO: Add links to SMT-LIB logic files.
.. TODO: Some logics are missing from SMT-LIB website
.. |ALL| replace:: :smt:`ALL`
.. |QF| replace:: :smt:`QF`
.. |UF| replace:: :smt:`UF`
.. |QF_UF| replace:: :smt:`QF_UF`
.. |QF_IDL| replace:: :smt:`QF_IDL`
.. |QF_RDL| replace:: :smt:`QF_RDL`
.. |QF_LIA| replace:: :smt:`QF_LIA`
.. |QF_LRA| replace:: :smt:`QF_LRA`
.. |QF_UF| replace:: `QF_UF <https://smt-lib.org/logics-all.shtml#QF_UF>`__
.. |QF_IDL| replace:: `QF_IDL <https://smt-lib.org/logics-all.shtml#QF_IDL>`__
.. |QF_RDL| replace:: `QF_RDL <https://smt-lib.org/logics-all.shtml#QF_RDL>`__
.. |QF_LIA| replace:: `QF_LIA <https://smt-lib.org/logics-all.shtml#QF_LIA>`__
.. |QF_LRA| replace:: `QF_LRA <https://smt-lib.org/logics-all.shtml#QF_LRA>`__
.. |QF_LIRA| replace:: :smt:`QF_LIRA`
.. |QF_NIA| replace:: :smt:`QF_NIA`
.. |QF_NRA| replace:: :smt:`QF_NRA`
.. |QF_AX| replace:: :smt:`QF_AX`
.. |QF_ALIA| replace:: :smt:`QF_ALIA`
.. |QF_BV| replace:: :smt:`QF_BV`
.. |QF_NIA| replace:: `QF_NIA <https://smt-lib.org/logics-all.shtml#QF_NIA>`__
.. |QF_NRA| replace:: `QF_NRA <https://smt-lib.org/logics-all.shtml#QF_NRA>`__
.. |QF_AX| replace:: `QF_AX <https://smt-lib.org/logics-all.shtml#QF_AX>`__
.. |QF_ALIA| replace:: :smt:`QF_DT`
.. |QF_BV| replace:: `QF_BV <https://smt-lib.org/logics-all.shtml#QF_BV>`__
.. |QF_DT| replace:: :smt:`QF_DT`
.. |QF_DTLIA| replace:: :smt:`QF_DTLIA`
.. |QF_FP| replace:: :smt:`QF_FP`
.. |QF_S| replace:: :smt:`QF_S`
.. |QF_SLIA| replace:: :smt:`QF_SLIA`
.. |LIA| replace:: :smt:`LIA`
.. |LRA| replace:: :smt:`LRA`
.. |NRA| replace:: :smt:`NRA`
.. |LIA| replace:: `LIA <https://smt-lib.org/logics-all.shtml#LIA>`__
.. |LRA| replace:: `LRA <https://smt-lib.org/logics-all.shtml#LRA>`__
.. |NRA| replace:: `NRA <https://smt-lib.org/logics-all.shtml#NRA>`__
.. |QF_FF| replace:: :smt:`QF_FF`
.. |QF_FS| replace:: :smt:`QF_FS`

Expand Down
7 changes: 3 additions & 4 deletions tutorials/beginners/_sources/overview.rst.txt
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
.. TODO: Links in api-examples are broken
.. TODO: Add button to copy code in api-examples
.. include:: macros.rst

.. _overview:
Expand Down Expand Up @@ -125,7 +122,9 @@ is |X|. Constant |z| names the value we must multiply by 2 to get |x|. There is
solution because an even number does not have a multiplicative inverse in
machine arithmetic (i.e., when doing arithmetic modulo a power of 2).

_`Exercise 2`. Find the multiplicative inverse of 5 (mod :math:`2^8`).
.. _Exercise 2:

Exercise 2. Find the multiplicative inverse of 5 (mod :math:`2^8`).

:ref:`Solution to Exercise 2 <Solution to Exercise 2>`

Expand Down
136 changes: 107 additions & 29 deletions tutorials/beginners/_sources/solutions.rst.txt
Original file line number Diff line number Diff line change
@@ -1,94 +1,172 @@
.. include:: macros.rst

.. _solutions:

Solutions to Exercises
======================

.. _Solution to Exercise 1:

Solution to Exercise 1
^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 1 <Exercise 1>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
.. api-examples::
<solutions>/Exercise1.smt2
<solutions>/Exercise1.py

The output is as follows.

.. api-examples::
<solutions>/Exercise1.out.smt2
<solutions>/Exercise1.out.py

The SMT solver says |unsat| (or "no solution" for the Python version)
because there are no *integer* values that satisfy the constraints.

.. _Solution to Exercise 2:

Solution to Exercise 2
^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 2 <Exercise 2>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
.. api-examples::
<solutions>/Exercise2.smt2
<solutions>/Exercise2.py

The output is as follows.

.. api-examples::
<solutions>/Exercise2.out.smt2
<solutions>/Exercise2.out.py

The SMT solver gives a binary value of :smt:`x` as :smt:`#b11001101`. This
equals :python:`205` in decimal. And, indeed, :math:`5 \times 205 = 1025`, and
:math:`1025 \equiv 1\ \mathsf{mod}\ 256`.

.. _Solution to Exercise 3:

Solution to Exercise 3
^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 3 <Exercise 3>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
One way to modify :ref:`Example 4 <Example 4>` to make it satisfiable is to change the
hypothesis so that :smt:`f` is applied 2 and 4 times instead of 3 and 5 times.
In fact, any two number of applications that are not relatively prime will work.

.. api-examples::
<solutions>/Exercise3a.smt2
<solutions>/Exercise3a.py

The output from |cvcv| is as follows.

.. api-examples::
<solutions>/Exercise3a.out.smt2
<solutions>/Exercise3a.out.py

Notice that for the SMT-LIB example, |cvcv| uses a custom output format to describe how it has
interpreted the sort :smt:`U`: as a set with two elements, :smt:`@U_0` and
:smt:`@U_1`. Furthermore, |cvcv| uses the :smt:`define-fun` command to
describe the value assigned to :smt:`f`. In this case, the interpretation of
:smt:`f` maps :smt:`@U_1` to :smt:`@U_0` and everything else (i.e.,
:smt:`@U_0`) to :smt:`@U_1`. Then, interpreting :smt:`x` as :smt:`@U_1`
satisfies the constraints. The Python output gives the same model, but it uses
:python:`Lambda` to define the function.

We next consider how to modify :ref:`Example 5 <Example 5>`. One way to do
this is to additionally require that :smt:`y` and :smt:`z`: are equal.

.. api-examples::
<solutions>/Exercise3b.smt2
<solutions>/Exercise3b.py

The output from |cvcv| is as follows.

.. api-examples::
<solutions>/Exercise3b.out.smt2
<solutions>/Exercise3b.out.py

.. _Solution to Exercise 4:

Solution to Exercise 4
^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 4 <Exercise 4>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

In the SMT-LIB solution, we make use of the :smt:`incremental` options, which
enables the commands :smt:`push` and :smt:`pop`. These commands allow us to
temporarily add one or more assertions, check for satisfiability, and then
return to the previous state. The Python example demonstrates the power of
having the solver embedded in a general-purpose programming language: we can
use a loop to iterate until no better solution is found.

.. api-examples::
<solutions>/Exercise4.smt2
<solutions>/Exercise4.py

The output from |cvcv| is as follows.

.. api-examples::
<solutions>/Exercise4.out.smt2
<solutions>/Exercise4.out.py

.. TODO
.. _Solution to Exercise 5:

Solution to Exercise 5
^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 5 <Exercise 5>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
.. _Solution to Exercise 6:

Solution to Exercise 6
^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 6 <Exercise 6>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
.. _Solution to Exercise 7:

Solution to Exercise 7
^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 7 <Exercise 7>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
.. _Solution to Exercise 8:

Solution to Exercise 8
^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 8 <Exercise 8>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
.. _Solution to Exercise 9:

Solution to Exercise 9
^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 9 <Exercise 9>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
.. _Solution to Exercise 10:

Solution to Exercise 10
^^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 10 <Exercise 10>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
.. _Solution to Exercise 11:

Solution to Exercise 11
^^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 11 <Exercise 11>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
.. _Solution to Exercise 12:

Solution to Exercise 12
^^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 12 <Exercise 12>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
.. _Solution to Exercise 13:

Solution to Exercise 13
^^^^^^^^^^^^^^^^^^^^^^^
Solution to :ref:`Exercise 13 <Exercise 13>`
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

.. TODO
27 changes: 15 additions & 12 deletions tutorials/beginners/conclusion.html
Original file line number Diff line number Diff line change
Expand Up @@ -5,22 +5,25 @@

<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Conclusion &mdash; Satisfiability Modulo Theories: A Beginner&#39;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/tabs.css?v=a5c4661c" />
<link rel="stylesheet" type="text/css" href="static/custom.css?v=b9602cbe" />
<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>
<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/js/theme.js"></script>
<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 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="References" href="references.html" />
Expand Down Expand Up @@ -126,4 +129,4 @@
</script>

</body>
</html>
</html>
27 changes: 15 additions & 12 deletions tutorials/beginners/formal.html
Original file line number Diff line number Diff line change
Expand Up @@ -5,23 +5,26 @@

<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Formal Foundations &mdash; Satisfiability Modulo Theories: A Beginner&#39;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/tabs.css?v=a5c4661c" />
<link rel="stylesheet" type="text/css" href="static/custom.css?v=b9602cbe" />
<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>
<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/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>
<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="SMT Theories" href="theories.html" />
Expand Down Expand Up @@ -288,4 +291,4 @@ <h3>Satisfiability modulo a theory<a class="headerlink" href="#satisfiability-mo
</script>

</body>
</html>
</html>
Loading

0 comments on commit 98998df

Please sign in to comment.