mirror of
https://github.com/Z3Prover/z3
synced 2025-10-27 01:39:22 +00:00
861 lines
83 KiB
HTML
861 lines
83 KiB
HTML
<html>
|
|
<head>
|
|
<title>Z3Py Advanced</title>
|
|
<link rel="StyleSheet" href="style.css" type="text/css">
|
|
</head>
|
|
<body>
|
|
|
|
<h1>Advanced Topics</h1>
|
|
|
|
<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>Expressions, Sorts and Declarations</h2>
|
|
|
|
<p>In Z3, expressions, sorts and declarations are called <i>ASTs</i>.
|
|
ASTs are directed acyclic graphs. Every expression has a sort (aka type).
|
|
The method <tt>sort()</tt> retrieves the sort of an expression.
|
|
</p>
|
|
|
|
<example pref="expr.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">Real</span><span class="p">(</span><span class="s">'y'</span><span class="p">)</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="p">)</span><span class="o">.</span><span class="n">sort</span><span class="p">()</span>
|
|
<span class="k">print</span> <span class="p">(</span><span class="n">y</span> <span class="o">+</span> <span class="mi">1</span><span class="p">)</span><span class="o">.</span><span class="n">sort</span><span class="p">()</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">sort</span><span class="p">()</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>The function <tt>eq(n1, n2)</tt> returns <tt>True</tt> if <tt>n1</tt>
|
|
and <tt>n2</tt> are the same AST. This is a structural test.
|
|
</p>
|
|
|
|
<example pref="expr.2"><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">Ints</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">eq</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="n">x</span> <span class="o">+</span> <span class="n">y</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">eq</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="n">y</span> <span class="o">+</span> <span class="n">x</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="k">print</span> <span class="n">eq</span><span class="p">(</span><span class="n">n</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="c"># x2 is eq to x</span>
|
|
<span class="n">x2</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="k">print</span> <span class="n">eq</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">x2</span><span class="p">)</span>
|
|
<span class="c"># the integer variable x is not equal to </span>
|
|
<span class="c"># the real variable x</span>
|
|
<span class="k">print</span> <span class="n">eq</span><span class="p">(</span><span class="n">Int</span><span class="p">(</span><span class="s">'x'</span><span class="p">),</span> <span class="n">Real</span><span class="p">(</span><span class="s">'x'</span><span class="p">))</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>The method <tt>hash()</tt> returns a hashcode for an AST node.
|
|
If <tt>eq(n1, n2)</tt> returns <tt>True</tt>, then <tt>n1.hash()</tt>
|
|
is equal to <tt>n2.hash()</tt>.
|
|
</p>
|
|
|
|
<example pref="expr.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="k">print</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="n">hash</span><span class="p">()</span>
|
|
<span class="k">print</span> <span class="p">(</span><span class="mi">1</span> <span class="o">+</span> <span class="n">x</span><span class="p">)</span><span class="o">.</span><span class="n">hash</span><span class="p">()</span>
|
|
<span class="k">print</span> <span class="n">x</span><span class="o">.</span><span class="n">sort</span><span class="p">()</span><span class="o">.</span><span class="n">hash</span><span class="p">()</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>Z3 expressions can be divided in three basic groups: <b>applications</b>,
|
|
<b>quantifiers</b> and <b>bounded/free variables</b>.
|
|
Applications are all you need if your problems do not contain
|
|
universal/existential quantifiers. Although we say <tt>Int('x')</tt> is an
|
|
integer "variable", it is technically an integer constant, and internally
|
|
is represented as a function application with <tt>0</tt> arguments.
|
|
Every application is associated with a <b>declaration</b> and contains
|
|
<tt>0</tt> or more arguments. The method <tt>decl()</tt> returns
|
|
the declaration associated with an application. The method <tt>num_args()</tt>
|
|
returns the number of arguments of an application, and <tt>arg(i)</tt> one of the arguments.
|
|
The function <tt>is_expr(n)</tt> returns <tt>True</tt>
|
|
if <tt>n</tt> is an expression. Similarly <tt>is_app(n)</tt> (<tt>is_func_decl(n)</tt>)
|
|
returns <tt>True</tt> if <tt>n</tt> is an application (declaration).
|
|
</p>
|
|
|
|
<example pref="expr.4"><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="k">print</span> <span class="s">"is expression: "</span><span class="p">,</span> <span class="n">is_expr</span><span class="p">(</span><span class="n">x</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="mi">1</span>
|
|
<span class="k">print</span> <span class="s">"is application:"</span><span class="p">,</span> <span class="n">is_app</span><span class="p">(</span><span class="n">n</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="s">"decl: "</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">"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">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</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">"arg("</span><span class="p">,</span> <span class="n">i</span><span class="p">,</span> <span class="s">") ->"</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="n">i</span><span class="p">)</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>Declarations have names, they are retrieved using the method <tt>name()</tt>.
|
|
A (function) declaration has an arity, a domain and range sorts.
|
|
</p>
|
|
|
|
<example pref="expr.5"><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">x_d</span> <span class="o">=</span> <span class="n">x</span><span class="o">.</span><span class="n">decl</span><span class="p">()</span>
|
|
<span class="k">print</span> <span class="s">"is_expr(x_d): "</span><span class="p">,</span> <span class="n">is_expr</span><span class="p">(</span><span class="n">x_d</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="s">"is_func_decl(x_d):"</span><span class="p">,</span> <span class="n">is_func_decl</span><span class="p">(</span><span class="n">x_d</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="s">"x_d.name(): "</span><span class="p">,</span> <span class="n">x_d</span><span class="o">.</span><span class="n">name</span><span class="p">()</span>
|
|
<span class="k">print</span> <span class="s">"x_d.range(): "</span><span class="p">,</span> <span class="n">x_d</span><span class="o">.</span><span class="n">range</span><span class="p">()</span>
|
|
<span class="k">print</span> <span class="s">"x_d.arity(): "</span><span class="p">,</span> <span class="n">x_d</span><span class="o">.</span><span class="n">arity</span><span class="p">()</span>
|
|
<span class="c"># x_d() creates an application with 0 arguments using x_d.</span>
|
|
<span class="k">print</span> <span class="s">"eq(x_d(), x): "</span><span class="p">,</span> <span class="n">eq</span><span class="p">(</span><span class="n">x_d</span><span class="p">(),</span> <span class="n">x</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="s">"</span><span class="se">\n</span><span class="s">"</span>
|
|
<span class="c"># f is a function from (Int, Real) to Bool</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">RealSort</span><span class="p">(),</span> <span class="n">BoolSort</span><span class="p">())</span>
|
|
<span class="k">print</span> <span class="s">"f.name(): "</span><span class="p">,</span> <span class="n">f</span><span class="o">.</span><span class="n">name</span><span class="p">()</span>
|
|
<span class="k">print</span> <span class="s">"f.range(): "</span><span class="p">,</span> <span class="n">f</span><span class="o">.</span><span class="n">range</span><span class="p">()</span>
|
|
<span class="k">print</span> <span class="s">"f.arity(): "</span><span class="p">,</span> <span class="n">f</span><span class="o">.</span><span class="n">arity</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="n">f</span><span class="o">.</span><span class="n">arity</span><span class="p">()):</span>
|
|
<span class="k">print</span> <span class="s">"domain("</span><span class="p">,</span> <span class="n">i</span><span class="p">,</span> <span class="s">"): "</span><span class="p">,</span> <span class="n">f</span><span class="o">.</span><span class="n">domain</span><span class="p">(</span><span class="n">i</span><span class="p">)</span>
|
|
<span class="c"># f(x, x) creates an application with 2 arguments using f.</span>
|
|
<span class="k">print</span> <span class="n">f</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">x</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">eq</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="n">x</span><span class="p">)</span><span class="o">.</span><span class="n">decl</span><span class="p">(),</span> <span class="n">f</span><span class="p">)</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>
|
|
The built-in declarations are identified using their <b>kind</b>. The kind
|
|
is retrieved using the method <tt>kind()</tt>. The complete list of built-in declarations
|
|
can be found in the file <tt>z3consts.py</tt> (<tt>z3_api.h</tt>) in the Z3 distribution.
|
|
</p>
|
|
|
|
<example pref="expr.6"><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">Ints</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
|
|
<span class="k">print</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="n">decl</span><span class="p">()</span><span class="o">.</span><span class="n">kind</span><span class="p">()</span> <span class="o">==</span> <span class="n">Z3_OP_ADD</span>
|
|
<span class="k">print</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="n">decl</span><span class="p">()</span><span class="o">.</span><span class="n">kind</span><span class="p">()</span> <span class="o">==</span> <span class="n">Z3_OP_SUB</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>
|
|
The following example demonstrates how to substitute sub-expressions in Z3 expressions.
|
|
</p>
|
|
|
|
<example pref="expr.7"><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">Ints</span><span class="p">(</span><span class="s">'x 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">IntSort</span><span class="p">())</span>
|
|
<span class="n">g</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'g'</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">n</span> <span class="o">=</span> <span class="n">f</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">x</span><span class="p">),</span> <span class="n">g</span><span class="p">(</span><span class="n">g</span><span class="p">(</span><span class="n">x</span><span class="p">))),</span> <span class="n">g</span><span class="p">(</span><span class="n">g</span><span class="p">(</span><span class="n">y</span><span class="p">)))</span>
|
|
<span class="k">print</span> <span class="n">n</span>
|
|
<span class="c"># substitute g(g(x)) with y and g(y) with x + 1</span>
|
|
<span class="k">print</span> <span class="n">substitute</span><span class="p">(</span><span class="n">n</span><span class="p">,</span> <span class="p">(</span><span class="n">g</span><span class="p">(</span><span class="n">g</span><span class="p">(</span><span class="n">x</span><span class="p">)),</span> <span class="n">y</span><span class="p">),</span> <span class="p">(</span><span class="n">g</span><span class="p">(</span><span class="n">y</span><span class="p">),</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>
|
|
The function <tt>Const(name, sort)</tt> declares a constant (aka variable) of the given sort.
|
|
For example, the functions <tt>Int(name)</tt> and <tt>Real(name)</tt> are shorthands for
|
|
<tt>Const(name, IntSort())</tt> and <tt>Const(name, RealSort())</tt>.
|
|
</p>
|
|
|
|
<example pref="expr.8"><html><body>
|
|
<div class="highlight"><pre><span class="n">x</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'x'</span><span class="p">,</span> <span class="n">IntSort</span><span class="p">())</span>
|
|
<span class="k">print</span> <span class="n">eq</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">Int</span><span class="p">(</span><span class="s">'x'</span><span class="p">))</span>
|
|
|
|
<span class="n">a</span><span class="p">,</span> <span class="n">b</span> <span class="o">=</span> <span class="n">Consts</span><span class="p">(</span><span class="s">'a b'</span><span class="p">,</span> <span class="n">BoolSort</span><span class="p">())</span>
|
|
<span class="k">print</span> <span class="n">And</span><span class="p">(</span><span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">)</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<h2>Arrays</h2>
|
|
|
|
<p>As part of formulating a programme of a mathematical theory of computation
|
|
McCarthy proposed a <i>basic</i> theory of arrays as characterized by
|
|
the select-store axioms. The expression <tt>Select(a, i)</tt> returns
|
|
the value stored at position <tt>i</tt> of the array <tt>a</tt>;
|
|
and <tt>Store(a, i, v)</tt> returns a new array identical to <tt>a</tt>,
|
|
but on position <tt>i</tt> it contains the value <tt>v</tt>.
|
|
In Z3Py, we can also write <tt>Select(a, i)</tt> as <tt>a[i]</tt>.
|
|
</p>
|
|
|
|
<example pref="array.1"><html><body>
|
|
<div class="highlight"><pre><span class="c"># Use I as an alias for IntSort()</span>
|
|
<span class="n">I</span> <span class="o">=</span> <span class="n">IntSort</span><span class="p">()</span>
|
|
<span class="c"># A is an array from integer to integer</span>
|
|
<span class="n">A</span> <span class="o">=</span> <span class="n">Array</span><span class="p">(</span><span class="s">'A'</span><span class="p">,</span> <span class="n">I</span><span class="p">,</span> <span class="n">I</span><span class="p">)</span>
|
|
<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="k">print</span> <span class="n">A</span><span class="p">[</span><span class="n">x</span><span class="p">]</span>
|
|
<span class="k">print</span> <span class="n">Select</span><span class="p">(</span><span class="n">A</span><span class="p">,</span> <span class="n">x</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">Store</span><span class="p">(</span><span class="n">A</span><span class="p">,</span> <span class="n">x</span><span class="p">,</span> <span class="mi">10</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">Select</span><span class="p">(</span><span class="n">Store</span><span class="p">(</span><span class="n">A</span><span class="p">,</span> <span class="mi">2</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="mi">2</span><span class="p">))</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>
|
|
By default, Z3 assumes that arrays are extensional over select.
|
|
In other words, Z3 also enforces that if two arrays agree on all positions,
|
|
then the arrays are equal.
|
|
</p>
|
|
|
|
<p>
|
|
Z3 also contains various extensions
|
|
for operations on arrays that remain decidable and amenable
|
|
to efficient saturation procedures (here efficient means,
|
|
with an NP-complete satisfiability complexity).
|
|
We describe these extensions in the following using a collection of examples.
|
|
Additional background on these extensions is available in the
|
|
paper <a href="http://research.microsoft.com/en-us/um/people/leonardo/fmcad09.pdf" target="_blank">Generalized and Efficient Array Decision Procedures</a>.
|
|
</p>
|
|
|
|
<p>
|
|
Arrays in Z3 are used to model unbounded or very large arrays.
|
|
Arrays should not be used to model small finite collections of values.
|
|
It is usually much more efficient to create different variables using list comprehensions.
|
|
</p>
|
|
|
|
<example pref="array.2"><html><body>
|
|
<div class="highlight"><pre><span class="c"># We want an array with 3 elements.</span>
|
|
<span class="c"># 1. Bad solution</span>
|
|
<span class="n">X</span> <span class="o">=</span> <span class="n">Array</span><span class="p">(</span><span class="s">'x'</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="c"># Example using the array</span>
|
|
<span class="k">print</span> <span class="n">X</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">+</span> <span class="n">X</span><span class="p">[</span><span class="mi">1</span><span class="p">]</span> <span class="o">+</span> <span class="n">X</span><span class="p">[</span><span class="mi">2</span><span class="p">]</span> <span class="o">>=</span><span class="mi">0</span>
|
|
|
|
<span class="c"># 2. More efficient solution</span>
|
|
<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">3</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">X</span><span class="p">[</span><span class="mi">0</span><span class="p">]</span> <span class="o">+</span> <span class="n">X</span><span class="p">[</span><span class="mi">1</span><span class="p">]</span> <span class="o">+</span> <span class="n">X</span><span class="p">[</span><span class="mi">2</span><span class="p">]</span> <span class="o">>=</span> <span class="mi">0</span>
|
|
<span class="k">print</span> <span class="n">Sum</span><span class="p">(</span><span class="n">X</span><span class="p">)</span> <span class="o">>=</span> <span class="mi">0</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<h3>Select and Store</h3>
|
|
|
|
|
|
<p>Let us first check a basic property of arrays.
|
|
Suppose <tt>A</tt> is an array of integers, then the constraints
|
|
<tt>A[x] == x, Store(A, x, y) == A</tt>
|
|
are satisfiable for an array that contains an index <tt>x</tt> that maps to <tt>x</tt>,
|
|
and when <tt>x == y</tt>.
|
|
We can solve these constraints.
|
|
</p>
|
|
|
|
<example pref="array.3"><html><body>
|
|
<div class="highlight"><pre><span class="n">A</span> <span class="o">=</span> <span class="n">Array</span><span class="p">(</span><span class="s">'A'</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">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Ints</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">A</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">Store</span><span class="p">(</span><span class="n">A</span><span class="p">,</span> <span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">)</span> <span class="o">==</span> <span class="n">A</span><span class="p">)</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>The interpretation/solution for array variables is very similar to the one used for functions.</p>
|
|
|
|
<p>The problem becomes unsatisfiable/infeasible if we add the constraint <tt>x != y</tt>.
|
|
|
|
</p>
|
|
<example pref="array.4"><html><body>
|
|
<div class="highlight"><pre><span class="n">A</span> <span class="o">=</span> <span class="n">Array</span><span class="p">(</span><span class="s">'A'</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">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Ints</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">A</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">Store</span><span class="p">(</span><span class="n">A</span><span class="p">,</span> <span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">)</span> <span class="o">==</span> <span class="n">A</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>
|
|
|
|
<h3>Constant arrays</h3>
|
|
|
|
<p>
|
|
The array that maps all indices to some fixed value can be specified in Z3Py using the
|
|
<tt>K(s, v)</tt> construct where <tt>s</tt> is a sort/type and <tt>v</tt> is an expression.
|
|
<tt>K(s, v)</tt> returns a array that maps any value of <tt>s</tt> into <tt>v</tt>.
|
|
The following example defines a constant array containing only ones.
|
|
</p>
|
|
|
|
<example pref="array.5"><html><body>
|
|
<div class="highlight"><pre><span class="n">AllOne</span> <span class="o">=</span> <span class="n">K</span><span class="p">(</span><span class="n">IntSort</span><span class="p">(),</span> <span class="mi">1</span><span class="p">)</span>
|
|
<span class="n">a</span><span class="p">,</span> <span class="n">i</span> <span class="o">=</span> <span class="n">Ints</span><span class="p">(</span><span class="s">'a i'</span><span class="p">)</span>
|
|
<span class="n">solve</span><span class="p">(</span><span class="n">a</span> <span class="o">==</span> <span class="n">AllOne</span><span class="p">[</span><span class="n">i</span><span class="p">])</span>
|
|
<span class="c"># The following constraints do not have a solution</span>
|
|
<span class="n">solve</span><span class="p">(</span><span class="n">a</span> <span class="o">==</span> <span class="n">AllOne</span><span class="p">[</span><span class="n">i</span><span class="p">],</span> <span class="n">a</span> <span class="o">!=</span> <span class="mi">1</span><span class="p">)</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<h2>Datatypes</h2>
|
|
|
|
<p>Algebraic datatypes, known from programming languages such as ML,
|
|
offer a convenient way for specifying common data structures. Records
|
|
and tuples are special cases of algebraic datatypes, and so are
|
|
scalars (enumeration types). But algebraic datatypes are more
|
|
general. They can be used to specify finite lists, trees and other
|
|
recursive structures.</p>
|
|
|
|
<p>
|
|
The following example demonstrates how to declare a List in Z3Py. It is
|
|
more verbose than using the SMT 2.0 front-end, but much simpler than using
|
|
the Z3 C API. It consists of two phases.
|
|
First, we have to declare the new datatype, its constructors and accessors.
|
|
The function <tt>Datatype('List')</tt> declares a "placeholder" that will
|
|
contain the constructors and accessors declarations. The method
|
|
<tt>declare(cname, (aname, sort)+)</tt> declares a constructor named
|
|
<tt>cname</tt> with the given accessors. Each accessor has an associated <tt>sort</tt>
|
|
or a reference to the datatypes being declared.
|
|
For example, <tt>declare('cons', ('car', IntSort()), ('cdr', List))</tt>
|
|
declares the constructor named <tt>cons</tt> that builds a new <tt>List</tt>
|
|
using an integer and a <tt>List</tt>. It also declares the accessors <tt>car</tt> and
|
|
<tt>cdr</tt>. The accessor <tt>car</tt> extracts the integer of a <tt>cons</tt>
|
|
cell, and <tt>cdr</tt> the list of a <tt>cons</tt> cell.
|
|
After all constructors were declared, we use the method <tt>create()</tt> to
|
|
create the actual datatype in Z3. Z3Py makes the new Z3 declarations and constants
|
|
available as slots of the new object.
|
|
</p>
|
|
|
|
<example pref="datatype.1"><html><body>
|
|
<div class="highlight"><pre><span class="c"># Declare a List of integers</span>
|
|
<span class="n">List</span> <span class="o">=</span> <span class="n">Datatype</span><span class="p">(</span><span class="s">'List'</span><span class="p">)</span>
|
|
<span class="c"># Constructor cons: (Int, List) -> List</span>
|
|
<span class="n">List</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'cons'</span><span class="p">,</span> <span class="p">(</span><span class="s">'car'</span><span class="p">,</span> <span class="n">IntSort</span><span class="p">()),</span> <span class="p">(</span><span class="s">'cdr'</span><span class="p">,</span> <span class="n">List</span><span class="p">))</span>
|
|
<span class="c"># Constructor nil: List</span>
|
|
<span class="n">List</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'nil'</span><span class="p">)</span>
|
|
<span class="c"># Create the datatype</span>
|
|
<span class="n">List</span> <span class="o">=</span> <span class="n">List</span><span class="o">.</span><span class="n">create</span><span class="p">()</span>
|
|
<span class="k">print</span> <span class="n">is_sort</span><span class="p">(</span><span class="n">List</span><span class="p">)</span>
|
|
<span class="n">cons</span> <span class="o">=</span> <span class="n">List</span><span class="o">.</span><span class="n">cons</span>
|
|
<span class="n">car</span> <span class="o">=</span> <span class="n">List</span><span class="o">.</span><span class="n">car</span>
|
|
<span class="n">cdr</span> <span class="o">=</span> <span class="n">List</span><span class="o">.</span><span class="n">cdr</span>
|
|
<span class="n">nil</span> <span class="o">=</span> <span class="n">List</span><span class="o">.</span><span class="n">nil</span>
|
|
<span class="c"># cons, car and cdr are function declarations, and nil a constant</span>
|
|
<span class="k">print</span> <span class="n">is_func_decl</span><span class="p">(</span><span class="n">cons</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">is_expr</span><span class="p">(</span><span class="n">nil</span><span class="p">)</span>
|
|
|
|
<span class="n">l1</span> <span class="o">=</span> <span class="n">cons</span><span class="p">(</span><span class="mi">10</span><span class="p">,</span> <span class="n">cons</span><span class="p">(</span><span class="mi">20</span><span class="p">,</span> <span class="n">nil</span><span class="p">))</span>
|
|
<span class="k">print</span> <span class="n">l1</span>
|
|
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">cdr</span><span class="p">(</span><span class="n">l1</span><span class="p">))</span>
|
|
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">car</span><span class="p">(</span><span class="n">l1</span><span class="p">))</span>
|
|
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">l1</span> <span class="o">==</span> <span class="n">nil</span><span class="p">)</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>
|
|
The following example demonstrates how to define a Python function that
|
|
given a sort creates a list of the given sort.
|
|
</p>
|
|
|
|
<example pref="datatype.2"><html><body>
|
|
<div class="highlight"><pre><span class="k">def</span> <span class="nf">DeclareList</span><span class="p">(</span><span class="n">sort</span><span class="p">):</span>
|
|
<span class="n">List</span> <span class="o">=</span> <span class="n">Datatype</span><span class="p">(</span><span class="s">'List_of_</span><span class="si">%s</span><span class="s">'</span> <span class="o">%</span> <span class="n">sort</span><span class="o">.</span><span class="n">name</span><span class="p">())</span>
|
|
<span class="n">List</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'cons'</span><span class="p">,</span> <span class="p">(</span><span class="s">'car'</span><span class="p">,</span> <span class="n">sort</span><span class="p">),</span> <span class="p">(</span><span class="s">'cdr'</span><span class="p">,</span> <span class="n">List</span><span class="p">))</span>
|
|
<span class="n">List</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'nil'</span><span class="p">)</span>
|
|
<span class="k">return</span> <span class="n">List</span><span class="o">.</span><span class="n">create</span><span class="p">()</span>
|
|
|
|
<span class="n">IntList</span> <span class="o">=</span> <span class="n">DeclareList</span><span class="p">(</span><span class="n">IntSort</span><span class="p">())</span>
|
|
<span class="n">RealList</span> <span class="o">=</span> <span class="n">DeclareList</span><span class="p">(</span><span class="n">RealSort</span><span class="p">())</span>
|
|
<span class="n">IntListList</span> <span class="o">=</span> <span class="n">DeclareList</span><span class="p">(</span><span class="n">IntList</span><span class="p">)</span>
|
|
|
|
<span class="n">l1</span> <span class="o">=</span> <span class="n">IntList</span><span class="o">.</span><span class="n">cons</span><span class="p">(</span><span class="mi">10</span><span class="p">,</span> <span class="n">IntList</span><span class="o">.</span><span class="n">nil</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">l1</span>
|
|
<span class="k">print</span> <span class="n">IntListList</span><span class="o">.</span><span class="n">cons</span><span class="p">(</span><span class="n">l1</span><span class="p">,</span> <span class="n">IntListList</span><span class="o">.</span><span class="n">cons</span><span class="p">(</span><span class="n">l1</span><span class="p">,</span> <span class="n">IntListList</span><span class="o">.</span><span class="n">nil</span><span class="p">))</span>
|
|
<span class="k">print</span> <span class="n">RealList</span><span class="o">.</span><span class="n">cons</span><span class="p">(</span><span class="s">"1/3"</span><span class="p">,</span> <span class="n">RealList</span><span class="o">.</span><span class="n">nil</span><span class="p">)</span>
|
|
|
|
<span class="k">print</span> <span class="n">l1</span><span class="o">.</span><span class="n">sort</span><span class="p">()</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>The example above demonstrates that Z3 supports operator overloading.
|
|
There are several functions named <tt>cons</tt>, but they are different since they receive and/or
|
|
return values of different sorts.
|
|
Note that it is not necessary to use a different sort name for each instance of the sort
|
|
list. That is, the expression <tt>'List_of_%s' % sort.name()</tt> is not necessary, we
|
|
use it just to provide more meaningful names.
|
|
</p>
|
|
|
|
<p>
|
|
As described above enumeration types are a special case of algebraic datatypes.
|
|
The following example declares an enumeration type consisting of three values:
|
|
<tt>red</tt>, <tt>green</tt> and <tt>blue</tt>.
|
|
</p>
|
|
|
|
<example pref="datatype.3"><html><body>
|
|
<div class="highlight"><pre><span class="n">Color</span> <span class="o">=</span> <span class="n">Datatype</span><span class="p">(</span><span class="s">'Color'</span><span class="p">)</span>
|
|
<span class="n">Color</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'red'</span><span class="p">)</span>
|
|
<span class="n">Color</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'green'</span><span class="p">)</span>
|
|
<span class="n">Color</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'blue'</span><span class="p">)</span>
|
|
<span class="n">Color</span> <span class="o">=</span> <span class="n">Color</span><span class="o">.</span><span class="n">create</span><span class="p">()</span>
|
|
|
|
<span class="k">print</span> <span class="n">is_expr</span><span class="p">(</span><span class="n">Color</span><span class="o">.</span><span class="n">green</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">Color</span><span class="o">.</span><span class="n">green</span> <span class="o">==</span> <span class="n">Color</span><span class="o">.</span><span class="n">blue</span>
|
|
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">Color</span><span class="o">.</span><span class="n">green</span> <span class="o">==</span> <span class="n">Color</span><span class="o">.</span><span class="n">blue</span><span class="p">)</span>
|
|
|
|
<span class="c"># Let c be a constant of sort Color</span>
|
|
<span class="n">c</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'c'</span><span class="p">,</span> <span class="n">Color</span><span class="p">)</span>
|
|
<span class="c"># Then, c must be red, green or blue</span>
|
|
<span class="n">prove</span><span class="p">(</span><span class="n">Or</span><span class="p">(</span><span class="n">c</span> <span class="o">==</span> <span class="n">Color</span><span class="o">.</span><span class="n">green</span><span class="p">,</span>
|
|
<span class="n">c</span> <span class="o">==</span> <span class="n">Color</span><span class="o">.</span><span class="n">blue</span><span class="p">,</span>
|
|
<span class="n">c</span> <span class="o">==</span> <span class="n">Color</span><span class="o">.</span><span class="n">red</span><span class="p">))</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>
|
|
Z3Py also provides the following shorthand for declaring enumeration sorts.
|
|
</p>
|
|
|
|
<example pref="datatype.4"><html><body>
|
|
<div class="highlight"><pre><span class="n">Color</span><span class="p">,</span> <span class="p">(</span><span class="n">red</span><span class="p">,</span> <span class="n">green</span><span class="p">,</span> <span class="n">blue</span><span class="p">)</span> <span class="o">=</span> <span class="n">EnumSort</span><span class="p">(</span><span class="s">'Color'</span><span class="p">,</span> <span class="p">(</span><span class="s">'red'</span><span class="p">,</span> <span class="s">'green'</span><span class="p">,</span> <span class="s">'blue'</span><span class="p">))</span>
|
|
|
|
<span class="k">print</span> <span class="n">green</span> <span class="o">==</span> <span class="n">blue</span>
|
|
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">green</span> <span class="o">==</span> <span class="n">blue</span><span class="p">)</span>
|
|
|
|
<span class="n">c</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'c'</span><span class="p">,</span> <span class="n">Color</span><span class="p">)</span>
|
|
<span class="n">solve</span><span class="p">(</span><span class="n">c</span> <span class="o">!=</span> <span class="n">green</span><span class="p">,</span> <span class="n">c</span> <span class="o">!=</span> <span class="n">blue</span><span class="p">)</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>
|
|
Mutually recursive datatypes can also be declared. The only difference is that we use
|
|
the function <tt>CreateDatatypes</tt> instead of the method <tt>create()</tt> to create
|
|
the mutually recursive datatypes.
|
|
</p>
|
|
|
|
<example pref="datatype.5"><html><body>
|
|
<div class="highlight"><pre><span class="n">TreeList</span> <span class="o">=</span> <span class="n">Datatype</span><span class="p">(</span><span class="s">'TreeList'</span><span class="p">)</span>
|
|
<span class="n">Tree</span> <span class="o">=</span> <span class="n">Datatype</span><span class="p">(</span><span class="s">'Tree'</span><span class="p">)</span>
|
|
<span class="n">Tree</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'leaf'</span><span class="p">,</span> <span class="p">(</span><span class="s">'val'</span><span class="p">,</span> <span class="n">IntSort</span><span class="p">()))</span>
|
|
<span class="n">Tree</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'node'</span><span class="p">,</span> <span class="p">(</span><span class="s">'left'</span><span class="p">,</span> <span class="n">TreeList</span><span class="p">),</span> <span class="p">(</span><span class="s">'right'</span><span class="p">,</span> <span class="n">TreeList</span><span class="p">))</span>
|
|
<span class="n">TreeList</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'nil'</span><span class="p">)</span>
|
|
<span class="n">TreeList</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'cons'</span><span class="p">,</span> <span class="p">(</span><span class="s">'car'</span><span class="p">,</span> <span class="n">Tree</span><span class="p">),</span> <span class="p">(</span><span class="s">'cdr'</span><span class="p">,</span> <span class="n">TreeList</span><span class="p">))</span>
|
|
|
|
<span class="n">Tree</span><span class="p">,</span> <span class="n">TreeList</span> <span class="o">=</span> <span class="n">CreateDatatypes</span><span class="p">(</span><span class="n">Tree</span><span class="p">,</span> <span class="n">TreeList</span><span class="p">)</span>
|
|
|
|
<span class="n">t1</span> <span class="o">=</span> <span class="n">Tree</span><span class="o">.</span><span class="n">leaf</span><span class="p">(</span><span class="mi">10</span><span class="p">)</span>
|
|
<span class="n">tl1</span> <span class="o">=</span> <span class="n">TreeList</span><span class="o">.</span><span class="n">cons</span><span class="p">(</span><span class="n">t1</span><span class="p">,</span> <span class="n">TreeList</span><span class="o">.</span><span class="n">nil</span><span class="p">)</span>
|
|
<span class="n">t2</span> <span class="o">=</span> <span class="n">Tree</span><span class="o">.</span><span class="n">node</span><span class="p">(</span><span class="n">tl1</span><span class="p">,</span> <span class="n">TreeList</span><span class="o">.</span><span class="n">nil</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">t2</span>
|
|
<span class="k">print</span> <span class="n">simplify</span><span class="p">(</span><span class="n">Tree</span><span class="o">.</span><span class="n">val</span><span class="p">(</span><span class="n">t1</span><span class="p">))</span>
|
|
|
|
<span class="n">t1</span><span class="p">,</span> <span class="n">t2</span><span class="p">,</span> <span class="n">t3</span> <span class="o">=</span> <span class="n">Consts</span><span class="p">(</span><span class="s">'t1 t2 t3'</span><span class="p">,</span> <span class="n">TreeList</span><span class="p">)</span>
|
|
|
|
<span class="n">solve</span><span class="p">(</span><span class="n">Distinct</span><span class="p">(</span><span class="n">t1</span><span class="p">,</span> <span class="n">t2</span><span class="p">,</span> <span class="n">t3</span><span class="p">))</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<h2>Uninterpreted Sorts</h2>
|
|
|
|
<p>
|
|
Function and constant symbols in pure first-order logic are uninterpreted or free,
|
|
which means that no a priori interpretation is attached.
|
|
This is in contrast to arithmetic operators such as <tt>+</tt> and <tt>-</tt>
|
|
that have a fixed standard interpretation.
|
|
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 introduce an (uninterpreted) sort <tt>A</tt>,
|
|
and the constants <tt>x</tt>, <tt>y</tt> ranging over <tt>A</tt>.
|
|
Finally let <tt>f</tt> be an uninterpreted function that takes one
|
|
argument of sort <tt>A</tt> and results in a value of sort <tt>A</tt>.
|
|
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="uninterp.1"><html><body>
|
|
<div class="highlight"><pre><span class="n">A</span> <span class="o">=</span> <span class="n">DeclareSort</span><span class="p">(</span><span class="s">'A'</span><span class="p">)</span>
|
|
<span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Consts</span><span class="p">(</span><span class="s">'x y'</span><span class="p">,</span> <span class="n">A</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">A</span><span class="p">,</span> <span class="n">A</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="n">m</span>
|
|
<span class="k">print</span> <span class="s">"interpretation assigned to A:"</span>
|
|
<span class="k">print</span> <span class="n">m</span><span class="p">[</span><span class="n">A</span><span class="p">]</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>
|
|
The resulting model introduces abstract values for the elements in <tt>A</tt>,
|
|
because the sort <tt>A</tt> is uninterpreted. The interpretation for <tt>f</tt> in the
|
|
model toggles between the two values for <tt>x</tt> and <tt>y</tt>, which are different.
|
|
The expression <tt>m[A]</tt> returns the interpretation (universe) for the uninterpreted sort <tt>A</tt>
|
|
in the model <tt>m</tt>.
|
|
</p>
|
|
|
|
<h2>Quantifiers</h2>
|
|
|
|
<p>
|
|
Z3 is can solve quantifier-free problems containing arithmetic, bit-vector, Booleans,
|
|
arrays, functions and datatypes. Z3 also accepts and can work with formulas
|
|
that use quantifiers. It is no longer a decision procedure for
|
|
such formulas in general (and for good reasons, as there can be
|
|
no decision procedure for first-order logic).
|
|
</p>
|
|
|
|
<example pref="quant.1"><html><body>
|
|
<div class="highlight"><pre><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">IntSort</span><span class="p">())</span>
|
|
<span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Ints</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">ForAll</span><span class="p">([</span><span class="n">x</span><span class="p">,</span> <span class="n">y</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="n">y</span><span class="p">)</span> <span class="o">==</span> <span class="mi">0</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">Exists</span><span class="p">(</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="n">x</span><span class="p">)</span> <span class="o">>=</span> <span class="mi">0</span><span class="p">)</span>
|
|
|
|
<span class="n">a</span><span class="p">,</span> <span class="n">b</span> <span class="o">=</span> <span class="n">Ints</span><span class="p">(</span><span class="s">'a b'</span><span class="p">)</span>
|
|
<span class="n">solve</span><span class="p">(</span><span class="n">ForAll</span><span class="p">(</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="n">x</span><span class="p">)</span> <span class="o">==</span> <span class="mi">0</span><span class="p">),</span> <span class="n">f</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="o">==</span> <span class="mi">1</span><span class="p">)</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>
|
|
Nevertheless, Z3 is often able to handle formulas involving
|
|
quantifiers. It uses several approaches to handle quantifiers.
|
|
The most prolific approach is using <i>pattern-based</i> quantifier
|
|
instantiation. This approach allows instantiating quantified formulas
|
|
with ground terms that appear in the current search context based
|
|
on <i>pattern annotations</i> on quantifiers.
|
|
Z3 also contains a model-based quantifier instantiation
|
|
component that uses a model construction to find good terms to instantiate
|
|
quantifiers with; and Z3 also handles many decidable fragments.
|
|
</p>
|
|
|
|
<p>Note that in the previous example the constants <tt>x</tt>
|
|
and <tt>y</tt> were used to create quantified formulas.
|
|
This is a "trick" for simplifying the construction of quantified
|
|
formulas in Z3Py. Internally, these constants are replaced by
|
|
bounded variables. The next example demonstrates that. The method
|
|
<tt>body()</tt> retrieves the quantified expression.
|
|
In the resultant formula the bounded variables are free.
|
|
The function <tt>Var(index, sort)</tt> creates a bounded/free variable
|
|
with the given index and sort.
|
|
</p>
|
|
|
|
<example pref="quant.2"><html><body>
|
|
<div class="highlight"><pre><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">IntSort</span><span class="p">())</span>
|
|
<span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Ints</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
|
|
<span class="n">f</span> <span class="o">=</span> <span class="n">ForAll</span><span class="p">([</span><span class="n">x</span><span class="p">,</span> <span class="n">y</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="n">y</span><span class="p">)</span> <span class="o">==</span> <span class="mi">0</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">f</span><span class="o">.</span><span class="n">body</span><span class="p">()</span>
|
|
<span class="n">v1</span> <span class="o">=</span> <span class="n">f</span><span class="o">.</span><span class="n">body</span><span class="p">()</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="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="n">v1</span>
|
|
<span class="k">print</span> <span class="n">eq</span><span class="p">(</span><span class="n">v1</span><span class="p">,</span> <span class="n">Var</span><span class="p">(</span><span class="mi">1</span><span class="p">,</span> <span class="n">IntSort</span><span class="p">()))</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<h3>Modeling with Quantifiers</h3>
|
|
|
|
<p>
|
|
Suppose we want to model an object oriented type system with single inheritance.
|
|
We would need a predicate for sub-typing. Sub-typing should be a partial order,
|
|
and respect single inheritance. For some built-in type constructors,
|
|
such as for <tt>array_of</tt>, sub-typing should be monotone.
|
|
</p>
|
|
|
|
<example pref="quant.3"><html><body>
|
|
<div class="highlight"><pre><span class="n">Type</span> <span class="o">=</span> <span class="n">DeclareSort</span><span class="p">(</span><span class="s">'Type'</span><span class="p">)</span>
|
|
<span class="n">subtype</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'subtype'</span><span class="p">,</span> <span class="n">Type</span><span class="p">,</span> <span class="n">Type</span><span class="p">,</span> <span class="n">BoolSort</span><span class="p">())</span>
|
|
<span class="n">array_of</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'array_of'</span><span class="p">,</span> <span class="n">Type</span><span class="p">,</span> <span class="n">Type</span><span class="p">)</span>
|
|
<span class="n">root</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'root'</span><span class="p">,</span> <span class="n">Type</span><span class="p">)</span>
|
|
|
|
<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">Consts</span><span class="p">(</span><span class="s">'x y z'</span><span class="p">,</span> <span class="n">Type</span><span class="p">)</span>
|
|
|
|
<span class="n">axioms</span> <span class="o">=</span> <span class="p">[</span> <span class="n">ForAll</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">subtype</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">x</span><span class="p">)),</span>
|
|
<span class="n">ForAll</span><span class="p">([</span><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="p">],</span> <span class="n">Implies</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">subtype</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">),</span> <span class="n">subtype</span><span class="p">(</span><span class="n">y</span><span class="p">,</span> <span class="n">z</span><span class="p">)),</span>
|
|
<span class="n">subtype</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">z</span><span class="p">))),</span>
|
|
<span class="n">ForAll</span><span class="p">([</span><span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">],</span> <span class="n">Implies</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">subtype</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">),</span> <span class="n">subtype</span><span class="p">(</span><span class="n">y</span><span class="p">,</span> <span class="n">x</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="n">ForAll</span><span class="p">([</span><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="p">],</span> <span class="n">Implies</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">subtype</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">),</span> <span class="n">subtype</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">z</span><span class="p">)),</span>
|
|
<span class="n">Or</span><span class="p">(</span><span class="n">subtype</span><span class="p">(</span><span class="n">y</span><span class="p">,</span> <span class="n">z</span><span class="p">),</span> <span class="n">subtype</span><span class="p">(</span><span class="n">z</span><span class="p">,</span> <span class="n">y</span><span class="p">)))),</span>
|
|
<span class="n">ForAll</span><span class="p">([</span><span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">],</span> <span class="n">Implies</span><span class="p">(</span><span class="n">subtype</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">),</span>
|
|
<span class="n">subtype</span><span class="p">(</span><span class="n">array_of</span><span class="p">(</span><span class="n">x</span><span class="p">),</span> <span class="n">array_of</span><span class="p">(</span><span class="n">y</span><span class="p">)))),</span>
|
|
|
|
<span class="n">ForAll</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">subtype</span><span class="p">(</span><span class="n">root</span><span class="p">,</span> <span class="n">x</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">axioms</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">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">"Interpretation for Type:"</span>
|
|
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">model</span><span class="p">()[</span><span class="n">Type</span><span class="p">]</span>
|
|
<span class="k">print</span> <span class="s">"Model:"</span>
|
|
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">model</span><span class="p">()</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<h3>Patterns</h3>
|
|
|
|
<p>
|
|
The Stanford Pascal verifier and the subsequent Simplify theorem prover pioneered
|
|
the use of pattern-based quantifier instantiation.
|
|
The basic idea behind pattern-based quantifier instantiation is in a sense straight-forward:
|
|
Annotate a quantified formula using a pattern that contains all the bound variables.
|
|
So a pattern is an expression (that does not contain binding operations, such as quantifiers)
|
|
that contains variables bound by a quantifier. Then instantiate the quantifier whenever a term
|
|
that matches the pattern is created during search. This is a conceptually easy starting point,
|
|
but there are several subtleties that are important.
|
|
</p>
|
|
|
|
<p>
|
|
In the following example, the first two options make sure that Model-based quantifier instantiation engine is disabled.
|
|
We also annotate the quantified formula with the pattern <tt>f(g(x))</tt>.
|
|
Since there is no ground instance of this pattern, the quantifier is not instantiated, and
|
|
Z3 fails to show that the formula is unsatisfiable.
|
|
</p>
|
|
|
|
<example pref="quant.4"><html><body>
|
|
<div class="highlight"><pre><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">g</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'g'</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">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">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">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">set</span><span class="p">(</span><span class="n">auto_config</span><span class="o">=</span><span class="bp">False</span><span class="p">,</span> <span class="n">mbqi</span><span class="o">=</span><span class="bp">False</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">ForAll</span><span class="p">(</span><span class="n">x</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">x</span><span class="p">))</span> <span class="o">==</span> <span class="n">x</span><span class="p">,</span> <span class="n">patterns</span> <span class="o">=</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">x</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="o">==</span> <span class="n">c</span><span class="p">,</span>
|
|
<span class="n">g</span><span class="p">(</span><span class="n">b</span><span class="p">)</span> <span class="o">==</span> <span class="n">c</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="c"># Display solver state using internal format</span>
|
|
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">sexpr</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>When the more permissive pattern <tt>g(x)</tt> is used. Z3 proves the formula
|
|
to be unsatisfiable. More restrictive patterns minimize the number of
|
|
instantiations (and potentially improve performance), but they may
|
|
also make Z3 "less complete".
|
|
</p>
|
|
|
|
<example pref="quant.5"><html><body>
|
|
<div class="highlight"><pre><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">g</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'g'</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">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">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">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">set</span><span class="p">(</span><span class="n">auto_config</span><span class="o">=</span><span class="bp">False</span><span class="p">,</span> <span class="n">mbqi</span><span class="o">=</span><span class="bp">False</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">ForAll</span><span class="p">(</span><span class="n">x</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">x</span><span class="p">))</span> <span class="o">==</span> <span class="n">x</span><span class="p">,</span> <span class="n">patterns</span> <span class="o">=</span> <span class="p">[</span><span class="n">g</span><span class="p">(</span><span class="n">x</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="o">==</span> <span class="n">c</span><span class="p">,</span>
|
|
<span class="n">g</span><span class="p">(</span><span class="n">b</span><span class="p">)</span> <span class="o">==</span> <span class="n">c</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="c"># Display solver state using internal format</span>
|
|
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">sexpr</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>
|
|
Some patterns may also create long instantiation chains. Consider the following assertion.
|
|
</p>
|
|
|
|
<pre>
|
|
ForAll([x, y], Implies(subtype(x, y),
|
|
subtype(array_of(x), array_of(y))),
|
|
patterns=[subtype(x, y)])
|
|
</pre>
|
|
|
|
<p>
|
|
The axiom gets instantiated whenever there is some ground term of the
|
|
form <tt>subtype(s, t)</tt>. The instantiation causes a fresh ground term
|
|
<tt>subtype(array_of(s), array_of(t))</tt>, which enables a new
|
|
instantiation. This undesirable situation is called a matching
|
|
loop. Z3 uses many heuristics to break matching loops.
|
|
</p>
|
|
|
|
<p>
|
|
Before elaborating on the subtleties, we should address an important
|
|
first question. What defines the terms that are created during search?
|
|
In the context of most SMT solvers, and of the Simplify theorem
|
|
prover, terms exist as part of the input formula, they are of course
|
|
also created by instantiating quantifiers, but terms are also
|
|
implicitly created when equalities are asserted. The last point means
|
|
that terms are considered up to congruence and pattern matching takes
|
|
place modulo ground equalities. We call the matching problem
|
|
<b>E-matching</b>. For example, if we have the following equalities:
|
|
</p>
|
|
|
|
<example pref="quant.6"><html><body>
|
|
<div class="highlight"><pre><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">g</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'g'</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">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">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">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">set</span><span class="p">(</span><span class="n">auto_config</span><span class="o">=</span><span class="bp">False</span><span class="p">,</span> <span class="n">mbqi</span><span class="o">=</span><span class="bp">False</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">ForAll</span><span class="p">(</span><span class="n">x</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">x</span><span class="p">))</span> <span class="o">==</span> <span class="n">x</span><span class="p">,</span> <span class="n">patterns</span> <span class="o">=</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">x</span><span class="p">))]),</span>
|
|
<span class="n">a</span> <span class="o">==</span> <span class="n">g</span><span class="p">(</span><span class="n">b</span><span class="p">),</span>
|
|
<span class="n">b</span> <span class="o">==</span> <span class="n">c</span><span class="p">,</span>
|
|
<span class="n">f</span><span class="p">(</span><span class="n">a</span><span class="p">)</span> <span class="o">!=</span> <span class="n">c</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 terms <tt>f(a)</tt> and <tt>f(g(b))</tt> are equal modulo the
|
|
equalities. The pattern <tt>f(g(x))</tt> can be matched and <tt>x</tt> bound to <tt>b</tt>
|
|
and the equality <tt>f(g(b)) == b</tt> is deduced.
|
|
</p>
|
|
|
|
<p>
|
|
While E-matching is an NP-complete problem, the main sources of overhead in larger verification
|
|
problems comes from matching thousands of patterns in the context of an evolving set of terms and
|
|
equalities. Z3 integrates an efficient E-matching engine using term indexing techniques.
|
|
</p>
|
|
|
|
<h3>Multi-patterns</h3>
|
|
|
|
<p>
|
|
In some cases, there is no pattern that contains all bound variables
|
|
and does not contain interpreted symbols. In these cases, we use
|
|
multi-patterns. In the following example, the quantified formula
|
|
states that <tt>f</tt> is injective. This quantified formula is annotated with
|
|
the multi-pattern <tt>MultiPattern(f(x), f(y))</tt>.
|
|
</p>
|
|
|
|
<example pref="quant.7"><html><body>
|
|
<div class="highlight"><pre><span class="n">A</span> <span class="o">=</span> <span class="n">DeclareSort</span><span class="p">(</span><span class="s">'A'</span><span class="p">)</span>
|
|
<span class="n">B</span> <span class="o">=</span> <span class="n">DeclareSort</span><span class="p">(</span><span class="s">'B'</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">A</span><span class="p">,</span> <span class="n">B</span><span class="p">)</span>
|
|
<span class="n">a1</span><span class="p">,</span> <span class="n">a2</span> <span class="o">=</span> <span class="n">Consts</span><span class="p">(</span><span class="s">'a1 a2'</span><span class="p">,</span> <span class="n">A</span><span class="p">)</span>
|
|
<span class="n">b</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'b'</span><span class="p">,</span> <span class="n">B</span><span class="p">)</span>
|
|
<span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Consts</span><span class="p">(</span><span class="s">'x y'</span><span class="p">,</span> <span class="n">A</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">a1</span> <span class="o">!=</span> <span class="n">a2</span><span class="p">,</span>
|
|
<span class="n">f</span><span class="p">(</span><span class="n">a1</span><span class="p">)</span> <span class="o">==</span> <span class="n">b</span><span class="p">,</span>
|
|
<span class="n">f</span><span class="p">(</span><span class="n">a2</span><span class="p">)</span> <span class="o">==</span> <span class="n">b</span><span class="p">,</span>
|
|
<span class="n">ForAll</span><span class="p">([</span><span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">],</span> <span class="n">Implies</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">f</span><span class="p">(</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="n">patterns</span><span class="o">=</span><span class="p">[</span><span class="n">MultiPattern</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="n">f</span><span class="p">(</span><span class="n">y</span><span class="p">))])</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 quantified formula is instantiated for every pair of occurrences
|
|
of <tt>f</tt>. A simple trick allows formulating injectivity of <tt>f</tt> in such a way
|
|
that only a linear number of instantiations is required. The trick is
|
|
to realize that <tt>f</tt> is injective if and only if it has a partial
|
|
inverse.
|
|
</p>
|
|
|
|
<example pref="quant.8"><html><body>
|
|
<div class="highlight"><pre><span class="n">A</span> <span class="o">=</span> <span class="n">DeclareSort</span><span class="p">(</span><span class="s">'A'</span><span class="p">)</span>
|
|
<span class="n">B</span> <span class="o">=</span> <span class="n">DeclareSort</span><span class="p">(</span><span class="s">'B'</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">A</span><span class="p">,</span> <span class="n">B</span><span class="p">)</span>
|
|
<span class="n">finv</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'finv'</span><span class="p">,</span> <span class="n">B</span><span class="p">,</span> <span class="n">A</span><span class="p">)</span>
|
|
<span class="n">a1</span><span class="p">,</span> <span class="n">a2</span> <span class="o">=</span> <span class="n">Consts</span><span class="p">(</span><span class="s">'a1 a2'</span><span class="p">,</span> <span class="n">A</span><span class="p">)</span>
|
|
<span class="n">b</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'b'</span><span class="p">,</span> <span class="n">B</span><span class="p">)</span>
|
|
<span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Consts</span><span class="p">(</span><span class="s">'x y'</span><span class="p">,</span> <span class="n">A</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">a1</span> <span class="o">!=</span> <span class="n">a2</span><span class="p">,</span>
|
|
<span class="n">f</span><span class="p">(</span><span class="n">a1</span><span class="p">)</span> <span class="o">==</span> <span class="n">b</span><span class="p">,</span>
|
|
<span class="n">f</span><span class="p">(</span><span class="n">a2</span><span class="p">)</span> <span class="o">==</span> <span class="n">b</span><span class="p">,</span>
|
|
<span class="n">ForAll</span><span class="p">(</span><span class="n">x</span><span class="p">,</span> <span class="n">finv</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="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>
|
|
|
|
<h3>Other attributes</h3>
|
|
|
|
<p>
|
|
In Z3Py, the following additional attributes are supported: <b>qid</b> (quantifier identifier
|
|
for debugging), <b>weight</b> (hint to the quantifier instantiation module: "more weight equals less instances"),
|
|
<b>no_patterns</b> (expressions that should not be used as patterns, <b>skid</b> (identifier
|
|
prefix used to create skolem constants/functions.
|
|
</p>
|
|
|
|
<h2>Multiple Solvers</h2>
|
|
|
|
<p>In Z3Py and Z3 4.0 multiple solvers can be simultaneously used.
|
|
It is also very easy to copy assertions/formulas from one solver to another.
|
|
</p>
|
|
|
|
<example pref="msolver.1"><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">Ints</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
|
|
<span class="n">s1</span> <span class="o">=</span> <span class="n">Solver</span><span class="p">()</span>
|
|
<span class="n">s1</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="n">x</span> <span class="o">></span> <span class="mi">10</span><span class="p">,</span> <span class="n">y</span> <span class="o">></span> <span class="mi">10</span><span class="p">)</span>
|
|
<span class="n">s2</span> <span class="o">=</span> <span class="n">Solver</span><span class="p">()</span>
|
|
<span class="c"># solver s2 is empty</span>
|
|
<span class="k">print</span> <span class="n">s2</span>
|
|
<span class="c"># copy assertions from s1 to s2</span>
|
|
<span class="n">s2</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="n">s1</span><span class="o">.</span><span class="n">assertions</span><span class="p">())</span>
|
|
<span class="k">print</span> <span class="n">s2</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<h2>Unsat Cores and Soft Constraints</h2>
|
|
|
|
<p>Z3Py also supports <i>unsat core extraction</i>. The basic idea is to use
|
|
<i>assumptions</i>, that is, auxiliary propositional variables that we want to track.
|
|
Assumptions are also available in the Z3 SMT 2.0 frontend, and in other Z3 front-ends.
|
|
They are used to extract unsatisfiable cores. They may be also used to "retract"
|
|
constraints. Note that, assumptions are not really <i>soft constraints</i>, but they can be used to implement them.
|
|
</p>
|
|
|
|
<example pref="unsatcore.1"><html><body>
|
|
<div class="highlight"><pre><span class="n">p1</span><span class="p">,</span> <span class="n">p2</span><span class="p">,</span> <span class="n">p3</span> <span class="o">=</span> <span class="n">Bools</span><span class="p">(</span><span class="s">'p1 p2 p3'</span><span class="p">)</span>
|
|
<span class="n">x</span><span class="p">,</span> <span class="n">y</span> <span class="o">=</span> <span class="n">Ints</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
|
|
<span class="c"># We assert Implies(p, C) to track constraint C using 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">Implies</span><span class="p">(</span><span class="n">p1</span><span class="p">,</span> <span class="n">x</span> <span class="o">></span> <span class="mi">10</span><span class="p">),</span>
|
|
<span class="n">Implies</span><span class="p">(</span><span class="n">p1</span><span class="p">,</span> <span class="n">y</span> <span class="o">></span> <span class="n">x</span><span class="p">),</span>
|
|
<span class="n">Implies</span><span class="p">(</span><span class="n">p2</span><span class="p">,</span> <span class="n">y</span> <span class="o"><</span> <span class="mi">5</span><span class="p">),</span>
|
|
<span class="n">Implies</span><span class="p">(</span><span class="n">p3</span><span class="p">,</span> <span class="n">y</span> <span class="o">></span> <span class="mi">0</span><span class="p">))</span>
|
|
<span class="k">print</span> <span class="n">s</span>
|
|
<span class="c"># Check satisfiability assuming p1, p2, p3 are true</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">p1</span><span class="p">,</span> <span class="n">p2</span><span class="p">,</span> <span class="n">p3</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">unsat_core</span><span class="p">()</span>
|
|
|
|
<span class="c"># Try again retracting p2</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">p1</span><span class="p">,</span> <span class="n">p3</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">model</span><span class="p">()</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>The example above also shows that a Boolean variable (<tt>p1</tt>) can be used to track
|
|
more than one constraint. Note that Z3 does not guarantee that the unsat cores are minimal.
|
|
</p>
|
|
|
|
<h2>Formatter</h2>
|
|
|
|
<p>
|
|
Z3Py uses a formatter (aka pretty printer) for displaying formulas, expressions, solvers, and other
|
|
Z3 objects. The formatter supports many configuration options.
|
|
The command <tt>set_option(html_mode=False)</tt> makes all formulas and expressions to be
|
|
displayed in Z3Py notation.
|
|
</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">>=</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">>=</span> <span class="mi">1</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
<p>By default, Z3Py will truncate the output if the object being displayed is too big.
|
|
Z3Py uses … to denote the output is truncated.
|
|
The following configuration options can be set to control the behavior of Z3Py's formatter:
|
|
</p>
|
|
|
|
<ul>
|
|
<li> <tt>max_depth</tt> Maximal expression depth. Deep expressions are replaced with …. </li>
|
|
<li> <tt>max_args</tt> Maximal number of arguments to display per node. </li>
|
|
<li> <tt>rational_to_decimal</tt> Display rationals as decimals if True. </li>
|
|
<li> <tt>precision</tt> Maximal number of decimal places for numbers being displayed in decimal notation. </li>
|
|
<li> <tt>max_lines</tt> Maximal number of lines to be displayed. </li>
|
|
<li> <tt>max_width</tt> Maximal line width (this is a suggestion to Z3Py). </li>
|
|
<li> <tt>max_indent</tt> Maximal indentation.</li>
|
|
</ul>
|
|
|
|
<example pref="format"><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">20</span><span class="p">)</span>
|
|
<span class="n">y</span> <span class="o">=</span> <span class="n">IntVector</span><span class="p">(</span><span class="s">'y'</span><span class="p">,</span> <span class="mi">20</span><span class="p">)</span>
|
|
<span class="n">f</span> <span class="o">=</span> <span class="n">And</span><span class="p">(</span><span class="n">Sum</span><span class="p">(</span><span class="n">x</span><span class="p">)</span> <span class="o">>=</span> <span class="mi">0</span><span class="p">,</span> <span class="n">Sum</span><span class="p">(</span><span class="n">y</span><span class="p">)</span> <span class="o">>=</span> <span class="mi">0</span><span class="p">)</span>
|
|
|
|
<span class="n">set_option</span><span class="p">(</span><span class="n">max_args</span><span class="o">=</span><span class="mi">5</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="s">"</span><span class="se">\n</span><span class="s">test 1:"</span>
|
|
<span class="k">print</span> <span class="n">f</span>
|
|
|
|
<span class="k">print</span> <span class="s">"</span><span class="se">\n</span><span class="s">test 2:"</span>
|
|
<span class="n">set_option</span><span class="p">(</span><span class="n">max_args</span><span class="o">=</span><span class="mi">100</span><span class="p">,</span> <span class="n">max_lines</span><span class="o">=</span><span class="mi">10</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">f</span>
|
|
|
|
<span class="k">print</span> <span class="s">"</span><span class="se">\n</span><span class="s">test 3:"</span>
|
|
<span class="n">set_option</span><span class="p">(</span><span class="n">max_width</span><span class="o">=</span><span class="mi">300</span><span class="p">)</span>
|
|
<span class="k">print</span> <span class="n">f</span>
|
|
</pre></div>
|
|
</body></html></example>
|
|
|
|
</body>
|
|
</html>
|