Final version of beginner's tutorial

cvc5 · Aug 10, 2024 · 5fc9ce5 · 5fc9ce5
1 parent e8db9a7
commit 5fc9ce5
Show file tree

Hide file tree

Showing 20 changed files with 1,079 additions and 105 deletions.
diff --git a/_data/menu.yml b/_data/menu.yml
@@ -7,6 +7,9 @@
 - title: Documentation
   url: /docs/index.html
 
+- title: Tutorials
+  url: /tutorials.html
+
 - title: Blog
   url: /blog.html
 

diff --git a/tutorials/beginners/.buildinfo b/tutorials/beginners/.buildinfo
@@ -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: 1e6a6a921061c558b28971484082c548
+config: aa8436ba302ac7e25ac748c5497e9af7
 tags: 645f666f9bcd5a90fca523b33c5a78b7
diff --git a/tutorials/beginners/_sources/conclusion.rst.txt b/tutorials/beginners/_sources/conclusion.rst.txt
@@ -6,7 +6,7 @@ Conclusion
 This tutorial is a basic introduction to using SMT solvers. There are numerous
 resources available for those who wish to learn more.
 
-The SMT-LIB website smt-lib.org has details about the SMT-LIB standard [5],
+The SMT-LIB website `smt-lib.org <http://smt-lib.org>`_ has details about the SMT-LIB standard [5],
 as well as links to software and an extensive collection of benchmarks. More
 information on the foundations of SMT and how solvers work under the hood can
 be found in several overview papers and book chapters [R6]_, [R9]_,

diff --git a/tutorials/beginners/_sources/index.rst.txt b/tutorials/beginners/_sources/index.rst.txt
@@ -28,12 +28,4 @@ SMT-LIB language, using either the cvc5 or the z3 SMT solver.
    references   
    solutions
 
-.. TODO: Add index and search
-
- Indices and tables
- ==================
-
- * :ref:`genindex`
- * :ref:`search`
-
 .. TODO: Add analytics
diff --git a/tutorials/beginners/_sources/overview.rst.txt b/tutorials/beginners/_sources/overview.rst.txt
@@ -120,7 +120,12 @@ this example. The |bvmul| symbol represents bit-vector multiplication, and the
 notation |bvX| is the bit-vector constant whose value, in decimal notation,
 is |X|. Constant |z| names the value we must multiply by 2 to get |x|.  There is no
 solution because an even number does not have a multiplicative inverse in
-machine arithmetic (i.e., when doing arithmetic modulo a power of 2).
+machine arithmetic (i.e., when doing arithmetic modulo a power of 2).  The
+output of |cvcv| is shown below.
+
+.. api-examples::
+    <examples>/Example2.out.smt2
+    <examples>/Example2.out.py
 
 .. _Exercise 2:
 
@@ -161,14 +166,20 @@ for integers and bit-vectors). Next, we declare two functions, |Human| and
 SMT-LIB Boolean sort. A function returning a Boolean is also called a
 *predicate*. We then declare an uninterpreted constant called |Socrates| of
 sort |S|. Now, we are ready to encode the first fact, namely that all humans are
-mortal. To do so, we use the *universal quantifier*, |ForAll|. The assertion states
+mortal. To do so, we use the *universal quantifier* (:smt:`forall` in SMT-LIB,
+|ForAll| in Python). The assertion states
 that for every individual |x| of sort |S|, if the predicate |Human| holds for that
 individual, then the predicate |Mortal| also holds. The next assertion states
 that the |Human| predicate holds for |Socrates|. Finally, we want to see whether
 the fact that Socrates is mortal necessarily follows from the assumptions. To
 do this, we assert the negation of the statement and check for
 satisfiability. Running the example confirms that the result is unsatisfiable
