mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
z3/examples/python/tutorial/html/guide-examples.htm
Nikolaj Bjorner e0a49dd556 html pages for z3 python tutorial 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-07 19:14:54 -07:00

1101 lines
102 KiB
HTML
Raw Blame History

<html>
<head>
<title>Z3Py Guide</title>
<link rel="StyleSheet" href="style.css" type="text/css">
</head>
<body>
<h1>Z3 API in Python</h1>
<p>Z3 is a high performance theorem prover developed at <a target="_blank" href="http://research.microsoft.com">Microsoft Research</a>.
Z3 is used in many applications such as: software/hardware verification and testing, constraint solving, analysis of hybrid systems,
security, biology (in silico analysis), and geometrical problems.</p>
<p>This tutorial demonstrates the main capabilities of Z3Py: the Z3 API in <a target="_blank" href="http://www.python.org">Python</a>.
No Python background is needed to read this tutorial. However, it is useful to learn Python (a fun language!) at some point, and
there are many excellent free resources for doing so (<a target="_blank" href="http://docs.python.org/tutorial/">Python Tutorial</a>).
</p>
<p>The Z3 distribution also contains the <b>C</b>, <b>.Net</b> and <b>OCaml</b> APIs. The source code of Z3Py is available in
the Z3 distribution, feel free to modify it to meet your needs. The source code also demonstrates how to use new features in Z3 4.0.
Other cool front-ends for Z3 include <a target="_blank" href="http://lara.epfl.ch/~psuter/ScalaZ3/">Scala^Z3</a> and <a target="_blank" href="http://hackage.haskell.org/package/sbv">SBV</a>.</p>
<p>
Be sure to follow along with the examples by clicking the <b>load in editor</b> link in the
corner. See what Z3Py says, try your own scripts, and experiment!
</p>
<p>
Please send feedback, comments and/or corrections to <a href="mailto:leonardo@microsoft.com">leonardo@microsoft.com</a>.
Your comments are very valuable.
</p>
<h2>Getting Started</h2>
<p>Let us start with the following simple example:</p>
<example pref="z3py.1"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span> <span class="o">&gt;</span> <span class="mi">2</span><span class="p">,</span> <span class="n">y</span> <span class="o">&lt;</span> <span class="mi">10</span><span class="p">,</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span><span class="o">*</span><span class="n">y</span> <span class="o">==</span> <span class="mi">7</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>The function <tt class="pre">Int('x')</tt> creates an integer variable in Z3 named <tt class="pre">x</tt>.
The <tt class="pre">solve</tt> function solves a system of constraints. The example above uses
two variables <tt class="pre">x</tt> and <tt class="pre">y</tt>, and three constraints.
Z3Py like Python uses <b class="pre">=</b> for assignment. The operators <tt class="pre">&lt;</tt>,
<tt class="pre">&lt;=</tt>,
<tt class="pre">&gt;</tt>,
<tt class="pre">&gt;=</tt>,
<tt class="pre">==</tt> and
<tt class="pre">!=</tt> for comparison.
In the example above, the expression <tt class="pre">x + 2*y == 7</tt> is a Z3 constraint.
Z3 can solve and crunch formulas.
</p>
<p>
The next examples show how to use the Z3 formula/expression simplifier.
</p>
<example pref="z3py.2"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="o">+</span> <span class="mi">2</span><span class="o">*</span><span class="n">x</span> <span class="o">+</span> <span class="mi">3</span><span class="p">)</span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">x</span> <span class="o">&lt;</span> <span class="n">y</span> <span class="o">+</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span><span class="p">)</span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">x</span> <span class="o">+</span> <span class="mi">1</span> <span class="o">&gt;=</span> <span class="mi">3</span><span class="p">,</span> <span class="n">x</span><span class="o">**</span><span class="mi">2</span> <span class="o">+</span> <span class="n">x</span><span class="o">**</span><span class="mi">2</span> <span class="o">+</span> <span class="n">y</span><span class="o">**</span><span class="mi">2</span> <span class="o">+</span> <span class="mi">2</span> <span class="o">&gt;=</span> <span class="mi">5</span><span class="p">))</span>
</pre></div>
</body></html></example>
<p>
By default, Z3Py (for the web) displays formulas and expressions using mathematical notation.
As usual, <tt>&#8743;</tt> is the logical and, <tt>&#8744;</tt> is the logical or, and so on.
The command <tt>set_option(html_mode=False)</tt> makes all formulas and expressions to be
displayed in Z3Py notation. This is also the default mode for the offline version of Z3Py that
comes with the Z3 distribution.
</p>
<example pref="printer"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="k">print</span> <span class="n">x</span><span class="o">**</span><span class="mi">2</span> <span class="o">+</span> <span class="n">y</span><span class="o">**</span><span class="mi">2</span> <span class="o">&gt;=</span> <span class="mi">1</span>
<span class="n">set_option</span><span class="p">(</span><span class="n">html_mode</span><span class="o">=</span><span class="bp">False</span><span class="p">)</span>
<span class="k">print</span> <span class="n">x</span><span class="o">**</span><span class="mi">2</span> <span class="o">+</span> <span class="n">y</span><span class="o">**</span><span class="mi">2</span> <span class="o">&gt;=</span> <span class="mi">1</span>
</pre></div>
</body></html></example>
<p>
Z3 provides functions for traversing expressions.
</p>
<example pref="z3py.3"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="n">n</span> <span class="o">=</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="o">&gt;=</span> <span class="mi">3</span>
<span class="k">print</span> <span class="s">"num args: "</span><span class="p">,</span> <span class="n">n</span><span class="o">.</span><span class="n">num_args</span><span class="p">()</span>
<span class="k">print</span> <span class="s">"children: "</span><span class="p">,</span> <span class="n">n</span><span class="o">.</span><span class="n">children</span><span class="p">()</span>
<span class="k">print</span> <span class="s">"1st child:"</span><span class="p">,</span> <span class="n">n</span><span class="o">.</span><span class="n">arg</span><span class="p">(</span><span class="mi">0</span><span class="p">)</span>
<span class="k">print</span> <span class="s">"2nd child:"</span><span class="p">,</span> <span class="n">n</span><span class="o">.</span><span class="n">arg</span><span class="p">(</span><span class="mi">1</span><span class="p">)</span>
<span class="k">print</span> <span class="s">"operator: "</span><span class="p">,</span> <span class="n">n</span><span class="o">.</span><span class="n">decl</span><span class="p">()</span>
<span class="k">print</span> <span class="s">"op name: "</span><span class="p">,</span> <span class="n">n</span><span class="o">.</span><span class="n">decl</span><span class="p">()</span><span class="o">.</span><span class="n">name</span><span class="p">()</span>
</pre></div>
</body></html></example>
<p>
Z3 provides all basic mathematical operations. Z3Py uses the same operator precedence of the Python language.
Like Python, <tt>**</tt> is the power operator. Z3 can solve nonlinear <i>polynomial</i> constraints.
</p>
<example pref="z3py.4"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span><span class="o">**</span><span class="mi">2</span> <span class="o">+</span> <span class="n">y</span><span class="o">**</span><span class="mi">2</span> <span class="o">&gt;</span> <span class="mi">3</span><span class="p">,</span> <span class="n">x</span><span class="o">**</span><span class="mi">3</span> <span class="o">+</span> <span class="n">y</span> <span class="o">&lt;</span> <span class="mi">5</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>
The procedure <tt>Real('x')</tt> creates the real variable <tt>x</tt>.
Z3Py can represent arbitrarily large integers, rational numbers (like in the example above),
and irrational algebraic numbers. An irrational algebraic number is a root of a polynomial with integer coefficients.
Internally, Z3 represents all these numbers precisely.
The irrational numbers are displayed in decimal notation for making it easy to read the results.
</p>
<example pref="z3py.5"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span><span class="o">**</span><span class="mi">2</span> <span class="o">+</span> <span class="n">y</span><span class="o">**</span><span class="mi">2</span> <span class="o">==</span> <span class="mi">3</span><span class="p">,</span> <span class="n">x</span><span class="o">**</span><span class="mi">3</span> <span class="o">==</span> <span class="mi">2</span><span class="p">)</span>
<span class="n">set_option</span><span class="p">(</span><span class="n">precision</span><span class="o">=</span><span class="mi">30</span><span class="p">)</span>
<span class="k">print</span> <span class="s">"Solving, and displaying result with 30 decimal places"</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span><span class="o">**</span><span class="mi">2</span> <span class="o">+</span> <span class="n">y</span><span class="o">**</span><span class="mi">2</span> <span class="o">==</span> <span class="mi">3</span><span class="p">,</span> <span class="n">x</span><span class="o">**</span><span class="mi">3</span> <span class="o">==</span> <span class="mi">2</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>
The procedure <tt>set_option</tt> is used to configure the Z3 environment. It is used to set global configuration options
such as how the result is displayed. The option <tt>set_option(precision=30)</tt> sets the number of decimal places used when displaying results.
The <tt>?</tt> mark in <tt>1.2599210498?</tt> indicates the output is truncated.
</p>
<p>
The following example demonstrates a common mistake. The expression <tt>3/2</tt> is a Python integer and not a Z3 rational number.
The example also shows different ways to create rational numbers in Z3Py. The procedure <tt>Q(num, den)</tt> creates a
Z3 rational where <tt>num</tt> is the numerator and <tt>den</tt> is the denominator. The <tt>RealVal(1)</tt> creates a Z3 real number
representing the number <tt>1</tt>.
</p>
<example pref="z3py.6"><html><body>
<div class="highlight"><pre><span class="k">print</span> <span class="mi">1</span><span class="o">/</span><span class="mi">3</span>
<span class="k">print</span> <span class="n">RealVal</span><span class="p">(</span><span class="mi">1</span><span class="p">)</span><span class="o">/</span><span class="mi">3</span>
<span class="k">print</span> <span class="n">Q</span><span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="mi">3</span><span class="p">)</span>
<span class="n">x</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="k">print</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span><span class="o">/</span><span class="mi">3</span>
<span class="k">print</span> <span class="n">x</span> <span class="o">+</span> <span class="n">Q</span><span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="mi">3</span><span class="p">)</span>
<span class="k">print</span> <span class="n">x</span> <span class="o">+</span> <span class="s">"1/3"</span>
<span class="k">print</span> <span class="n">x</span> <span class="o">+</span> <span class="mf">0.25</span>
</pre></div>
</body></html></example>
<p>
Rational numbers can also be displayed in decimal notation.
</p>
<example pref="z3py.6aa"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="mi">3</span><span class="o">*</span><span class="n">x</span> <span class="o">==</span> <span class="mi">1</span><span class="p">)</span>
<span class="n">set_option</span><span class="p">(</span><span class="n">rational_to_decimal</span><span class="o">=</span><span class="bp">True</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="mi">3</span><span class="o">*</span><span class="n">x</span> <span class="o">==</span> <span class="mi">1</span><span class="p">)</span>
<span class="n">set_option</span><span class="p">(</span><span class="n">precision</span><span class="o">=</span><span class="mi">30</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="mi">3</span><span class="o">*</span><span class="n">x</span> <span class="o">==</span> <span class="mi">1</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>
A system of constraints may not have a solution. In this case, we say the system is <b>unsatisfiable</b>.
</p>
<example pref="z3py.6a"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span> <span class="o">&gt;</span> <span class="mi">4</span><span class="p">,</span> <span class="n">x</span> <span class="o">&lt;</span> <span class="mi">0</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>
Like in Python, comments begin with the hash character <tt>#</tt> and are terminated by the end of line.
Z3Py does not support comments that span more than one line.
</p>
<example pref="comment"><html><body>
<div class="highlight"><pre><span class="c"># This is a comment</span>
<span class="n">x</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span> <span class="c"># comment: creating x</span>
<span class="k">print</span> <span class="n">x</span><span class="o">**</span><span class="mi">2</span> <span class="o">+</span> <span class="mi">2</span><span class="o">*</span><span class="n">x</span> <span class="o">+</span> <span class="mi">2</span> <span class="c"># comment: printing polynomial</span>
</pre></div>
</body></html></example>
<h2>Boolean Logic</h2>
<p>
Z3 supports Boolean operators: <tt>And</tt>, <tt>Or</tt>, <tt>Not</tt>, <tt>Implies</tt> (implication),
<tt>If</tt> (if-then-else). Bi-implications are represented using equality <tt>==</tt>.
The following example shows how to solve a simple set of Boolean constraints.
</p>
<example pref="z3py.7"><html><body>
<div class="highlight"><pre><span class="n">p</span> <span class="o">=</span> <span class="n">Bool</span><span class="p">(</span><span class="s">'p'</span><span class="p">)</span>
<span class="n">q</span> <span class="o">=</span> <span class="n">Bool</span><span class="p">(</span><span class="s">'q'</span><span class="p">)</span>
<span class="n">r</span> <span class="o">=</span> <span class="n">Bool</span><span class="p">(</span><span class="s">'r'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">Implies</span><span class="p">(</span><span class="n">p</span><span class="p">,</span> <span class="n">q</span><span class="p">),</span> <span class="n">r</span> <span class="o">==</span> <span class="n">Not</span><span class="p">(</span><span class="n">q</span><span class="p">),</span> <span class="n">Or</span><span class="p">(</span><span class="n">Not</span><span class="p">(</span><span class="n">p</span><span class="p">),</span> <span class="n">r</span><span class="p">))</span>
</pre></div>
</body></html></example>
<p>
The Python Boolean constants <tt>True</tt> and <tt>False</tt> can be used to build Z3 Boolean expressions.
</p>
<example pref="z3py.8"><html><body>
<div class="highlight"><pre><span class="n">p</span> <span class="o">=</span> <span class="n">Bool</span><span class="p">(</span><span class="s">'p'</span><span class="p">)</span>
<span class="n">q</span> <span class="o">=</span> <span class="n">Bool</span><span class="p">(</span><span class="s">'q'</span><span class="p">)</span>
<span class="k">print</span> <span class="n">And</span><span class="p">(</span><span class="n">p</span><span class="p">,</span> <span class="n">q</span><span class="p">,</span> <span class="bp">True</span><span class="p">)</span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">p</span><span class="p">,</span> <span class="n">q</span><span class="p">,</span> <span class="bp">True</span><span class="p">))</span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">p</span><span class="p">,</span> <span class="bp">False</span><span class="p">))</span>
</pre></div>
</body></html></example>
<p>The following example uses a combination of polynomial and Boolean constraints.
</p>
<example pref="z3py.9"><html><body>
<div class="highlight"><pre><span class="n">p</span> <span class="o">=</span> <span class="n">Bool</span><span class="p">(</span><span class="s">'p'</span><span class="p">)</span>
<span class="n">x</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">Or</span><span class="p">(</span><span class="n">x</span> <span class="o">&lt;</span> <span class="mi">5</span><span class="p">,</span> <span class="n">x</span> <span class="o">&gt;</span> <span class="mi">10</span><span class="p">),</span> <span class="n">Or</span><span class="p">(</span><span class="n">p</span><span class="p">,</span> <span class="n">x</span><span class="o">**</span><span class="mi">2</span> <span class="o">==</span> <span class="mi">2</span><span class="p">),</span> <span class="n">Not</span><span class="p">(</span><span class="n">p</span><span class="p">))</span>
</pre></div>
</body></html></example>
<h2>Solvers</h2>
<p>Z3 provides different solvers. The command <tt>solve</tt>, used in the previous examples, is implemented using the Z3 solver API.
The implementation can be found in the file <tt>z3.py</tt> in the Z3 distribution.
The following example demonstrates the basic Solver API.
</p>
<example pref="z3py.10"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">Solver</span><span class="p">()</span>
<span class="k">print</span> <span class="n">s</span>
<span class="n">s</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="n">x</span> <span class="o">&gt;</span> <span class="mi">10</span><span class="p">,</span> <span class="n">y</span> <span class="o">==</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span><span class="p">)</span>
<span class="k">print</span> <span class="n">s</span>
<span class="k">print</span> <span class="s">"Solving constraints in the solver s ..."</span>
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">check</span><span class="p">()</span>
<span class="k">print</span> <span class="s">"Create a new scope..."</span>
<span class="n">s</span><span class="o">.</span><span class="n">push</span><span class="p">()</span>
<span class="n">s</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="n">y</span> <span class="o">&lt;</span> <span class="mi">11</span><span class="p">)</span>
<span class="k">print</span> <span class="n">s</span>
<span class="k">print</span> <span class="s">"Solving updated set of constraints..."</span>
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">check</span><span class="p">()</span>
<span class="k">print</span> <span class="s">"Restoring state..."</span>
<span class="n">s</span><span class="o">.</span><span class="n">pop</span><span class="p">()</span>
<span class="k">print</span> <span class="n">s</span>
<span class="k">print</span> <span class="s">"Solving restored set of constraints..."</span>
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">check</span><span class="p">()</span>
</pre></div>
</body></html></example>
<p>
The command <tt>Solver()</tt> creates a general purpose solver. Constraints can be added using the method <tt>add</tt>.
We say the constraints have been <b>asserted</b> in the solver. The method <tt>check()</tt> solves the asserted constraints.
The result is <tt>sat</tt> (satisfiable) if a solution was found. The result is <tt>unsat</tt> (unsatisfiable) if
no solution exists. We may also say the system of asserted constraints is <b>infeasible</b>. Finally, a solver may fail
to solve a system of constraints and <tt>unknown</tt> is returned.
</p>
<p>
In some applications, we want to explore several similar problems that share several constraints.
We can use the commands <tt>push</tt> and <tt>pop</tt> for doing that.
Each solver maintains a stack of assertions. The command <tt>push</tt> creates a new scope by
saving the current stack size.
The command <tt>pop</tt> removes any assertion performed between it and the matching <tt>push</tt>.
The <tt>check</tt> method always operates on the content of solver assertion stack.
</p>
<p>
The following example shows an example that Z3 cannot solve. The solver returns <tt>unknown</tt> in this case.
Recall that Z3 can solve nonlinear polynomial constraints, but <tt>2**x</tt> is not a polynomial.
</p>
<example pref="z3py.11"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">Solver</span><span class="p">()</span>
<span class="n">s</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="mi">2</span><span class="o">**</span><span class="n">x</span> <span class="o">==</span> <span class="mi">3</span><span class="p">)</span>
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">check</span><span class="p">()</span>
</pre></div>
</body></html></example>
<p>
The following example shows how to traverse the constraints asserted into a solver, and how to collect performance statistics for
the <tt>check</tt> method.
</p>
<example pref="z3py.12"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">Solver</span><span class="p">()</span>
<span class="n">s</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="n">x</span> <span class="o">&gt;</span> <span class="mi">1</span><span class="p">,</span> <span class="n">y</span> <span class="o">&gt;</span> <span class="mi">1</span><span class="p">,</span> <span class="n">Or</span><span class="p">(</span><span class="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="o">&gt;</span> <span class="mi">3</span><span class="p">,</span> <span class="n">x</span> <span class="o">-</span> <span class="n">y</span> <span class="o">&lt;</span> <span class="mi">2</span><span class="p">))</span>
<span class="k">print</span> <span class="s">"asserted constraints..."</span>
<span class="k">for</span> <span class="n">c</span> <span class="ow">in</span> <span class="n">s</span><span class="o">.</span><span class="n">assertions</span><span class="p">():</span>
<span class="k">print</span> <span class="n">c</span>
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">check</span><span class="p">()</span>
<span class="k">print</span> <span class="s">"statistics for the last check method..."</span>
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">statistics</span><span class="p">()</span>
<span class="c"># Traversing statistics</span>
<span class="k">for</span> <span class="n">k</span><span class="p">,</span> <span class="n">v</span> <span class="ow">in</span> <span class="n">s</span><span class="o">.</span><span class="n">statistics</span><span class="p">():</span>
<span class="k">print</span> <span class="s">"</span><span class="si">%s</span><span class="s"> : </span><span class="si">%s</span><span class="s">"</span> <span class="o">%</span> <span class="p">(</span><span class="n">k</span><span class="p">,</span> <span class="n">v</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>
The command <tt>check</tt> returns <tt>sat</tt> when Z3 finds a solution for the set of asserted constraints.
We say Z3 <b>satisfied</b> the set of constraints. We say the solution is a <b>model</b> for the set of asserted
constraints. A model is an <b>interpretation</b> that makes each asserted constraint <b>true</b>.
The following example shows the basic methods for inspecting models.
</p>
<example pref="z3py.13"><html><body>
<div class="highlight"><pre><span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">,</span> <span class="n">z</span> <span class="o">=</span> <span class="n">Reals</span><span class="p">(</span><span class="s">'x y z'</span><span class="p">)</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">Solver</span><span class="p">()</span>
<span class="n">s</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="n">x</span> <span class="o">&gt;</span> <span class="mi">1</span><span class="p">,</span> <span class="n">y</span> <span class="o">&gt;</span> <span class="mi">1</span><span class="p">,</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="o">&gt;</span> <span class="mi">3</span><span class="p">,</span> <span class="n">z</span> <span class="o">-</span> <span class="n">x</span> <span class="o">&lt;</span> <span class="mi">10</span><span class="p">)</span>
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">check</span><span class="p">()</span>
<span class="n">m</span> <span class="o">=</span> <span class="n">s</span><span class="o">.</span><span class="n">model</span><span class="p">()</span>
<span class="k">print</span> <span class="s">"x = </span><span class="si">%s</span><span class="s">"</span> <span class="o">%</span> <span class="n">m</span><span class="p">[</span><span class="n">x</span><span class="p">]</span>
<span class="k">print</span> <span class="s">"traversing model..."</span>
<span class="k">for</span> <span class="n">d</span> <span class="ow">in</span> <span class="n">m</span><span class="o">.</span><span class="n">decls</span><span class="p">():</span>
<span class="k">print</span> <span class="s">"</span><span class="si">%s</span><span class="s"> = </span><span class="si">%s</span><span class="s">"</span> <span class="o">%</span> <span class="p">(</span><span class="n">d</span><span class="o">.</span><span class="n">name</span><span class="p">(),</span> <span class="n">m</span><span class="p">[</span><span class="n">d</span><span class="p">])</span>
</pre></div>
</body></html></example>
<p>In the example above, the function <tt>Reals('x y z')</tt> creates the variables. <tt>x</tt>, <tt>y</tt> and <tt>z</tt>.
It is shorthand for:
</p>
<pre>
x = Real('x')
y = Real('y')
z = Real('z')
</pre>
<p>
The expression <tt>m[x]</tt> returns the interpretation of <tt>x</tt> in the model <tt>m</tt>.
The expression <tt>"%s = %s" % (d.name(), m[d])</tt> returns a string where the first <tt>%s</tt> is replaced with
the name of <tt>d</tt> (i.e., <tt>d.name()</tt>), and the second <tt>%s</tt> with a textual representation of the
interpretation of <tt>d</tt> (i.e., <tt>m[d]</tt>). Z3Py automatically converts Z3 objects into a textual representation
when needed.
</p>
<h2>Arithmetic</h2>
<p>Z3 supports real and integer variables. They can be mixed in a single problem.
Like most programming languages, Z3Py will automatically add coercions converting integer expressions to real ones when needed.
The following example demonstrates different ways to declare integer and real variables.
</p>
<example pref="arith.1"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">,</span> <span class="n">c</span> <span class="o">=</span> <span class="n">Reals</span><span class="p">(</span><span class="s">'a b c'</span><span class="p">)</span>
<span class="n">s</span><span class="p">,</span> <span class="n">r</span> <span class="o">=</span> <span class="n">Ints</span><span class="p">(</span><span class="s">'s r'</span><span class="p">)</span>
<span class="k">print</span> <span class="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="o">+</span> <span class="mi">1</span> <span class="o">+</span> <span class="p">(</span><span class="n">a</span> <span class="o">+</span> <span class="n">s</span><span class="p">)</span>
<span class="k">print</span> <span class="n">ToReal</span><span class="p">(</span><span class="n">y</span><span class="p">)</span> <span class="o">+</span> <span class="n">c</span>
</pre></div>
</body></html></example>
<p>The function <tt>ToReal</tt> casts an integer expression into a real expression.</p>
<p>Z3Py supports all basic arithmetic operations.</p>
<example pref="arith.2"><html><body>
<div class="highlight"><pre><span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">,</span> <span class="n">c</span> <span class="o">=</span> <span class="n">Ints</span><span class="p">(</span><span class="s">'a b c'</span><span class="p">)</span>
<span class="n">d</span><span class="p">,</span> <span class="n">e</span> <span class="o">=</span> <span class="n">Reals</span><span class="p">(</span><span class="s">'d e'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">a</span> <span class="o">&gt;</span> <span class="n">b</span> <span class="o">+</span> <span class="mi">2</span><span class="p">,</span>
<span class="n">a</span> <span class="o">==</span> <span class="mi">2</span><span class="o">*</span><span class="n">c</span> <span class="o">+</span> <span class="mi">10</span><span class="p">,</span>
<span class="n">c</span> <span class="o">+</span> <span class="n">b</span> <span class="o">&lt;=</span> <span class="mi">1000</span><span class="p">,</span>
<span class="n">d</span> <span class="o">&gt;=</span> <span class="n">e</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>The command <tt>simplify</tt> applies simple transformations on Z3 expressions.</p>
<example pref="arith.3"><html><body>
<div class="highlight"><pre><span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Reals</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
<span class="c"># Put expression in sum-of-monomials form</span>
<span class="n">t</span> <span class="o">=</span> <span class="n">simplify</span><span class="p">((</span><span class="n">x</span> <span class="o">+</span> <span class="n">y</span><span class="p">)</span><span class="o">**</span><span class="mi">3</span><span class="p">,</span> <span class="n">som</span><span class="o">=</span><span class="bp">True</span><span class="p">)</span>
<span class="k">print</span> <span class="n">t</span>
<span class="c"># Use power operator</span>
<span class="n">t</span> <span class="o">=</span> <span class="n">simplify</span><span class="p">(</span><span class="n">t</span><span class="p">,</span> <span class="n">mul_to_power</span><span class="o">=</span><span class="bp">True</span><span class="p">)</span>
<span class="k">print</span> <span class="n">t</span>
</pre></div>
</body></html></example>
<p>The command <tt>help_simplify()</tt> prints all available options.
Z3Py allows users to write option in two styles. The Z3 internal option names start with <tt>:</tt> and words are separated by <tt>-</tt>.
These options can be used in Z3Py. Z3Py also supports Python-like names,
where <tt>:</tt> is suppressed and <tt>-</tt> is replaced with <tt>_</tt>.
The following example demonstrates how to use both styles.
</p>
<example pref="arith.4"><html><body>
<div class="highlight"><pre><span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Reals</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
<span class="c"># Using Z3 native option names</span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">x</span> <span class="o">==</span> <span class="n">y</span> <span class="o">+</span> <span class="mi">2</span><span class="p">,</span> <span class="s">':arith-lhs'</span><span class="p">,</span> <span class="bp">True</span><span class="p">)</span>
<span class="c"># Using Z3Py option names</span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">x</span> <span class="o">==</span> <span class="n">y</span> <span class="o">+</span> <span class="mi">2</span><span class="p">,</span> <span class="n">arith_lhs</span><span class="o">=</span><span class="bp">True</span><span class="p">)</span>
<span class="k">print</span> <span class="s">"</span><span class="se">\n</span><span class="s">All available options:"</span>
<span class="n">help_simplify</span><span class="p">()</span>
</pre></div>
</body></html></example>
<p>Z3Py supports arbitrarily large numbers. The following example demonstrates how to perform basic arithmetic using larger integer, rational and irrational numbers.
Z3Py only supports <a target="&#148;_blank&#148;" href="http://en.wikipedia.org/wiki/Algebraic_number">algebraic irrational numbers</a>. Algebraic irrational numbers are sufficient for presenting the solutions of systems of polynomial constraints.
Z3Py will always display irrational numbers in decimal notation since it is more convenient to read. The internal representation can be extracted using the method <tt>sexpr()</tt>.
It displays Z3 internal representation for mathematical formulas and expressions in <a target="_blank" href="http://en.wikipedia.org/wiki/S-expression">s-expression</a> (Lisp-like) notation.
</p>
<example pref="arith.5"><html><body>
<div class="highlight"><pre><span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Reals</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span> <span class="o">+</span> <span class="mi">10000000000000000000000</span> <span class="o">==</span> <span class="n">y</span><span class="p">,</span> <span class="n">y</span> <span class="o">&gt;</span> <span class="mi">20000000000000000</span><span class="p">)</span>
<span class="k">print</span> <span class="n">Sqrt</span><span class="p">(</span><span class="mi">2</span><span class="p">)</span> <span class="o">+</span> <span class="n">Sqrt</span><span class="p">(</span><span class="mi">3</span><span class="p">)</span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">Sqrt</span><span class="p">(</span><span class="mi">2</span><span class="p">)</span> <span class="o">+</span> <span class="n">Sqrt</span><span class="p">(</span><span class="mi">3</span><span class="p">))</span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">Sqrt</span><span class="p">(</span><span class="mi">2</span><span class="p">)</span> <span class="o">+</span> <span class="n">Sqrt</span><span class="p">(</span><span class="mi">3</span><span class="p">))</span><span class="o">.</span><span class="n">sexpr</span><span class="p">()</span>
<span class="c"># The sexpr() method is available for any Z3 expression</span>
<span class="k">print</span> <span class="p">(</span><span class="n">x</span> <span class="o">+</span> <span class="n">Sqrt</span><span class="p">(</span><span class="n">y</span><span class="p">)</span> <span class="o">*</span> <span class="mi">2</span><span class="p">)</span><span class="o">.</span><span class="n">sexpr</span><span class="p">()</span>
</pre></div>
</body></html></example>
<h2>Machine Arithmetic</h2>
<p>
Modern CPUs and main-stream programming languages use
arithmetic over fixed-size bit-vectors.
Machine arithmetic is available in Z3Py as <i>Bit-Vectors</i>.
They implement the
precise semantics of unsigned and of
signed <a target="_blank" href="http://en.wikipedia.org/wiki/Two's_complement">two-complements arithmetic</a>.
</p>
<p>
The following example demonstrates how to create bit-vector variables and constants.
The function <tt>BitVec('x', 16)</tt> creates a bit-vector variable in Z3 named <tt>x</tt> with <tt>16</tt> bits.
For convenience, integer constants can be used to create bit-vector expressions in Z3Py.
The function <tt>BitVecVal(10, 32)</tt> creates a bit-vector of size <tt>32</tt> containing the value <tt>10</tt>.
</p>
<example pref="bitvec.1"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">BitVec</span><span class="p">(</span><span class="s">'x'</span><span class="p">,</span> <span class="mi">16</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">BitVec</span><span class="p">(</span><span class="s">'y'</span><span class="p">,</span> <span class="mi">16</span><span class="p">)</span>
<span class="k">print</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">2</span>
<span class="c"># Internal representation</span>
<span class="k">print</span> <span class="p">(</span><span class="n">x</span> <span class="o">+</span> <span class="mi">2</span><span class="p">)</span><span class="o">.</span><span class="n">sexpr</span><span class="p">()</span>
<span class="c"># -1 is equal to 65535 for 16-bit integers </span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="o">-</span> <span class="mi">1</span><span class="p">)</span>
<span class="c"># Creating bit-vector constants</span>
<span class="n">a</span> <span class="o">=</span> <span class="n">BitVecVal</span><span class="p">(</span><span class="o">-</span><span class="mi">1</span><span class="p">,</span> <span class="mi">16</span><span class="p">)</span>
<span class="n">b</span> <span class="o">=</span> <span class="n">BitVecVal</span><span class="p">(</span><span class="mi">65535</span><span class="p">,</span> <span class="mi">16</span><span class="p">)</span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">a</span> <span class="o">==</span> <span class="n">b</span><span class="p">)</span>
<span class="n">a</span> <span class="o">=</span> <span class="n">BitVecVal</span><span class="p">(</span><span class="o">-</span><span class="mi">1</span><span class="p">,</span> <span class="mi">32</span><span class="p">)</span>
<span class="n">b</span> <span class="o">=</span> <span class="n">BitVecVal</span><span class="p">(</span><span class="mi">65535</span><span class="p">,</span> <span class="mi">32</span><span class="p">)</span>
<span class="c"># -1 is not equal to 65535 for 32-bit integers </span>
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">a</span> <span class="o">==</span> <span class="n">b</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>
In contrast to programming languages, such as C, C++, C#, Java,
there is no distinction between signed and unsigned bit-vectors
as numbers. Instead, Z3 provides special signed versions of arithmetical operations
where it makes a difference whether the bit-vector is treated as signed or unsigned.
In Z3Py, the operators
<tt class="pre">&lt;</tt>,
<tt class="pre">&lt;=</tt>,
<tt class="pre">&gt;</tt>,
<tt class="pre">&gt;=</tt>, <tt>/</tt>, <tt>%</tt> and <tt>&gt;&gt;</tt> correspond to the signed versions.
The corresponding unsigned operators are
<tt class="pre">ULT</tt>,
<tt class="pre">ULE</tt>,
<tt class="pre">UGT</tt>,
<tt class="pre">UGE</tt>, <tt>UDiv</tt>, <tt>URem</tt> and <tt>LShR</tt>.
</p>
<example pref="bitvec.2"><html><body>
<div class="highlight"><pre><span class="c"># Create to bit-vectors of size 32</span>
<span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">BitVecs</span><span class="p">(</span><span class="s">'x y'</span><span class="p">,</span> <span class="mi">32</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="o">==</span> <span class="mi">2</span><span class="p">,</span> <span class="n">x</span> <span class="o">&gt;</span> <span class="mi">0</span><span class="p">,</span> <span class="n">y</span> <span class="o">&gt;</span> <span class="mi">0</span><span class="p">)</span>
<span class="c"># Bit-wise operators</span>
<span class="c"># &amp; bit-wise and</span>
<span class="c"># | bit-wise or</span>
<span class="c"># ~ bit-wise not</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span> <span class="o">&amp;</span> <span class="n">y</span> <span class="o">==</span> <span class="o">~</span><span class="n">y</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span> <span class="o">&lt;</span> <span class="mi">0</span><span class="p">)</span>
<span class="c"># using unsigned version of &lt; </span>
<span class="n">solve</span><span class="p">(</span><span class="n">ULT</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="mi">0</span><span class="p">))</span>
</pre></div>
</body></html></example>
<p>
The operator <tt>&gt;&gt;</tt> is the arithmetic shift right, and
<tt>&lt;&lt;</tt> is the shift left. The logical shift right is the operator <tt>LShR</tt>.
</p>
<example pref="bitvec.3"><html><body>
<div class="highlight"><pre><span class="c"># Create to bit-vectors of size 32</span>
<span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">BitVecs</span><span class="p">(</span><span class="s">'x y'</span><span class="p">,</span> <span class="mi">32</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span> <span class="o">&gt;&gt;</span> <span class="mi">2</span> <span class="o">==</span> <span class="mi">3</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span> <span class="o">&lt;&lt;</span> <span class="mi">2</span> <span class="o">==</span> <span class="mi">3</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">x</span> <span class="o">&lt;&lt;</span> <span class="mi">2</span> <span class="o">==</span> <span class="mi">24</span><span class="p">)</span>
</pre></div>
</body></html></example>
<h2>Functions</h2>
<p>
Unlike programming languages, where functions have side-effects, can throw exceptions,
or never return, functions in Z3 have no side-effects and are <b>total</b>.
That is, they are defined on all input values. This includes functions, such
as division. Z3 is based on <a target="_blank" href="http://en.wikipedia.org/wiki/First-order_logic">first-order logic</a>.
</p>
<p>
Given a constraints such as <tt>x + y &gt; 3</tt>, we have been saying that <tt>x</tt> and <tt>y</tt>
are variables. In many textbooks, <tt>x</tt> and <tt>y</tt> are called uninterpreted constants.
That is, they allow any interpretation that is consistent with the constraint <tt>x + y &gt; 3</tt>.
</p>
<p>
More precisely, function and constant symbols in pure first-order logic are <i>uninterpreted</i> or <i>free</i>,
which means that no a priori interpretation is attached.
This is in contrast to functions belonging to the signature of theories,
such as arithmetic where the function <tt>+</tt> has a fixed standard interpretation
(it adds two numbers). Uninterpreted functions and constants are maximally flexible;
they allow any interpretation that is consistent with the constraints over the function or constant.
</p>
<p>
To illustrate uninterpreted functions and constants let us the uninterpreted integer constants (aka variables)
<tt>x</tt>, <tt>y</tt>. Finally let <tt>f</tt> be an uninterpreted function that takes one argument of type (aka sort) integer
and results in an integer value.
The example illustrates how one can force an interpretation where <tt>f</tt>
applied twice to <tt>x</tt> results in <tt>x</tt> again, but <tt>f</tt> applied once to <tt>x</tt> is different from <tt>x</tt>.
</p>
<example pref="z3py.14"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="n">f</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'f'</span><span class="p">,</span> <span class="n">IntSort</span><span class="p">(),</span> <span class="n">IntSort</span><span class="p">())</span>
<span class="n">solve</span><span class="p">(</span><span class="n">f</span><span class="p">(</span><span class="n">f</span><span class="p">(</span><span class="n">x</span><span class="p">))</span> <span class="o">==</span> <span class="n">x</span><span class="p">,</span> <span class="n">f</span><span class="p">(</span><span class="n">x</span><span class="p">)</span> <span class="o">==</span> <span class="n">y</span><span class="p">,</span> <span class="n">x</span> <span class="o">!=</span> <span class="n">y</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>The solution (interpretation) for <tt>f</tt> should be read as <tt>f(0)</tt> is <tt>1</tt>, <tt>f(1)</tt> is <tt>0</tt>, and <tt>f(a)</tt>
is <tt>1</tt> for all <tt>a</tt> different from <tt>0</tt> and <tt>1</tt>.
</p>
<p>In Z3, we can also evaluate expressions in the model for a system of constraints. The following example shows how to
use the <tt>evaluate</tt> method.</p>
<example pref="z3py.15"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'x'</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</span>
<span class="n">f</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'f'</span><span class="p">,</span> <span class="n">IntSort</span><span class="p">(),</span> <span class="n">IntSort</span><span class="p">())</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">Solver</span><span class="p">()</span>
<span class="n">s</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="n">f</span><span class="p">(</span><span class="n">f</span><span class="p">(</span><span class="n">x</span><span class="p">))</span> <span class="o">==</span> <span class="n">x</span><span class="p">,</span> <span class="n">f</span><span class="p">(</span><span class="n">x</span><span class="p">)</span> <span class="o">==</span> <span class="n">y</span><span class="p">,</span> <span class="n">x</span> <span class="o">!=</span> <span class="n">y</span><span class="p">)</span>
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">check</span><span class="p">()</span>
<span class="n">m</span> <span class="o">=</span> <span class="n">s</span><span class="o">.</span><span class="n">model</span><span class="p">()</span>
<span class="k">print</span> <span class="s">"f(f(x)) ="</span><span class="p">,</span> <span class="n">m</span><span class="o">.</span><span class="n">evaluate</span><span class="p">(</span><span class="n">f</span><span class="p">(</span><span class="n">f</span><span class="p">(</span><span class="n">x</span><span class="p">)))</span>
<span class="k">print</span> <span class="s">"f(x) ="</span><span class="p">,</span> <span class="n">m</span><span class="o">.</span><span class="n">evaluate</span><span class="p">(</span><span class="n">f</span><span class="p">(</span><span class="n">x</span><span class="p">))</span>
</pre></div>
</body></html></example>
<h2>Satisfiability and Validity</h2>
<p>A formula/constraint <tt>F</tt> is <b>valid</b> if <tt>F</tt> always evaluates to true for any assignment of appropriate values to its
uninterpreted symbols.
A formula/constraint <tt>F</tt> is <b>satisfiable</b> if there is some assignment of appropriate values
to its uninterpreted symbols under which <tt>F</tt> evaluates to true.
Validity is about finding a proof of a statement; satisfiability is about finding a solution to a set of constraints.
Consider a formula <tt>F</tt> containing <tt>a</tt> and <tt>b</tt>.
We can ask whether <tt>F</tt> is valid, that is whether it is always true for any combination of values for
<tt>a</tt> and <tt>b</tt>. If <tt>F</tt> is always
true, then <tt>Not(F)</tt> is always false, and then <tt>Not(F)</tt> will not have any satisfying assignment (i.e., solution); that is,
<tt>Not(F)</tt> is unsatisfiable. That is,
<tt>F</tt> is valid precisely when <tt>Not(F)</tt> is not satisfiable (is unsatisfiable).
Alternately,
<tt>F</tt> is satisfiable if and only if <tt>Not(F)</tt> is not valid (is invalid).
The following example proves the deMorgan's law.
</p>
<p>The following example redefines the Z3Py function <tt>prove</tt> that receives a formula as a parameter.
This function creates a solver, adds/asserts the negation of the formula, and check if the negation is unsatisfiable.
The implementation of this function is a simpler version of the Z3Py command <tt>prove</tt>.
</p>
<example pref="z3py.16"><html><body>
<div class="highlight"><pre><span class="n">p</span><span class="p">,</span> <span class="n">q</span> <span class="o">=</span> <span class="n">Bools</span><span class="p">(</span><span class="s">'p q'</span><span class="p">)</span>
<span class="n">demorgan</span> <span class="o">=</span> <span class="n">And</span><span class="p">(</span><span class="n">p</span><span class="p">,</span> <span class="n">q</span><span class="p">)</span> <span class="o">==</span> <span class="n">Not</span><span class="p">(</span><span class="n">Or</span><span class="p">(</span><span class="n">Not</span><span class="p">(</span><span class="n">p</span><span class="p">),</span> <span class="n">Not</span><span class="p">(</span><span class="n">q</span><span class="p">)))</span>
<span class="k">print</span> <span class="n">demorgan</span>
<span class="k">def</span> <span class="nf">prove</span><span class="p">(</span><span class="n">f</span><span class="p">):</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">Solver</span><span class="p">()</span>
<span class="n">s</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="n">Not</span><span class="p">(</span><span class="n">f</span><span class="p">))</span>
<span class="k">if</span> <span class="n">s</span><span class="o">.</span><span class="n">check</span><span class="p">()</span> <span class="o">==</span> <span class="n">unsat</span><span class="p">:</span>
<span class="k">print</span> <span class="s">"proved"</span>
<span class="k">else</span><span class="p">:</span>
<span class="k">print</span> <span class="s">"failed to prove"</span>
<span class="k">print</span> <span class="s">"Proving demorgan..."</span>
<span class="n">prove</span><span class="p">(</span><span class="n">demorgan</span><span class="p">)</span>
</pre></div>
</body></html></example>
<h2>List Comprehensions</h2>
<p>
Python supports <a target="_blank" href="http://docs.python.org/tutorial/datastructures.html#list-comprehensions">list comprehensions</a>.
List comprehensions provide a concise way to create lists. They can be used to create Z3 expressions and problems in Z3Py.
The following example demonstrates how to use Python list comprehensions in Z3Py.
</p>
<example pref="list.1"><html><body>
<div class="highlight"><pre><span class="c"># Create list [1, ..., 5] </span>
<span class="k">print</span> <span class="p">[</span> <span class="n">x</span> <span class="o">+</span> <span class="mi">1</span> <span class="k">for</span> <span class="n">x</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">5</span><span class="p">)</span> <span class="p">]</span>
<span class="c"># Create two lists containing 5 integer variables</span>
<span class="n">X</span> <span class="o">=</span> <span class="p">[</span> <span class="n">Int</span><span class="p">(</span><span class="s">'x</span><span class="si">%s</span><span class="s">'</span> <span class="o">%</span> <span class="n">i</span><span class="p">)</span> <span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">5</span><span class="p">)</span> <span class="p">]</span>
<span class="n">Y</span> <span class="o">=</span> <span class="p">[</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y</span><span class="si">%s</span><span class="s">'</span> <span class="o">%</span> <span class="n">i</span><span class="p">)</span> <span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">5</span><span class="p">)</span> <span class="p">]</span>
<span class="k">print</span> <span class="n">X</span>
<span class="c"># Create a list containing X[i]+Y[i]</span>
<span class="n">X_plus_Y</span> <span class="o">=</span> <span class="p">[</span> <span class="n">X</span><span class="p">[</span><span class="n">i</span><span class="p">]</span> <span class="o">+</span> <span class="n">Y</span><span class="p">[</span><span class="n">i</span><span class="p">]</span> <span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">5</span><span class="p">)</span> <span class="p">]</span>
<span class="k">print</span> <span class="n">X_plus_Y</span>
<span class="c"># Create a list containing X[i] &gt; Y[i]</span>
<span class="n">X_gt_Y</span> <span class="o">=</span> <span class="p">[</span> <span class="n">X</span><span class="p">[</span><span class="n">i</span><span class="p">]</span> <span class="o">&gt;</span> <span class="n">Y</span><span class="p">[</span><span class="n">i</span><span class="p">]</span> <span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">5</span><span class="p">)</span> <span class="p">]</span>
<span class="k">print</span> <span class="n">X_gt_Y</span>
<span class="k">print</span> <span class="n">And</span><span class="p">(</span><span class="n">X_gt_Y</span><span class="p">)</span>
<span class="c"># Create a 3x3 "matrix" (list of lists) of integer variables</span>
<span class="n">X</span> <span class="o">=</span> <span class="p">[</span> <span class="p">[</span> <span class="n">Int</span><span class="p">(</span><span class="s">"x_</span><span class="si">%s</span><span class="s">_</span><span class="si">%s</span><span class="s">"</span> <span class="o">%</span> <span class="p">(</span><span class="n">i</span><span class="o">+</span><span class="mi">1</span><span class="p">,</span> <span class="n">j</span><span class="o">+</span><span class="mi">1</span><span class="p">))</span> <span class="k">for</span> <span class="n">j</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">3</span><span class="p">)</span> <span class="p">]</span>
<span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">3</span><span class="p">)</span> <span class="p">]</span>
<span class="n">pp</span><span class="p">(</span><span class="n">X</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>In the example above, the expression <tt>"x%s" % i</tt> returns a string where <tt>%s</tt> is replaced with the value of <tt>i</tt>.</p>
<p>The command <tt>pp</tt> is similar to <tt>print</tt>, but it uses Z3Py formatter for lists and tuples instead of Python's formatter.</p>
<p>Z3Py also provides functions for creating vectors of Boolean, Integer and Real variables. These functions
are implemented using list comprehensions.
</p>
<example pref="list.2"><html><body>
<div class="highlight"><pre><span class="n">X</span> <span class="o">=</span> <span class="n">IntVector</span><span class="p">(</span><span class="s">'x'</span><span class="p">,</span> <span class="mi">5</span><span class="p">)</span>
<span class="n">Y</span> <span class="o">=</span> <span class="n">RealVector</span><span class="p">(</span><span class="s">'y'</span><span class="p">,</span> <span class="mi">5</span><span class="p">)</span>
<span class="n">P</span> <span class="o">=</span> <span class="n">BoolVector</span><span class="p">(</span><span class="s">'p'</span><span class="p">,</span> <span class="mi">5</span><span class="p">)</span>
<span class="k">print</span> <span class="n">X</span>
<span class="k">print</span> <span class="n">Y</span>
<span class="k">print</span> <span class="n">P</span>
<span class="k">print</span> <span class="p">[</span> <span class="n">y</span><span class="o">**</span><span class="mi">2</span> <span class="k">for</span> <span class="n">y</span> <span class="ow">in</span> <span class="n">Y</span> <span class="p">]</span>
<span class="k">print</span> <span class="n">Sum</span><span class="p">([</span> <span class="n">y</span><span class="o">**</span><span class="mi">2</span> <span class="k">for</span> <span class="n">y</span> <span class="ow">in</span> <span class="n">Y</span> <span class="p">])</span>
</pre></div>
</body></html></example>
<h2>Kinematic Equations</h2>
<p>
In high school, students learn the kinematic equations.
These equations describe the mathematical relationship between <b>displacement</b> (<tt>d</tt>),
<b>time</b> (<tt>t</tt>), <b>acceleration</b> (<tt>a</tt>), <b>initial velocity</b> (<tt>v_i</tt>) and <b>final velocity</b> (<tt>v_f</tt>).
In Z3Py notation, we can write these equations as:
</p>
<pre>
d == v_i * t + (a*t**2)/2,
v_f == v_i + a*t
</pre>
<h3>Problem 1</h3>
<p>
Ima Hurryin is approaching a stoplight moving with a velocity of <tt>30.0</tt> m/s.
The light turns yellow, and Ima applies the brakes and skids to a stop.
If Ima's acceleration is <tt>-8.00</tt> m/s<sup>2</sup>, then determine the displacement of the
car during the skidding process.
</p>
<example pref="k.1"><html><body>
<div class="highlight"><pre><span class="n">d</span><span class="p">,</span> <span class="n">a</span><span class="p">,</span> <span class="n">t</span><span class="p">,</span> <span class="n">v_i</span><span class="p">,</span> <span class="n">v_f</span> <span class="o">=</span> <span class="n">Reals</span><span class="p">(</span><span class="s">'d a t v__i v__f'</span><span class="p">)</span>
<span class="n">equations</span> <span class="o">=</span> <span class="p">[</span>
<span class="n">d</span> <span class="o">==</span> <span class="n">v_i</span> <span class="o">*</span> <span class="n">t</span> <span class="o">+</span> <span class="p">(</span><span class="n">a</span><span class="o">*</span><span class="n">t</span><span class="o">**</span><span class="mi">2</span><span class="p">)</span><span class="o">/</span><span class="mi">2</span><span class="p">,</span>
<span class="n">v_f</span> <span class="o">==</span> <span class="n">v_i</span> <span class="o">+</span> <span class="n">a</span><span class="o">*</span><span class="n">t</span><span class="p">,</span>
<span class="p">]</span>
<span class="k">print</span> <span class="s">"Kinematic equations:"</span>
<span class="k">print</span> <span class="n">equations</span>
<span class="c"># Given v_i, v_f and a, find d</span>
<span class="n">problem</span> <span class="o">=</span> <span class="p">[</span>
<span class="n">v_i</span> <span class="o">==</span> <span class="mi">30</span><span class="p">,</span>
<span class="n">v_f</span> <span class="o">==</span> <span class="mi">0</span><span class="p">,</span>
<span class="n">a</span> <span class="o">==</span> <span class="o">-</span><span class="mi">8</span>
<span class="p">]</span>
<span class="k">print</span> <span class="s">"Problem:"</span>
<span class="k">print</span> <span class="n">problem</span>
<span class="k">print</span> <span class="s">"Solution:"</span>
<span class="n">solve</span><span class="p">(</span><span class="n">equations</span> <span class="o">+</span> <span class="n">problem</span><span class="p">)</span>
</pre></div>
</body></html></example>
<h3>Problem 2</h3>
<p>
Ben Rushin is waiting at a stoplight. When it finally turns green, Ben accelerated from rest at a rate of
a <tt>6.00</tt> m/s<sup>2</sup> for a time of <tt>4.10</tt> seconds. Determine the displacement of Ben's car during this time period.
</p>
<example pref="k.2"><html><body>
<div class="highlight"><pre><span class="n">d</span><span class="p">,</span> <span class="n">a</span><span class="p">,</span> <span class="n">t</span><span class="p">,</span> <span class="n">v_i</span><span class="p">,</span> <span class="n">v_f</span> <span class="o">=</span> <span class="n">Reals</span><span class="p">(</span><span class="s">'d a t v__i v__f'</span><span class="p">)</span>
<span class="n">equations</span> <span class="o">=</span> <span class="p">[</span>
<span class="n">d</span> <span class="o">==</span> <span class="n">v_i</span> <span class="o">*</span> <span class="n">t</span> <span class="o">+</span> <span class="p">(</span><span class="n">a</span><span class="o">*</span><span class="n">t</span><span class="o">**</span><span class="mi">2</span><span class="p">)</span><span class="o">/</span><span class="mi">2</span><span class="p">,</span>
<span class="n">v_f</span> <span class="o">==</span> <span class="n">v_i</span> <span class="o">+</span> <span class="n">a</span><span class="o">*</span><span class="n">t</span><span class="p">,</span>
<span class="p">]</span>
<span class="c"># Given v_i, t and a, find d</span>
<span class="n">problem</span> <span class="o">=</span> <span class="p">[</span>
<span class="n">v_i</span> <span class="o">==</span> <span class="mi">0</span><span class="p">,</span>
<span class="n">t</span> <span class="o">==</span> <span class="mf">4.10</span><span class="p">,</span>
<span class="n">a</span> <span class="o">==</span> <span class="mi">6</span>
<span class="p">]</span>
<span class="n">solve</span><span class="p">(</span><span class="n">equations</span> <span class="o">+</span> <span class="n">problem</span><span class="p">)</span>
<span class="c"># Display rationals in decimal notation</span>
<span class="n">set_option</span><span class="p">(</span><span class="n">rational_to_decimal</span><span class="o">=</span><span class="bp">True</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">equations</span> <span class="o">+</span> <span class="n">problem</span><span class="p">)</span>
</pre></div>
</body></html></example>
<h2>Bit Tricks</h2>
<p>Some low level <a target="_blank" href="http://graphics.stanford.edu/~seander/bithacks.html">hacks</a> are very popular with C programmers.
We use some of these hacks in the Z3 implementation.
</p>
<h3>Power of two</h3>
<p>This hack is frequently used in C programs (Z3 included) to test whether a machine integer is a power of two.
We can use Z3 to prove it really works. The claim is that <tt>x != 0 &amp;&amp; !(x &amp; (x - 1))</tt> is true if and only if <tt>x</tt>
is a power of two.
</p>
<example pref="bit.1"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">BitVec</span><span class="p">(</span><span class="s">'x'</span><span class="p">,</span> <span class="mi">32</span><span class="p">)</span>
<span class="n">powers</span> <span class="o">=</span> <span class="p">[</span> <span class="mi">2</span><span class="o">**</span><span class="n">i</span> <span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">32</span><span class="p">)</span> <span class="p">]</span>
<span class="n">fast</span> <span class="o">=</span> <span class="n">And</span><span class="p">(</span><span class="n">x</span> <span class="o">!=</span> <span class="mi">0</span><span class="p">,</span> <span class="n">x</span> <span class="o">&amp;</span> <span class="p">(</span><span class="n">x</span> <span class="o">-</span> <span class="mi">1</span><span class="p">)</span> <span class="o">==</span> <span class="mi">0</span><span class="p">)</span>
<span class="n">slow</span> <span class="o">=</span> <span class="n">Or</span><span class="p">([</span> <span class="n">x</span> <span class="o">==</span> <span class="n">p</span> <span class="k">for</span> <span class="n">p</span> <span class="ow">in</span> <span class="n">powers</span> <span class="p">])</span>
<span class="k">print</span> <span class="n">fast</span>
<span class="n">prove</span><span class="p">(</span><span class="n">fast</span> <span class="o">==</span> <span class="n">slow</span><span class="p">)</span>
<span class="k">print</span> <span class="s">"trying to prove buggy version..."</span>
<span class="n">fast</span> <span class="o">=</span> <span class="n">x</span> <span class="o">&amp;</span> <span class="p">(</span><span class="n">x</span> <span class="o">-</span> <span class="mi">1</span><span class="p">)</span> <span class="o">==</span> <span class="mi">0</span>
<span class="n">prove</span><span class="p">(</span><span class="n">fast</span> <span class="o">==</span> <span class="n">slow</span><span class="p">)</span>
</pre></div>
</body></html></example>
<h3>Opposite signs</h3>
<p>The following simple hack can be used to test whether two machine integers have opposite signs.</p>
<example pref="bit.2"><html><body>
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">BitVec</span><span class="p">(</span><span class="s">'x'</span><span class="p">,</span> <span class="mi">32</span><span class="p">)</span>
<span class="n">y</span> <span class="o">=</span> <span class="n">BitVec</span><span class="p">(</span><span class="s">'y'</span><span class="p">,</span> <span class="mi">32</span><span class="p">)</span>
<span class="c"># Claim: (x ^ y) &lt; 0 iff x and y have opposite signs</span>
<span class="n">trick</span> <span class="o">=</span> <span class="p">(</span><span class="n">x</span> <span class="o">^</span> <span class="n">y</span><span class="p">)</span> <span class="o">&lt;</span> <span class="mi">0</span>
<span class="c"># Naive way to check if x and y have opposite signs</span>
<span class="n">opposite</span> <span class="o">=</span> <span class="n">Or</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">x</span> <span class="o">&lt;</span> <span class="mi">0</span><span class="p">,</span> <span class="n">y</span> <span class="o">&gt;=</span> <span class="mi">0</span><span class="p">),</span>
<span class="n">And</span><span class="p">(</span><span class="n">x</span> <span class="o">&gt;=</span> <span class="mi">0</span><span class="p">,</span> <span class="n">y</span> <span class="o">&lt;</span> <span class="mi">0</span><span class="p">))</span>
<span class="n">prove</span><span class="p">(</span><span class="n">trick</span> <span class="o">==</span> <span class="n">opposite</span><span class="p">)</span>
</pre></div>
</body></html></example>
<h2>Puzzles</h2>
<h3>Dog, Cat and Mouse</h3>
<p>Consider the following puzzle. Spend exactly 100 dollars and buy exactly 100 animals.
Dogs cost 15 dollars, cats cost 1 dollar, and mice cost 25 cents each.
You have to buy at least one of each.
How many of each should you buy?
</p>
<example pref="puzzle.1"><html><body>
<div class="highlight"><pre><span class="c"># Create 3 integer variables</span>
<span class="n">dog</span><span class="p">,</span> <span class="n">cat</span><span class="p">,</span> <span class="n">mouse</span> <span class="o">=</span> <span class="n">Ints</span><span class="p">(</span><span class="s">'dog cat mouse'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">dog</span> <span class="o">&gt;=</span> <span class="mi">1</span><span class="p">,</span> <span class="c"># at least one dog</span>
<span class="n">cat</span> <span class="o">&gt;=</span> <span class="mi">1</span><span class="p">,</span> <span class="c"># at least one cat</span>
<span class="n">mouse</span> <span class="o">&gt;=</span> <span class="mi">1</span><span class="p">,</span> <span class="c"># at least one mouse</span>
<span class="c"># we want to buy 100 animals</span>
<span class="n">dog</span> <span class="o">+</span> <span class="n">cat</span> <span class="o">+</span> <span class="n">mouse</span> <span class="o">==</span> <span class="mi">100</span><span class="p">,</span>
<span class="c"># We have 100 dollars (10000 cents):</span>
<span class="c"># dogs cost 15 dollars (1500 cents), </span>
<span class="c"># cats cost 1 dollar (100 cents), and </span>
<span class="c"># mice cost 25 cents </span>
<span class="mi">1500</span> <span class="o">*</span> <span class="n">dog</span> <span class="o">+</span> <span class="mi">100</span> <span class="o">*</span> <span class="n">cat</span> <span class="o">+</span> <span class="mi">25</span> <span class="o">*</span> <span class="n">mouse</span> <span class="o">==</span> <span class="mi">10000</span><span class="p">)</span>
</pre></div>
</body></html></example>
<h3>Sudoku</h3>
<p><a target="_blank" href="http://www.dailysudoku.com/sudoku/">Sudoku</a> is a very popular puzzle.
The goal is to insert the numbers in the boxes to satisfy only one condition: each row, column and
<tt>3x3</tt> box must contain the digits <tt>1</tt> through <tt>9</tt> exactly once.
</p>
<img style="width:213px;margin:20px;" src="examples/sudoku.png">
<p>
The following example encodes the sudoku problem in Z3. Different sudoku instances can be solved
by modifying the matrix <tt>instance</tt>. This example makes heavy use of
<a target="_blank" href="http://docs.python.org/tutorial/datastructures.html#list-comprehensions">list comprehensions</a>
available in the Python programming language.
</p>
<example pref="puzzle.2"><html><body>
<div class="highlight"><pre><span class="c"># 9x9 matrix of integer variables</span>
<span class="n">X</span> <span class="o">=</span> <span class="p">[</span> <span class="p">[</span> <span class="n">Int</span><span class="p">(</span><span class="s">"x_</span><span class="si">%s</span><span class="s">_</span><span class="si">%s</span><span class="s">"</span> <span class="o">%</span> <span class="p">(</span><span class="n">i</span><span class="o">+</span><span class="mi">1</span><span class="p">,</span> <span class="n">j</span><span class="o">+</span><span class="mi">1</span><span class="p">))</span> <span class="k">for</span> <span class="n">j</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="p">]</span>
<span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="p">]</span>
<span class="c"># each cell contains a value in {1, ..., 9}</span>
<span class="n">cells_c</span> <span class="o">=</span> <span class="p">[</span> <span class="n">And</span><span class="p">(</span><span class="mi">1</span> <span class="o">&lt;=</span> <span class="n">X</span><span class="p">[</span><span class="n">i</span><span class="p">][</span><span class="n">j</span><span class="p">],</span> <span class="n">X</span><span class="p">[</span><span class="n">i</span><span class="p">][</span><span class="n">j</span><span class="p">]</span> <span class="o">&lt;=</span> <span class="mi">9</span><span class="p">)</span>
<span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="k">for</span> <span class="n">j</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="p">]</span>
<span class="c"># each row contains a digit at most once</span>
<span class="n">rows_c</span> <span class="o">=</span> <span class="p">[</span> <span class="n">Distinct</span><span class="p">(</span><span class="n">X</span><span class="p">[</span><span class="n">i</span><span class="p">])</span> <span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="p">]</span>
<span class="c"># each column contains a digit at most once</span>
<span class="n">cols_c</span> <span class="o">=</span> <span class="p">[</span> <span class="n">Distinct</span><span class="p">([</span> <span class="n">X</span><span class="p">[</span><span class="n">i</span><span class="p">][</span><span class="n">j</span><span class="p">]</span> <span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="p">])</span>
<span class="k">for</span> <span class="n">j</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="p">]</span>
<span class="c"># each 3x3 square contains a digit at most once</span>
<span class="n">sq_c</span> <span class="o">=</span> <span class="p">[</span> <span class="n">Distinct</span><span class="p">([</span> <span class="n">X</span><span class="p">[</span><span class="mi">3</span><span class="o">*</span><span class="n">i0</span> <span class="o">+</span> <span class="n">i</span><span class="p">][</span><span class="mi">3</span><span class="o">*</span><span class="n">j0</span> <span class="o">+</span> <span class="n">j</span><span class="p">]</span>
<span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">3</span><span class="p">)</span> <span class="k">for</span> <span class="n">j</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">3</span><span class="p">)</span> <span class="p">])</span>
<span class="k">for</span> <span class="n">i0</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">3</span><span class="p">)</span> <span class="k">for</span> <span class="n">j0</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">3</span><span class="p">)</span> <span class="p">]</span>
<span class="n">sudoku_c</span> <span class="o">=</span> <span class="n">cells_c</span> <span class="o">+</span> <span class="n">rows_c</span> <span class="o">+</span> <span class="n">cols_c</span> <span class="o">+</span> <span class="n">sq_c</span>
<span class="c"># sudoku instance, we use '0' for empty cells</span>
<span class="n">instance</span> <span class="o">=</span> <span class="p">((</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">9</span><span class="p">,</span><span class="mi">4</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">3</span><span class="p">,</span><span class="mi">0</span><span class="p">),</span>
<span class="p">(</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">5</span><span class="p">,</span><span class="mi">1</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">7</span><span class="p">),</span>
<span class="p">(</span><span class="mi">0</span><span class="p">,</span><span class="mi">8</span><span class="p">,</span><span class="mi">9</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">4</span><span class="p">,</span><span class="mi">0</span><span class="p">),</span>
<span class="p">(</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">2</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">8</span><span class="p">),</span>
<span class="p">(</span><span class="mi">0</span><span class="p">,</span><span class="mi">6</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">2</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">1</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">5</span><span class="p">,</span><span class="mi">0</span><span class="p">),</span>
<span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">2</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">),</span>
<span class="p">(</span><span class="mi">0</span><span class="p">,</span><span class="mi">7</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">5</span><span class="p">,</span><span class="mi">2</span><span class="p">,</span><span class="mi">0</span><span class="p">),</span>
<span class="p">(</span><span class="mi">9</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">6</span><span class="p">,</span><span class="mi">5</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">),</span>
<span class="p">(</span><span class="mi">0</span><span class="p">,</span><span class="mi">4</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">9</span><span class="p">,</span><span class="mi">7</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">,</span><span class="mi">0</span><span class="p">))</span>
<span class="n">instance_c</span> <span class="o">=</span> <span class="p">[</span> <span class="n">If</span><span class="p">(</span><span class="n">instance</span><span class="p">[</span><span class="n">i</span><span class="p">][</span><span class="n">j</span><span class="p">]</span> <span class="o">==</span> <span class="mi">0</span><span class="p">,</span>
<span class="bp">True</span><span class="p">,</span>
<span class="n">X</span><span class="p">[</span><span class="n">i</span><span class="p">][</span><span class="n">j</span><span class="p">]</span> <span class="o">==</span> <span class="n">instance</span><span class="p">[</span><span class="n">i</span><span class="p">][</span><span class="n">j</span><span class="p">])</span>
<span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="k">for</span> <span class="n">j</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="p">]</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">Solver</span><span class="p">()</span>
<span class="n">s</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="n">sudoku_c</span> <span class="o">+</span> <span class="n">instance_c</span><span class="p">)</span>
<span class="k">if</span> <span class="n">s</span><span class="o">.</span><span class="n">check</span><span class="p">()</span> <span class="o">==</span> <span class="n">sat</span><span class="p">:</span>
<span class="n">m</span> <span class="o">=</span> <span class="n">s</span><span class="o">.</span><span class="n">model</span><span class="p">()</span>
<span class="n">r</span> <span class="o">=</span> <span class="p">[</span> <span class="p">[</span> <span class="n">m</span><span class="o">.</span><span class="n">evaluate</span><span class="p">(</span><span class="n">X</span><span class="p">[</span><span class="n">i</span><span class="p">][</span><span class="n">j</span><span class="p">])</span> <span class="k">for</span> <span class="n">j</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="p">]</span>
<span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">9</span><span class="p">)</span> <span class="p">]</span>
<span class="n">print_matrix</span><span class="p">(</span><span class="n">r</span><span class="p">)</span>
<span class="k">else</span><span class="p">:</span>
<span class="k">print</span> <span class="s">"failed to solve"</span>
</pre></div>
</body></html></example>
<h3>Eight Queens</h3>
<p>
The eight queens puzzle is the problem of placing eight chess queens on an 8x8 chessboard so that no two queens attack each other.
Thus, a solution requires that no two queens share the same row, column, or diagonal.
</p>
<p> <img style="margin:20px;" src="examples/queens.png">
</p>
<example pref="puzzle.3"><html><body>
<div class="highlight"><pre><span class="c"># We know each queen must be in a different row.</span>
<span class="c"># So, we represent each queen by a single integer: the column position</span>
<span class="n">Q</span> <span class="o">=</span> <span class="p">[</span> <span class="n">Int</span><span class="p">(</span><span class="s">'Q_</span><span class="si">%i</span><span class="s">'</span> <span class="o">%</span> <span class="p">(</span><span class="n">i</span> <span class="o">+</span> <span class="mi">1</span><span class="p">))</span> <span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">8</span><span class="p">)</span> <span class="p">]</span>
<span class="c"># Each queen is in a column {1, ... 8 }</span>
<span class="n">val_c</span> <span class="o">=</span> <span class="p">[</span> <span class="n">And</span><span class="p">(</span><span class="mi">1</span> <span class="o">&lt;=</span> <span class="n">Q</span><span class="p">[</span><span class="n">i</span><span class="p">],</span> <span class="n">Q</span><span class="p">[</span><span class="n">i</span><span class="p">]</span> <span class="o">&lt;=</span> <span class="mi">8</span><span class="p">)</span> <span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">8</span><span class="p">)</span> <span class="p">]</span>
<span class="c"># At most one queen per column</span>
<span class="n">col_c</span> <span class="o">=</span> <span class="p">[</span> <span class="n">Distinct</span><span class="p">(</span><span class="n">Q</span><span class="p">)</span> <span class="p">]</span>
<span class="c"># Diagonal constraint</span>
<span class="n">diag_c</span> <span class="o">=</span> <span class="p">[</span> <span class="n">If</span><span class="p">(</span><span class="n">i</span> <span class="o">==</span> <span class="n">j</span><span class="p">,</span>
<span class="bp">True</span><span class="p">,</span>
<span class="n">And</span><span class="p">(</span><span class="n">Q</span><span class="p">[</span><span class="n">i</span><span class="p">]</span> <span class="o">-</span> <span class="n">Q</span><span class="p">[</span><span class="n">j</span><span class="p">]</span> <span class="o">!=</span> <span class="n">i</span> <span class="o">-</span> <span class="n">j</span><span class="p">,</span> <span class="n">Q</span><span class="p">[</span><span class="n">i</span><span class="p">]</span> <span class="o">-</span> <span class="n">Q</span><span class="p">[</span><span class="n">j</span><span class="p">]</span> <span class="o">!=</span> <span class="n">j</span> <span class="o">-</span> <span class="n">i</span><span class="p">))</span>
<span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">8</span><span class="p">)</span> <span class="k">for</span> <span class="n">j</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="n">i</span><span class="p">)</span> <span class="p">]</span>
<span class="n">solve</span><span class="p">(</span><span class="n">val_c</span> <span class="o">+</span> <span class="n">col_c</span> <span class="o">+</span> <span class="n">diag_c</span><span class="p">)</span>
</pre></div>
</body></html></example>
<h2>Application: Install Problem</h2>
<p>The <b>install problem</b> consists of determining whether a new set of packages can be installed in a system.
This application is based on the article
<a target="_blank" href="http://cseweb.ucsd.edu/~rjhala/papers/opium.pdf">OPIUM: Optimal Package Install/Uninstall Manager</a>.
Many packages depend on other packages to provide some functionality.
Each distribution contains a meta-data file that
explicates the requirements of each package of the distribution.
The meta-data contains details like the name, version, etc. More importantly, it contains
<b>depends</b> and <b>conflicts</b>
clauses that stipulate which other packages should be on the
system. The depends clauses stipulate which other packages must be present.
The conflicts clauses stipulate which other packages must not be present.
</p>
<p>The install problem can be easily solved using Z3. The idea is to define a Boolean variable for each
package. This variable is true if the package must be in the system. If package <tt>a</tt> depends on
packages <tt>b</tt>, <tt>c</tt> and <tt>z</tt>, we write:
</p>
<pre>
DependsOn(a, [b, c, z])
</pre>
<p><tt>DependsOn</tt> is a simple Python function that creates Z3 constraints that capture the
depends clause semantics.
</p>
<pre>
def DependsOn(pack, deps):
return And([ Implies(pack, dep) for dep in deps ])
</pre>
<p>
Thus, <tt>Depends(a, [b, c, z])</tt> generates the constraint
</p>
<pre>
And(Implies(a, b), Implies(a, c), Implies(a, z))
</pre>
<p>That is, if users install package <tt>a</tt>, they must also install packages
<tt>b</tt>, <tt>c</tt> and <tt>z</tt>.
</p>
<p>
If package <tt>d</tt> conflicts with package <tt>e</tt>, we write <tt>Conflict(d, e)</tt>.
<tt>Conflict</tt> is also a simple Python function.
</p>
<pre>
def Conflict(p1, p2):
return Or(Not(p1), Not(p2))
</pre>
<p><tt>Conflict(d, e)</tt> generates the constraint <tt>Or(Not(d), Not(e))</tt>.
With these two functions, we can easily encode the example in the
<a target="_blank" href="http://cseweb.ucsd.edu/~rjhala/papers/opium.pdf">Opium article</a> (Section 2) in Z3Py as:
</p>
<example pref="install.1"><html><body>
<div class="highlight"><pre><span class="k">def</span> <span class="nf">DependsOn</span><span class="p">(</span><span class="n">pack</span><span class="p">,</span> <span class="n">deps</span><span class="p">):</span>
<span class="k">return</span> <span class="n">And</span><span class="p">([</span> <span class="n">Implies</span><span class="p">(</span><span class="n">pack</span><span class="p">,</span> <span class="n">dep</span><span class="p">)</span> <span class="k">for</span> <span class="n">dep</span> <span class="ow">in</span> <span class="n">deps</span> <span class="p">])</span>
<span class="k">def</span> <span class="nf">Conflict</span><span class="p">(</span><span class="n">p1</span><span class="p">,</span> <span class="n">p2</span><span class="p">):</span>
<span class="k">return</span> <span class="n">Or</span><span class="p">(</span><span class="n">Not</span><span class="p">(</span><span class="n">p1</span><span class="p">),</span> <span class="n">Not</span><span class="p">(</span><span class="n">p2</span><span class="p">))</span>
<span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">,</span> <span class="n">c</span><span class="p">,</span> <span class="n">d</span><span class="p">,</span> <span class="n">e</span><span class="p">,</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">,</span> <span class="n">z</span> <span class="o">=</span> <span class="n">Bools</span><span class="p">(</span><span class="s">'a b c d e f g z'</span><span class="p">)</span>
<span class="n">solve</span><span class="p">(</span><span class="n">DependsOn</span><span class="p">(</span><span class="n">a</span><span class="p">,</span> <span class="p">[</span><span class="n">b</span><span class="p">,</span> <span class="n">c</span><span class="p">,</span> <span class="n">z</span><span class="p">]),</span>
<span class="n">DependsOn</span><span class="p">(</span><span class="n">b</span><span class="p">,</span> <span class="p">[</span><span class="n">d</span><span class="p">]),</span>
<span class="n">DependsOn</span><span class="p">(</span><span class="n">c</span><span class="p">,</span> <span class="p">[</span><span class="n">Or</span><span class="p">(</span><span class="n">d</span><span class="p">,</span> <span class="n">e</span><span class="p">),</span> <span class="n">Or</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)]),</span>
<span class="n">Conflict</span><span class="p">(</span><span class="n">d</span><span class="p">,</span> <span class="n">e</span><span class="p">),</span>
<span class="n">a</span><span class="p">,</span> <span class="n">z</span><span class="p">)</span>
</pre></div>
</body></html></example>
<p>
Note that the example contains the constraint
</p>
<pre>
DependsOn(c, [Or(d, e), Or(f, g)]),
</pre>
<p>
The meaning is: to install <tt>c</tt>, we must install <tt>d</tt> or <tt>e</tt>, and <tt>f</tt> or <tt>g</tt>
</p>
<p>Now, we refine the previous example. First, we modify <tt>DependsOn</tt> to allow
us to write <tt>DependsOn(b, d)</tt> instead of <tt>DependsOn(b, [d])</tt>. We also
write a function <tt>install_check</tt> that returns a list of packages that must be installed
in the system. The function <tt>Conflict</tt> is also modified. It can now receive multiple
arguments.
</p>
<example pref="install.2"><html><body>
<div class="highlight"><pre><span class="k">def</span> <span class="nf">DependsOn</span><span class="p">(</span><span class="n">pack</span><span class="p">,</span> <span class="n">deps</span><span class="p">):</span>
<span class="k">if</span> <span class="n">is_expr</span><span class="p">(</span><span class="n">deps</span><span class="p">):</span>
<span class="k">return</span> <span class="n">Implies</span><span class="p">(</span><span class="n">pack</span><span class="p">,</span> <span class="n">deps</span><span class="p">)</span>
<span class="k">else</span><span class="p">:</span>
<span class="k">return</span> <span class="n">And</span><span class="p">([</span> <span class="n">Implies</span><span class="p">(</span><span class="n">pack</span><span class="p">,</span> <span class="n">dep</span><span class="p">)</span> <span class="k">for</span> <span class="n">dep</span> <span class="ow">in</span> <span class="n">deps</span> <span class="p">])</span>
<span class="k">def</span> <span class="nf">Conflict</span><span class="p">(</span><span class="o">*</span><span class="n">packs</span><span class="p">):</span>
<span class="k">return</span> <span class="n">Or</span><span class="p">([</span> <span class="n">Not</span><span class="p">(</span><span class="n">pack</span><span class="p">)</span> <span class="k">for</span> <span class="n">pack</span> <span class="ow">in</span> <span class="n">packs</span> <span class="p">])</span>
<span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">,</span> <span class="n">c</span><span class="p">,</span> <span class="n">d</span><span class="p">,</span> <span class="n">e</span><span class="p">,</span> <span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">,</span> <span class="n">z</span> <span class="o">=</span> <span class="n">Bools</span><span class="p">(</span><span class="s">'a b c d e f g z'</span><span class="p">)</span>
<span class="k">def</span> <span class="nf">install_check</span><span class="p">(</span><span class="o">*</span><span class="n">problem</span><span class="p">):</span>
<span class="n">s</span> <span class="o">=</span> <span class="n">Solver</span><span class="p">()</span>
<span class="n">s</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="o">*</span><span class="n">problem</span><span class="p">)</span>
<span class="k">if</span> <span class="n">s</span><span class="o">.</span><span class="n">check</span><span class="p">()</span> <span class="o">==</span> <span class="n">sat</span><span class="p">:</span>
<span class="n">m</span> <span class="o">=</span> <span class="n">s</span><span class="o">.</span><span class="n">model</span><span class="p">()</span>
<span class="n">r</span> <span class="o">=</span> <span class="p">[]</span>
<span class="k">for</span> <span class="n">x</span> <span class="ow">in</span> <span class="n">m</span><span class="p">:</span>
<span class="k">if</span> <span class="n">is_true</span><span class="p">(</span><span class="n">m</span><span class="p">[</span><span class="n">x</span><span class="p">]):</span>
<span class="c"># x is a Z3 declaration</span>
<span class="c"># x() returns the Z3 expression</span>
<span class="c"># x.name() returns a string</span>
<span class="n">r</span><span class="o">.</span><span class="n">append</span><span class="p">(</span><span class="n">x</span><span class="p">())</span>
<span class="k">print</span> <span class="n">r</span>
<span class="k">else</span><span class="p">:</span>
<span class="k">print</span> <span class="s">"invalid installation profile"</span>
<span class="k">print</span> <span class="s">"Check 1"</span>
<span class="n">install_check</span><span class="p">(</span><span class="n">DependsOn</span><span class="p">(</span><span class="n">a</span><span class="p">,</span> <span class="p">[</span><span class="n">b</span><span class="p">,</span> <span class="n">c</span><span class="p">,</span> <span class="n">z</span><span class="p">]),</span>
<span class="n">DependsOn</span><span class="p">(</span><span class="n">b</span><span class="p">,</span> <span class="n">d</span><span class="p">),</span>
<span class="n">DependsOn</span><span class="p">(</span><span class="n">c</span><span class="p">,</span> <span class="p">[</span><span class="n">Or</span><span class="p">(</span><span class="n">d</span><span class="p">,</span> <span class="n">e</span><span class="p">),</span> <span class="n">Or</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)]),</span>
<span class="n">Conflict</span><span class="p">(</span><span class="n">d</span><span class="p">,</span> <span class="n">e</span><span class="p">),</span>
<span class="n">Conflict</span><span class="p">(</span><span class="n">d</span><span class="p">,</span> <span class="n">g</span><span class="p">),</span>
<span class="n">a</span><span class="p">,</span> <span class="n">z</span><span class="p">)</span>
<span class="k">print</span> <span class="s">"Check 2"</span>
<span class="n">install_check</span><span class="p">(</span><span class="n">DependsOn</span><span class="p">(</span><span class="n">a</span><span class="p">,</span> <span class="p">[</span><span class="n">b</span><span class="p">,</span> <span class="n">c</span><span class="p">,</span> <span class="n">z</span><span class="p">]),</span>
<span class="n">DependsOn</span><span class="p">(</span><span class="n">b</span><span class="p">,</span> <span class="n">d</span><span class="p">),</span>
<span class="n">DependsOn</span><span class="p">(</span><span class="n">c</span><span class="p">,</span> <span class="p">[</span><span class="n">Or</span><span class="p">(</span><span class="n">d</span><span class="p">,</span> <span class="n">e</span><span class="p">),</span> <span class="n">Or</span><span class="p">(</span><span class="n">f</span><span class="p">,</span> <span class="n">g</span><span class="p">)]),</span>
<span class="n">Conflict</span><span class="p">(</span><span class="n">d</span><span class="p">,</span> <span class="n">e</span><span class="p">),</span>
<span class="n">Conflict</span><span class="p">(</span><span class="n">d</span><span class="p">,</span> <span class="n">g</span><span class="p">),</span>
<span class="n">a</span><span class="p">,</span> <span class="n">z</span><span class="p">,</span> <span class="n">g</span><span class="p">)</span>
</pre></div>
</body></html></example>
<h2>Using Z3Py Locally</h2>
<p>Z3Py is part of the Z3 distribution. It is located in the <tt>python</tt> subdirectory.
To use it locally, you have to include the following command in your Python script.</p>
<pre>
from Z3 import *
</pre>
<p>
The Z3 Python frontend directory must be in your <tt>PYTHONPATH</tt> environment variable.
Z3Py will automatically search for the Z3 library (<tt>z3.dll</tt> (Windows), <tt>libz3.so</tt> (Linux), or <tt>libz3.dylib</tt> (OSX)).
You may also initialize Z3Py manually using the command:
</p>
<pre>
init("z3.dll")
</pre>
</body>
</html>
View git blame Copy permalink