-and thus, indeed, this statement is entailed.
+and thus, indeed, this statement is entailed.  The output of |cvcv| is shown
+below.
+
+.. api-examples::
+   <examples>/socrates.out.smt2
+   <examples>/socrates.out.py
 
 What we have presented so far should provide a good high-level idea of what is
 possible with SMT solvers. [#]_ We cover these ideas in more detail in the

diff --git a/tutorials/beginners/_sources/references.rst.txt b/tutorials/beginners/_sources/references.rst.txt
@@ -21,8 +21,7 @@ References
         (TACAS ’22). Lecture Notes in Computer Science, vol. 13243,
         pp. 415–442. Springer (Apr
         2022). https://doi.org/10.1007/978-3-030-99524-9_24,
-        http://theory.stanford.edu/~barrett/pubs/BBB+22.pdf, Best SCP Tool
-        Paper Award.
+        http://theory.stanford.edu/~barrett/pubs/BBB+22.pdf.
         
 .. [R4] Barbosa, H., Barrett, C.W., Cook, B., Dutertre, B., Kremer, G.,
         Lachnitt, H., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M.,
@@ -101,16 +100,17 @@ References
          Notes in Computer Science, vol. 4121, pp. 170–183. Springer
          (2006). https://doi.org/10.1007/11814948_19
          
-.. [R18] De Moura, L., Bjørner, N.: Satisfiability modulo theories:
-         introduction and ap- plications. Commun. ACM 54(9), 69–77 (sep
+.. [R18] de Moura, L., Bjørner, N.: Satisfiability modulo theories:
+         introduction and applications. Commun. ACM 54(9), 69–77 (sep
          2011). https://doi.org/10.1145/1995376.1995394
          
 .. [R19] Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV
          ’14. Lecture Notes in Computer Science, vol. 8559,
          pp. 737–744. Springer
          (2014). https://doi.org/10.1007/978-3-319-08867-9_49
          
-.. [R20] Dutertre,B.,deMoura,L.M.:Afastlinear-arithmeticsolverforDPLL(T).In:Ball,
+.. [R20] Dutertre, B., de Moura, L.M.:A fast linear-arithmetic solver for
+         DPLL(T). In: Ball,
          T., Jones, R.B. (eds.) Computer Aided Verification, 18th International
          Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006,
          Proceedings. Lecture Notes in Computer Science, vol. 4144,
@@ -127,7 +127,7 @@ References
          (2007). https://doi.org/10.1007/978-3-540-73368-3_52
          
 .. [R23] Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas
-         in sat- isfiabiliby modulo theories. In: Bouajjani, A.,
+         in satisfiabiliby modulo theories. In: Bouajjani, A.,
          Maler, O. (eds.) Computer Aided Verification, 21st International
          Conference, CAV 2009, Grenoble, France, June 26 - July
          2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643,
@@ -233,17 +233,17 @@ References
          (2017). https://doi.org/10.1007/s10703-017-0290-y
          
 .. [R40] Reynolds, A., Tinelli, C., de Moura, L.M.: Finding conflicting
-         instances of quan- tified formulas in SMT. In: Formal Methods in
+         instances of quantified formulas in SMT. In: Formal Methods in
          Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October
          21-24, 2014. pp. 195–202. IEEE
          (2014). https://doi.org/10.1109/FMCAD.2014.6987613
                   
 .. [R41] Roselli, S.F., Bengtsson, K., Åkesson, K.: SMT solvers for job-shop
          scheduling problems: Models comparison and performance evaluation. In:
-         14th IEEE Interna- tional Conference on Automation Science and
+         14th IEEE International Conference on Automation Science and
          Engineering, CASE 2018, Munich, Germany, August
          20-24, 2018. pp. 547–552. IEEE
          (2018). https://doi.org/10.1109/COASE.2018.8560344
          
 .. [R42] Turing, A.M., et al.: On computable numbers, with an application to
-         the entschei- dungsproblem. Journal of Math 58(345-363), 5 (1936)
+         the Entscheidungsproblem. Journal of Math 58(345-363), 5 (1936).
diff --git a/tutorials/beginners/_sources/solutions.rst.txt b/tutorials/beginners/_sources/solutions.rst.txt
@@ -88,7 +88,7 @@ The output from |cvcv| is as follows.
 Solution to :ref:`Exercise 4 <Exercise 4>`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-In the SMT-LIB solution, we make use of the :smt:`incremental` options, which
+In the SMT-LIB solution, we make use of the :smt:`incremental` option, 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
@@ -105,68 +105,169 @@ The output from |cvcv| is as follows.
    <solutions>/Exercise4.out.smt2
    <solutions>/Exercise4.out.py
 
-.. TODO
-
 .. _Solution to Exercise 5:
 
 Solution to :ref:`Exercise 5 <Exercise 5>`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-.. TODO
+.. api-examples::
+   <solutions>/Exercise5.smt2
+   <solutions>/Exercise5.py
+
+The output is as follows.
+
+.. api-examples::
+   <solutions>/Exercise5.out.smt2
+   <solutions>/Exercise5.out.py
 
 .. _Solution to Exercise 6:
 
 Solution to :ref:`Exercise 6 <Exercise 6>`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+The changes are pretty simple. 
+In :ref:`Example 4 <Example 4>`, we proved
+that if the elements in indexes :smt:`i` and :smt:`j`
+are the same, then the arrays are the same.
+The way to do that was to assert that the elements are the same
+while the arrays are different, and expect to get an |unsat|
+answer, which indeed we got.
+
+Now, we want to show that if the elements are different, then 
+so are the arrays. Hence, we would like to assert that
+the elements are different while the arrays are the same.
+Hence, we interchange the equality and dis-equality in the last
+two assertions.
 
-.. TODO
+.. api-examples::
+   <solutions>/Exercise6.smt2
+   <solutions>/Exercise6.py
+
+The output is as follows.
+
+.. api-examples::
+   <solutions>/Exercise6.out.smt2
+   <solutions>/Exercise6.out.py
 
 .. _Solution to Exercise 7:
 
 Solution to :ref:`Exercise 7 <Exercise 7>`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-.. TODO
+.. api-examples::
+   <solutions>/Exercise7.smt2
+   <solutions>/Exercise7.py
+
+The output is as follows.
+
+.. api-examples::
+   <solutions>/Exercise7.out.smt2
+   <solutions>/Exercise7.out.py
 
 .. _Solution to Exercise 8:
 
 Solution to :ref:`Exercise 8 <Exercise 8>`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-.. TODO
+.. api-examples::
+   <solutions>/Exercise8.smt2
+   <solutions>/Exercise8.py
+
+The output is as follows.
+
+.. api-examples::
+   <solutions>/Exercise8.out.smt2
+   <solutions>/Exercise8.out.py
 
 .. _Solution to Exercise 9:
 
 Solution to :ref:`Exercise 9 <Exercise 9>`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-.. TODO
+.. api-examples::
+   <solutions>/Exercise9.smt2
+   <solutions>/Exercise9.py
+
+The output is as follows.
+
+.. api-examples::
+   <solutions>/Exercise9.out.smt2
+   <solutions>/Exercise9.out.py
 
 .. _Solution to Exercise 10:
 
 Solution to :ref:`Exercise 10 <Exercise 10>`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-.. TODO
+We can change the solution to :ref:`Example 12 <Example 12>` to enforce that :smt:`x1` and
+:smt:`x2` have length 1.  With this change, the problem becomes unsatisfiable.
+Thus, to obtain the solution, we add one more layer of concatenations, as shown
+below.
+
+.. api-examples::
+   <solutions>/Exercise10.smt2
+   <solutions>/Exercise10.py
+
+The output is as follows.
+
+.. api-examples::
+   <solutions>/Exercise10.out.smt2
+   <solutions>/Exercise10.out.py
+
+Thus, the answer is that four concatentations are required.
 
 .. _Solution to Exercise 11:
 
 Solution to :ref:`Exercise 11 <Exercise 11>`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+The most natural solution to this exercise seems to be to use the :smt:`seq.prefixof` operator in SMT-LIB
+(:python:`PrefixOf` in python).
+However, this operator only enforces the property of being a prefix,
+not a proper prefix.
+Hence, we also need to add for each pair of variables
+that they are distinct.
+The result is indeed |unsat| as expected.
+
+.. api-examples::
+   <solutions>/Exercise11.smt2
+   <solutions>/Exercise11.py
+
+The output is as follows.
+
+.. api-examples::
+   <solutions>/Exercise11.out.smt2
+   <solutions>/Exercise11.out.py
 
-.. TODO
 
 .. _Solution to Exercise 12:
 
 Solution to :ref:`Exercise 12 <Exercise 12>`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-.. TODO
+.. api-examples::
+   <solutions>/Exercise12.smt2
+   <solutions>/Exercise12.py
+
+The output is as follows.
+
+.. api-examples::
+   <solutions>/Exercise12.out.smt2
+   <solutions>/Exercise12.out.py
 
 .. _Solution to Exercise 13:
 
 Solution to :ref:`Exercise 13 <Exercise 13>`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Set difference does not distribute over intersection.
+The solver is able to find a counterexample for this property.
+
+.. api-examples::
+   <solutions>/Exercise13.smt2
+   <solutions>/Exercise13.py
+
+The output is as follows.
+
+.. api-examples::
+   <solutions>/Exercise13.out.smt2
+   <solutions>/Exercise13.out.py
 
-.. TODO
 
diff --git a/tutorials/beginners/conclusion.html b/tutorials/beginners/conclusion.html
@@ -3,6 +3,15 @@
 <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>Conclusion &mdash; Satisfiability Modulo Theories: A Beginner&#39;s Tutorial  documentation</title>
       <link rel="stylesheet" type="text/css" href="static/pygments.css?v=80d5e7a1" />
@@ -87,7 +96,7 @@
 <span id="id1"></span><h1>Conclusion<a class="headerlink" href="#conclusion" title="Link to this heading"></a></h1>
 <p>This tutorial is a basic introduction to using SMT solvers. There are numerous
 resources available for those who wish to learn more.</p>
-<p>The SMT-LIB website smt-lib.org has details about the SMT-LIB standard [5],
+<p>The SMT-LIB website <a class="reference external" href="http://smt-lib.org">smt-lib.org</a> has details about the SMT-LIB standard [5],
 as well as links to software and an extensive collection of benchmarks. More
 information on the foundations of SMT and how solvers work under the hood can
 be found in several overview papers and book chapters <a class="reference internal" href="references.html#r6" id="id2"><span>[R6]</span></a>, <a class="reference internal" href="references.html#r9" id="id3"><span>[R9]</span></a>,
@@ -129,4 +138,4 @@
   </script> 
 
 </body>
-</html>
+</html>
diff --git a/tutorials/beginners/formal.html b/tutorials/beginners/formal.html
@@ -3,6 +3,15 @@
 <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>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" />
@@ -291,4 +300,4 @@ <h3>Satisfiability modulo a theory<a class="headerlink" href="#satisfiability-mo
   </script> 
 
 </body>
-</html>
+</html>