mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
html pages for z3 python tutorial
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
165c0ef3e1
commit
e0a49dd556
861
examples/python/tutorial/html/advanced-examples.htm
Normal file
861
examples/python/tutorial/html/advanced-examples.htm
Normal file
|
|
@ -0,0 +1,861 @@
|
|||
<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> retrives 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 restrive 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>
|
||||
651
examples/python/tutorial/html/fixpoint-examples.htm
Normal file
651
examples/python/tutorial/html/fixpoint-examples.htm
Normal file
|
|
@ -0,0 +1,651 @@
|
|||
<html>
|
||||
<head>
|
||||
<title>Z3Py Fixedpoints</title>
|
||||
<link rel="StyleSheet" href="style.css" type="text/css">
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<h1>Fixedpoints</h1>
|
||||
|
||||
<p>
|
||||
</p>
|
||||
|
||||
<p>
|
||||
This tutorial illustrates uses of Z3's fixedpoint engine.
|
||||
The following papers
|
||||
<a href="http://research.microsoft.com/en-us/people/nbjorner/z3fix.pdf">
|
||||
μZ - An Efficient Engine for Fixed-Points with Constraints.</a>
|
||||
(CAV 2011) and
|
||||
<a href="http://research.microsoft.com/en-us/people/nbjorner/z3pdr.pdf">
|
||||
Generalized Property Directed Reachability</a> (SAT 2012)
|
||||
describe some of the main features of the engine.
|
||||
</p>
|
||||
|
||||
<p>
|
||||
Please send feedback, comments and/or corrections to
|
||||
<a href="mailto:nbjorner@microsoft.com">nbjorner@microsoft.com</a>.
|
||||
</p>
|
||||
|
||||
<h2>Introduction</h2>
|
||||
|
||||
|
||||
<p>
|
||||
This tutorial covers some of the fixedpoint utilities available with Z3.
|
||||
The main features are a basic Datalog engine, an engine with relational
|
||||
algebra and an engine based on a generalization of the Property
|
||||
Directed Reachability algorithm.
|
||||
</p>
|
||||
|
||||
|
||||
<h2>Basic Datalog </h2>
|
||||
|
||||
<p>The default fixed-point engine is a bottom-up Datalog engine.
|
||||
It works with finite relations and uses finite table representations
|
||||
as hash tables as the default way to represent finite relations.
|
||||
</p>
|
||||
|
||||
<h3>Relations, rules and queries</h3>
|
||||
|
||||
The first example illustrates how to declare relations, rules and
|
||||
how to pose queries.
|
||||
|
||||
<example pref="fixedpoint.1"><html><body>
|
||||
<div class="highlight"><pre><span class="n">fp</span> <span class="o">=</span> <span class="n">Fixedpoint</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">Bools</span><span class="p">(</span><span class="s">'a b c'</span><span class="p">)</span>
|
||||
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">register_relation</span><span class="p">(</span><span class="n">a</span><span class="o">.</span><span class="n">decl</span><span class="p">(),</span> <span class="n">b</span><span class="o">.</span><span class="n">decl</span><span class="p">(),</span> <span class="n">c</span><span class="o">.</span><span class="n">decl</span><span class="p">())</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">rule</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">fp</span><span class="o">.</span><span class="n">rule</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">fp</span><span class="o">.</span><span class="n">set</span><span class="p">(</span><span class="n">engine</span><span class="o">=</span><span class="s">'datalog'</span><span class="p">)</span>
|
||||
|
||||
<span class="k">print</span> <span class="s">"current set of rules</span><span class="se">\n</span><span class="s">"</span><span class="p">,</span> <span class="n">fp</span>
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">a</span><span class="p">)</span>
|
||||
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">fact</span><span class="p">(</span><span class="n">c</span><span class="p">)</span>
|
||||
<span class="k">print</span> <span class="s">"updated set of rules</span><span class="se">\n</span><span class="s">"</span><span class="p">,</span> <span class="n">fp</span>
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">a</span><span class="p">)</span>
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">get_answer</span><span class="p">()</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
The example illustrates some of the basic constructs.
|
||||
<pre>
|
||||
fp = Fixedpoint()
|
||||
</pre>
|
||||
creates a context for fixed-point computation.
|
||||
<pre>
|
||||
fp.register_relation(a.decl(), b.decl(), c.decl())
|
||||
</pre>
|
||||
Register the relations <tt>a, b, c</tt> as recursively defined.
|
||||
<pre>
|
||||
fp.rule(a,b)
|
||||
</pre>
|
||||
Create the rule that <tt>a</tt> follows from <tt>b</tt>.
|
||||
In general you can create a rule with multiple premises and a name using
|
||||
the format
|
||||
<pre>
|
||||
fp.rule(<em>head</em>,[<em>body1,...,bodyN</em>],<em>name</em>)
|
||||
</pre>
|
||||
The <em>name</em> is optional. It is used for tracking the rule in derivation proofs.
|
||||
|
||||
Continuing with the example, <tt>a</tt> is false unless <tt>b</tt> is established.
|
||||
<pre>
|
||||
fp.query(a)
|
||||
</pre>
|
||||
Asks if <tt>a</tt> can be derived. The rules so far say that <tt>a</tt>
|
||||
follows if <tt>b</tt> is established and that <tt>b</tt> follows if <tt>c</tt>
|
||||
is established. But nothing establishes <tt>c</tt> and <tt>b</tt> is also not
|
||||
established, so <tt>a</tt> cannot be derived.
|
||||
<pre>
|
||||
fp.fact(c)
|
||||
</pre>
|
||||
Add a fact (shorthand for <tt>fp.rule(c,True)</tt>).
|
||||
Now it is the case that <tt>a</tt> can be derived.
|
||||
|
||||
<h3>Explanations</h3>
|
||||
<p>
|
||||
It is also possible to get an explanation for a derived query.
|
||||
For the finite Datalog engine, an explanation is a trace that
|
||||
provides information of how a fact was derived. The explanation
|
||||
is an expression whose function symbols are Horn rules and facts used
|
||||
in the derivation.
|
||||
</p>
|
||||
<example pref="fixedpoint.2"><html><body>
|
||||
<div class="highlight"><pre><span class="n">fp</span> <span class="o">=</span> <span class="n">Fixedpoint</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">Bools</span><span class="p">(</span><span class="s">'a b c'</span><span class="p">)</span>
|
||||
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">register_relation</span><span class="p">(</span><span class="n">a</span><span class="o">.</span><span class="n">decl</span><span class="p">(),</span> <span class="n">b</span><span class="o">.</span><span class="n">decl</span><span class="p">(),</span> <span class="n">c</span><span class="o">.</span><span class="n">decl</span><span class="p">())</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">rule</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">fp</span><span class="o">.</span><span class="n">rule</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">fp</span><span class="o">.</span><span class="n">fact</span><span class="p">(</span><span class="n">c</span><span class="p">)</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">set</span><span class="p">(</span><span class="n">generate_explanations</span><span class="o">=</span><span class="bp">True</span><span class="p">,</span> <span class="n">engine</span><span class="o">=</span><span class="s">'datalog'</span><span class="p">)</span>
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">a</span><span class="p">)</span>
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">get_answer</span><span class="p">()</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<h3>Relations with arguments</h3>
|
||||
<p>
|
||||
Relations can take arguments. We illustrate relations with arguments
|
||||
using edges and paths in a graph.
|
||||
</p>
|
||||
<example pref="fixedpoint.3"><html><body>
|
||||
<div class="highlight"><pre><span class="n">fp</span> <span class="o">=</span> <span class="n">Fixedpoint</span><span class="p">()</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">set</span><span class="p">(</span><span class="n">engine</span><span class="o">=</span><span class="s">'datalog'</span><span class="p">)</span>
|
||||
|
||||
<span class="n">s</span> <span class="o">=</span> <span class="n">BitVecSort</span><span class="p">(</span><span class="mi">3</span><span class="p">)</span>
|
||||
<span class="n">edge</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'edge'</span><span class="p">,</span> <span class="n">s</span><span class="p">,</span> <span class="n">s</span><span class="p">,</span> <span class="n">BoolSort</span><span class="p">())</span>
|
||||
<span class="n">path</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'path'</span><span class="p">,</span> <span class="n">s</span><span class="p">,</span> <span class="n">s</span><span class="p">,</span> <span class="n">BoolSort</span><span class="p">())</span>
|
||||
<span class="n">a</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'a'</span><span class="p">,</span><span class="n">s</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">s</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">s</span><span class="p">)</span>
|
||||
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">register_relation</span><span class="p">(</span><span class="n">path</span><span class="p">,</span><span class="n">edge</span><span class="p">)</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">declare_var</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">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">path</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">edge</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">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">path</span><span class="p">(</span><span class="n">a</span><span class="p">,</span><span class="n">c</span><span class="p">),</span> <span class="p">[</span><span class="n">edge</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">path</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">v1</span> <span class="o">=</span> <span class="n">BitVecVal</span><span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="n">s</span><span class="p">)</span>
|
||||
<span class="n">v2</span> <span class="o">=</span> <span class="n">BitVecVal</span><span class="p">(</span><span class="mi">2</span><span class="p">,</span><span class="n">s</span><span class="p">)</span>
|
||||
<span class="n">v3</span> <span class="o">=</span> <span class="n">BitVecVal</span><span class="p">(</span><span class="mi">3</span><span class="p">,</span><span class="n">s</span><span class="p">)</span>
|
||||
<span class="n">v4</span> <span class="o">=</span> <span class="n">BitVecVal</span><span class="p">(</span><span class="mi">4</span><span class="p">,</span><span class="n">s</span><span class="p">)</span>
|
||||
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">fact</span><span class="p">(</span><span class="n">edge</span><span class="p">(</span><span class="n">v1</span><span class="p">,</span><span class="n">v2</span><span class="p">))</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">fact</span><span class="p">(</span><span class="n">edge</span><span class="p">(</span><span class="n">v1</span><span class="p">,</span><span class="n">v3</span><span class="p">))</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">fact</span><span class="p">(</span><span class="n">edge</span><span class="p">(</span><span class="n">v2</span><span class="p">,</span><span class="n">v4</span><span class="p">))</span>
|
||||
|
||||
<span class="k">print</span> <span class="s">"current set of rules"</span><span class="p">,</span> <span class="n">fp</span>
|
||||
|
||||
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">path</span><span class="p">(</span><span class="n">v1</span><span class="p">,</span><span class="n">v4</span><span class="p">)),</span> <span class="s">"yes we can reach v4 from v1"</span>
|
||||
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">path</span><span class="p">(</span><span class="n">v3</span><span class="p">,</span><span class="n">v4</span><span class="p">)),</span> <span class="s">"no we cannot reach v4 from v3"</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
The example uses the declaration
|
||||
<pre>
|
||||
fp.declare_var(a,b,c)
|
||||
</pre>
|
||||
to instrument the fixed-point engine that <tt>a, b, c</tt>
|
||||
should be treated as variables
|
||||
when they appear in rules. Think of the convention as they way bound variables are
|
||||
passed to quantifiers in Z3Py.
|
||||
|
||||
<h3>Rush Hour</h3>
|
||||
<p>
|
||||
A more entertaining example of using the basic fixed point engine
|
||||
is to solve the Rush Hour puzzle. The puzzle is about moving
|
||||
a red car out of a gridlock. We have encoded a configuration
|
||||
and compiled a set of rules that encode the legal moves of the cars
|
||||
given the configuration. Other configurations can be tested by
|
||||
changing the parameters passed to the constructor for <t>Car</t>.
|
||||
We have encoded the configuration from
|
||||
<a href="http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40" target="_top">
|
||||
an online puzzle you can solve manually, or cheat on by asking Z3</a>.
|
||||
</p>
|
||||
<example pref="fixedpoint.4"><html><body>
|
||||
<div class="highlight"><pre><span class="k">class</span> <span class="nc">Car</span><span class="p">():</span>
|
||||
<span class="k">def</span> <span class="nf">__init__</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">is_vertical</span><span class="p">,</span> <span class="n">base_pos</span><span class="p">,</span> <span class="n">length</span><span class="p">,</span> <span class="n">start</span><span class="p">,</span> <span class="n">color</span><span class="p">):</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">is_vertical</span> <span class="o">=</span> <span class="n">is_vertical</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">base</span> <span class="o">=</span> <span class="n">base_pos</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">length</span> <span class="o">=</span> <span class="n">length</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">start</span> <span class="o">=</span> <span class="n">start</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">color</span> <span class="o">=</span> <span class="n">color</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">__eq__</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">other</span><span class="p">):</span>
|
||||
<span class="k">return</span> <span class="bp">self</span><span class="o">.</span><span class="n">color</span> <span class="o">==</span> <span class="n">other</span><span class="o">.</span><span class="n">color</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">__ne__</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">other</span><span class="p">):</span>
|
||||
<span class="k">return</span> <span class="bp">self</span><span class="o">.</span><span class="n">color</span> <span class="o">!=</span> <span class="n">other</span><span class="o">.</span><span class="n">color</span>
|
||||
|
||||
<span class="n">dimension</span> <span class="o">=</span> <span class="mi">6</span>
|
||||
|
||||
<span class="n">red_car</span> <span class="o">=</span> <span class="n">Car</span><span class="p">(</span><span class="bp">False</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">3</span><span class="p">,</span> <span class="s">"red"</span><span class="p">)</span>
|
||||
<span class="n">cars</span> <span class="o">=</span> <span class="p">[</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">True</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="s">'yellow'</span><span class="p">),</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">False</span><span class="p">,</span> <span class="mi">3</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="s">'blue'</span><span class="p">),</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">False</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="s">"brown"</span><span class="p">),</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">False</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">1</span><span class="p">,</span> <span class="s">"lgreen"</span><span class="p">),</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">True</span><span class="p">,</span> <span class="mi">1</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">1</span><span class="p">,</span> <span class="s">"light blue"</span><span class="p">),</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">True</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">1</span><span class="p">,</span> <span class="s">"pink"</span><span class="p">),</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">True</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">4</span><span class="p">,</span> <span class="s">"dark green"</span><span class="p">),</span>
|
||||
<span class="n">red_car</span><span class="p">,</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">True</span><span class="p">,</span> <span class="mi">3</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">3</span><span class="p">,</span> <span class="s">"purple"</span><span class="p">),</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">False</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">3</span><span class="p">,</span> <span class="s">"light yellow"</span><span class="p">),</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">True</span><span class="p">,</span> <span class="mi">4</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="s">"orange"</span><span class="p">),</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">False</span><span class="p">,</span> <span class="mi">4</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">4</span><span class="p">,</span> <span class="s">"black"</span><span class="p">),</span>
|
||||
<span class="n">Car</span><span class="p">(</span><span class="bp">True</span><span class="p">,</span> <span class="mi">5</span><span class="p">,</span> <span class="mi">3</span><span class="p">,</span> <span class="mi">1</span><span class="p">,</span> <span class="s">"light purple"</span><span class="p">)</span>
|
||||
<span class="p">]</span>
|
||||
|
||||
<span class="n">num_cars</span> <span class="o">=</span> <span class="nb">len</span><span class="p">(</span><span class="n">cars</span><span class="p">)</span>
|
||||
<span class="n">B</span> <span class="o">=</span> <span class="n">BoolSort</span><span class="p">()</span>
|
||||
<span class="n">bv3</span> <span class="o">=</span> <span class="n">BitVecSort</span><span class="p">(</span><span class="mi">3</span><span class="p">)</span>
|
||||
|
||||
|
||||
<span class="n">state</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'state'</span><span class="p">,</span> <span class="p">[</span> <span class="n">bv3</span> <span class="k">for</span> <span class="n">c</span> <span class="ow">in</span> <span class="n">cars</span><span class="p">]</span> <span class="o">+</span> <span class="p">[</span><span class="n">B</span><span class="p">])</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">num</span><span class="p">(</span><span class="n">i</span><span class="p">):</span>
|
||||
<span class="k">return</span> <span class="n">BitVecVal</span><span class="p">(</span><span class="n">i</span><span class="p">,</span><span class="n">bv3</span><span class="p">)</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">bound</span><span class="p">(</span><span class="n">i</span><span class="p">):</span>
|
||||
<span class="k">return</span> <span class="n">Const</span><span class="p">(</span><span class="n">cars</span><span class="p">[</span><span class="n">i</span><span class="p">]</span><span class="o">.</span><span class="n">color</span><span class="p">,</span> <span class="n">bv3</span><span class="p">)</span>
|
||||
|
||||
<span class="n">fp</span> <span class="o">=</span> <span class="n">Fixedpoint</span><span class="p">()</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">set</span><span class="p">(</span><span class="n">generate_explanations</span><span class="o">=</span><span class="bp">True</span><span class="p">)</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">declare_var</span><span class="p">([</span><span class="n">bound</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="n">num_cars</span><span class="p">)])</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">register_relation</span><span class="p">(</span><span class="n">state</span><span class="p">)</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">mk_state</span><span class="p">(</span><span class="n">car</span><span class="p">,</span> <span class="n">value</span><span class="p">):</span>
|
||||
<span class="k">return</span> <span class="n">state</span><span class="p">([</span> <span class="p">(</span><span class="n">num</span><span class="p">(</span><span class="n">value</span><span class="p">)</span> <span class="k">if</span> <span class="p">(</span><span class="n">cars</span><span class="p">[</span><span class="n">i</span><span class="p">]</span> <span class="o">==</span> <span class="n">car</span><span class="p">)</span> <span class="k">else</span> <span class="n">bound</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="n">num_cars</span><span class="p">)])</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">mk_transition</span><span class="p">(</span><span class="n">row</span><span class="p">,</span> <span class="n">col</span><span class="p">,</span> <span class="n">i0</span><span class="p">,</span> <span class="n">j</span><span class="p">,</span> <span class="n">car0</span><span class="p">):</span>
|
||||
<span class="n">body</span> <span class="o">=</span> <span class="p">[</span><span class="n">mk_state</span><span class="p">(</span><span class="n">car0</span><span class="p">,</span> <span class="n">i0</span><span class="p">)]</span>
|
||||
<span class="k">for</span> <span class="n">index</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="n">num_cars</span><span class="p">):</span>
|
||||
<span class="n">car</span> <span class="o">=</span> <span class="n">cars</span><span class="p">[</span><span class="n">index</span><span class="p">]</span>
|
||||
<span class="k">if</span> <span class="n">car0</span> <span class="o">!=</span> <span class="n">car</span><span class="p">:</span>
|
||||
<span class="k">if</span> <span class="n">car</span><span class="o">.</span><span class="n">is_vertical</span> <span class="ow">and</span> <span class="n">car</span><span class="o">.</span><span class="n">base</span> <span class="o">==</span> <span class="n">col</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">dimension</span><span class="p">):</span>
|
||||
<span class="k">if</span> <span class="n">i</span> <span class="o"><=</span> <span class="n">row</span> <span class="ow">and</span> <span class="n">row</span> <span class="o"><</span> <span class="n">i</span> <span class="o">+</span> <span class="n">car</span><span class="o">.</span><span class="n">length</span> <span class="ow">and</span> <span class="n">i</span> <span class="o">+</span> <span class="n">car</span><span class="o">.</span><span class="n">length</span> <span class="o"><=</span> <span class="n">dimension</span><span class="p">:</span>
|
||||
<span class="n">body</span> <span class="o">+=</span> <span class="p">[</span><span class="n">bound</span><span class="p">(</span><span class="n">index</span><span class="p">)</span> <span class="o">!=</span> <span class="n">num</span><span class="p">(</span><span class="n">i</span><span class="p">)]</span>
|
||||
<span class="k">if</span> <span class="n">car</span><span class="o">.</span><span class="n">base</span> <span class="o">==</span> <span class="n">row</span> <span class="ow">and</span> <span class="ow">not</span> <span class="n">car</span><span class="o">.</span><span class="n">is_vertical</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">dimension</span><span class="p">):</span>
|
||||
<span class="k">if</span> <span class="n">i</span> <span class="o"><=</span> <span class="n">col</span> <span class="ow">and</span> <span class="n">col</span> <span class="o"><</span> <span class="n">i</span> <span class="o">+</span> <span class="n">car</span><span class="o">.</span><span class="n">length</span> <span class="ow">and</span> <span class="n">i</span> <span class="o">+</span> <span class="n">car</span><span class="o">.</span><span class="n">length</span> <span class="o"><=</span> <span class="n">dimension</span><span class="p">:</span>
|
||||
<span class="n">body</span> <span class="o">+=</span> <span class="p">[</span><span class="n">bound</span><span class="p">(</span><span class="n">index</span><span class="p">)</span> <span class="o">!=</span> <span class="n">num</span><span class="p">(</span><span class="n">i</span><span class="p">)]</span>
|
||||
|
||||
<span class="n">s</span> <span class="o">=</span> <span class="s">"</span><span class="si">%s</span><span class="s"> </span><span class="si">%d</span><span class="s">-></span><span class="si">%d</span><span class="s">"</span> <span class="o">%</span> <span class="p">(</span><span class="n">car0</span><span class="o">.</span><span class="n">color</span><span class="p">,</span> <span class="n">i0</span><span class="p">,</span> <span class="n">j</span><span class="p">)</span>
|
||||
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">mk_state</span><span class="p">(</span><span class="n">car0</span><span class="p">,</span> <span class="n">j</span><span class="p">),</span> <span class="n">body</span><span class="p">,</span> <span class="n">s</span><span class="p">)</span>
|
||||
|
||||
|
||||
<span class="k">def</span> <span class="nf">move_down</span><span class="p">(</span><span class="n">i</span><span class="p">,</span> <span class="n">car</span><span class="p">):</span>
|
||||
<span class="n">free_row</span> <span class="o">=</span> <span class="n">i</span> <span class="o">+</span> <span class="n">car</span><span class="o">.</span><span class="n">length</span>
|
||||
<span class="k">if</span> <span class="n">free_row</span> <span class="o"><</span> <span class="n">dimension</span><span class="p">:</span>
|
||||
<span class="n">mk_transition</span><span class="p">(</span><span class="n">free_row</span><span class="p">,</span> <span class="n">car</span><span class="o">.</span><span class="n">base</span><span class="p">,</span> <span class="n">i</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">car</span><span class="p">)</span>
|
||||
|
||||
|
||||
<span class="k">def</span> <span class="nf">move_up</span><span class="p">(</span><span class="n">i</span><span class="p">,</span> <span class="n">car</span><span class="p">):</span>
|
||||
<span class="n">free_row</span> <span class="o">=</span> <span class="n">i</span> <span class="o">-</span> <span class="mi">1</span>
|
||||
<span class="k">if</span> <span class="mi">0</span> <span class="o"><=</span> <span class="n">free_row</span> <span class="ow">and</span> <span class="n">i</span> <span class="o">+</span> <span class="n">car</span><span class="o">.</span><span class="n">length</span> <span class="o"><=</span> <span class="n">dimension</span><span class="p">:</span>
|
||||
<span class="n">mk_transition</span><span class="p">(</span><span class="n">free_row</span><span class="p">,</span> <span class="n">car</span><span class="o">.</span><span class="n">base</span><span class="p">,</span> <span class="n">i</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">car</span><span class="p">)</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">move_left</span><span class="p">(</span><span class="n">i</span><span class="p">,</span> <span class="n">car</span><span class="p">):</span>
|
||||
<span class="n">free_col</span> <span class="o">=</span> <span class="n">i</span> <span class="o">-</span> <span class="mi">1</span><span class="p">;</span>
|
||||
<span class="k">if</span> <span class="mi">0</span> <span class="o"><=</span> <span class="n">free_col</span> <span class="ow">and</span> <span class="n">i</span> <span class="o">+</span> <span class="n">car</span><span class="o">.</span><span class="n">length</span> <span class="o"><=</span> <span class="n">dimension</span><span class="p">:</span>
|
||||
<span class="n">mk_transition</span><span class="p">(</span><span class="n">car</span><span class="o">.</span><span class="n">base</span><span class="p">,</span> <span class="n">free_col</span><span class="p">,</span> <span class="n">i</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">car</span><span class="p">)</span>
|
||||
|
||||
|
||||
<span class="k">def</span> <span class="nf">move_right</span><span class="p">(</span><span class="n">i</span><span class="p">,</span> <span class="n">car</span><span class="p">):</span>
|
||||
<span class="n">free_col</span> <span class="o">=</span> <span class="n">car</span><span class="o">.</span><span class="n">length</span> <span class="o">+</span> <span class="n">i</span>
|
||||
<span class="k">if</span> <span class="n">free_col</span> <span class="o"><</span> <span class="n">dimension</span><span class="p">:</span>
|
||||
<span class="n">mk_transition</span><span class="p">(</span><span class="n">car</span><span class="o">.</span><span class="n">base</span><span class="p">,</span> <span class="n">free_col</span><span class="p">,</span> <span class="n">i</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">car</span><span class="p">)</span>
|
||||
|
||||
|
||||
<span class="c"># Initial state:</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">fact</span><span class="p">(</span><span class="n">state</span><span class="p">([</span><span class="n">num</span><span class="p">(</span><span class="n">cars</span><span class="p">[</span><span class="n">i</span><span class="p">]</span><span class="o">.</span><span class="n">start</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">num_cars</span><span class="p">)]))</span>
|
||||
|
||||
<span class="c"># Transitions:</span>
|
||||
<span class="k">for</span> <span class="n">car</span> <span class="ow">in</span> <span class="n">cars</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">dimension</span><span class="p">):</span>
|
||||
<span class="k">if</span> <span class="n">car</span><span class="o">.</span><span class="n">is_vertical</span><span class="p">:</span>
|
||||
<span class="n">move_down</span><span class="p">(</span><span class="n">i</span><span class="p">,</span> <span class="n">car</span><span class="p">)</span>
|
||||
<span class="n">move_up</span><span class="p">(</span><span class="n">i</span><span class="p">,</span> <span class="n">car</span><span class="p">)</span>
|
||||
<span class="k">else</span><span class="p">:</span>
|
||||
<span class="n">move_left</span><span class="p">(</span><span class="n">i</span><span class="p">,</span> <span class="n">car</span><span class="p">)</span>
|
||||
<span class="n">move_right</span><span class="p">(</span><span class="n">i</span><span class="p">,</span> <span class="n">car</span><span class="p">)</span>
|
||||
|
||||
|
||||
<span class="k">def</span> <span class="nf">get_instructions</span><span class="p">(</span><span class="n">ans</span><span class="p">):</span>
|
||||
<span class="n">lastAnd</span> <span class="o">=</span> <span class="n">ans</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">children</span><span class="p">()[</span><span class="o">-</span><span class="mi">1</span><span class="p">]</span>
|
||||
<span class="n">trace</span> <span class="o">=</span> <span class="n">lastAnd</span><span class="o">.</span><span class="n">children</span><span class="p">()[</span><span class="mi">1</span><span class="p">]</span>
|
||||
<span class="k">while</span> <span class="n">trace</span><span class="o">.</span><span class="n">num_args</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">trace</span><span class="o">.</span><span class="n">decl</span><span class="p">()</span>
|
||||
<span class="n">trace</span> <span class="o">=</span> <span class="n">trace</span><span class="o">.</span><span class="n">children</span><span class="p">()[</span><span class="o">-</span><span class="mi">1</span><span class="p">]</span>
|
||||
|
||||
<span class="k">print</span> <span class="n">fp</span>
|
||||
|
||||
<span class="n">goal</span> <span class="o">=</span> <span class="n">state</span><span class="p">([</span> <span class="p">(</span><span class="n">num</span><span class="p">(</span><span class="mi">4</span><span class="p">)</span> <span class="k">if</span> <span class="n">cars</span><span class="p">[</span><span class="n">i</span><span class="p">]</span> <span class="o">==</span> <span class="n">red_car</span> <span class="k">else</span> <span class="n">bound</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="n">num_cars</span><span class="p">)])</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">goal</span><span class="p">)</span>
|
||||
|
||||
<span class="n">get_instructions</span><span class="p">(</span><span class="n">fp</span><span class="o">.</span><span class="n">get_answer</span><span class="p">())</span>
|
||||
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
|
||||
<h2>Abstract Domains</h2>
|
||||
The underlying engine uses table operations
|
||||
that are based on relational algebra. Representations are
|
||||
opaque to the underlying engine.
|
||||
Relational algebra operations are well defined for arbitrary relations.
|
||||
They don't depend on whether the relations denote a finite or an
|
||||
infinite set of values.
|
||||
Z3 contains two built-in tables for infinite domains.
|
||||
The first is for intervals of integers and reals.
|
||||
The second is for bound constraints between two integers or reals.
|
||||
A bound constraint is of the form <tt>x or <tt> x .
|
||||
When used in conjunction, they form
|
||||
an abstract domain that is called the
|
||||
<a href="http://www.sciencedirect.com/science/article/pii/S0167642309000719">
|
||||
<em>Pentagon</em></a> abstract
|
||||
domain. Z3 implements <em>reduced products</em>
|
||||
of abstract domains that enables sharing constraints between
|
||||
the interval and bounds domains.
|
||||
|
||||
</tt></tt><p>
|
||||
Below we give a simple example that illustrates a loop at location <tt>l0</tt>.
|
||||
The loop is incremented as long as the loop counter does not exceed an upper
|
||||
bound. Using the combination of bound and interval domains
|
||||
we can collect derived invariants from the loop and we can also establish
|
||||
that the state after the loop does not exceed the bound.
|
||||
</p>
|
||||
|
||||
|
||||
<example pref="fixedpoint.5"><html><body>
|
||||
<div class="highlight"><pre><span class="n">I</span> <span class="o">=</span> <span class="n">IntSort</span><span class="p">()</span>
|
||||
<span class="n">B</span> <span class="o">=</span> <span class="n">BoolSort</span><span class="p">()</span>
|
||||
<span class="n">l0</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'l0'</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">B</span><span class="p">)</span>
|
||||
<span class="n">l1</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'l1'</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">B</span><span class="p">)</span>
|
||||
|
||||
<span class="n">s</span> <span class="o">=</span> <span class="n">Fixedpoint</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">engine</span><span class="o">=</span><span class="s">'datalog'</span><span class="p">,</span><span class="n">compile_with_widening</span><span class="o">=</span><span class="bp">True</span><span class="p">,</span>
|
||||
<span class="n">unbound_compressor</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">register_relation</span><span class="p">(</span><span class="n">l0</span><span class="p">,</span><span class="n">l1</span><span class="p">)</span>
|
||||
<span class="n">s</span><span class="o">.</span><span class="n">set_predicate_representation</span><span class="p">(</span><span class="n">l0</span><span class="p">,</span> <span class="s">'interval_relation'</span><span class="p">,</span> <span class="s">'bound_relation'</span><span class="p">)</span>
|
||||
<span class="n">s</span><span class="o">.</span><span class="n">set_predicate_representation</span><span class="p">(</span><span class="n">l1</span><span class="p">,</span> <span class="s">'interval_relation'</span><span class="p">,</span> <span class="s">'bound_relation'</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="n">y</span> <span class="o">=</span> <span class="n">Ints</span><span class="p">(</span><span class="s">'m x y'</span><span class="p">)</span>
|
||||
|
||||
<span class="n">s</span><span class="o">.</span><span class="n">declare_var</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="n">y</span><span class="p">)</span>
|
||||
<span class="n">s</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">l0</span><span class="p">(</span><span class="mi">0</span><span class="p">,</span><span class="n">m</span><span class="p">),</span> <span class="mi">0</span> <span class="o"><</span> <span class="n">m</span><span class="p">)</span>
|
||||
<span class="n">s</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">l0</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="n">m</span><span class="p">),</span> <span class="p">[</span><span class="n">l0</span><span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="n">m</span><span class="p">),</span> <span class="n">x</span> <span class="o"><</span> <span class="n">m</span><span class="p">])</span>
|
||||
<span class="n">s</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">l1</span><span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="n">m</span><span class="p">),</span> <span class="p">[</span><span class="n">l0</span><span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="n">m</span><span class="p">),</span> <span class="n">m</span> <span class="o"><=</span> <span class="n">x</span><span class="p">])</span>
|
||||
|
||||
<span class="k">print</span> <span class="s">"At l0 we learn that x, y are non-negative:"</span>
|
||||
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">l0</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="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">get_answer</span><span class="p">()</span>
|
||||
|
||||
<span class="k">print</span> <span class="s">"At l1 we learn that x <= y and both x and y are bigger than 0:"</span>
|
||||
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">l1</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="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">get_answer</span><span class="p">()</span>
|
||||
|
||||
|
||||
<span class="k">print</span> <span class="s">"The state where x < y is not reachable"</span>
|
||||
<span class="k">print</span> <span class="n">s</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">l1</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">x</span> <span class="o"><</span> <span class="n">y</span><span class="p">))</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
The example uses the option
|
||||
<pre>
|
||||
set_option(dl_compile_with_widening=True)
|
||||
</pre>
|
||||
to instrument Z3 to apply abstract interpretation <em>widening</em> on loop boundaries.
|
||||
|
||||
|
||||
<h2>Engine for Property Directed Reachability</h2>
|
||||
|
||||
A different underlying engine for fixed-points is based on
|
||||
an algorithm for <it>Property Directed Reachability (PDR)</it>.
|
||||
The PDR engine is enabled using the instruction
|
||||
<pre>
|
||||
set_option(dl_engine=1)
|
||||
</pre>
|
||||
The version in Z3 applies to Horn clauses with arithmetic and
|
||||
Boolean domains. When using arithmetic you should enable
|
||||
the main abstraction engine used in Z3 for arithmetic in PDR.
|
||||
<pre>
|
||||
set_option(dl_pdr_use_farkas=True)
|
||||
</pre>
|
||||
The engine also works with domains using algebraic
|
||||
data-types and bit-vectors, although it is currently not
|
||||
overly tuned for either.
|
||||
The PDR engine is targeted at applications from symbolic model
|
||||
checking of software. The systems may be infinite state.
|
||||
The following examples also serve a purpose of showing
|
||||
how software model checking problems (of safety properties)
|
||||
can be embedded into Horn clauses and solved using PDR.
|
||||
|
||||
<h3>Procedure Calls</h3>
|
||||
<p>
|
||||
McCarthy's 91 function illustrates a procedure that calls itself recursively
|
||||
twice. The Horn clauses below encode the recursive function:
|
||||
|
||||
</p>
|
||||
<pre>
|
||||
mc(x) = if x > 100 then x - 10 else mc(mc(x+11))
|
||||
</pre>
|
||||
|
||||
The general scheme for encoding recursive procedures is by creating a predicate
|
||||
for each procedure and adding an additional output variable to the predicate.
|
||||
Nested calls to procedures within a body can be encoded as a conjunction
|
||||
of relations.
|
||||
|
||||
|
||||
<example pref="fixedpoint.8"><html><body>
|
||||
<div class="highlight"><pre><span class="n">mc</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'mc'</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">BoolSort</span><span class="p">())</span>
|
||||
<span class="n">n</span><span class="p">,</span> <span class="n">m</span><span class="p">,</span> <span class="n">p</span> <span class="o">=</span> <span class="n">Ints</span><span class="p">(</span><span class="s">'n m p'</span><span class="p">)</span>
|
||||
|
||||
<span class="n">fp</span> <span class="o">=</span> <span class="n">Fixedpoint</span><span class="p">()</span>
|
||||
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">declare_var</span><span class="p">(</span><span class="n">n</span><span class="p">,</span><span class="n">m</span><span class="p">)</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">register_relation</span><span class="p">(</span><span class="n">mc</span><span class="p">)</span>
|
||||
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">mc</span><span class="p">(</span><span class="n">m</span><span class="p">,</span> <span class="n">m</span><span class="o">-</span><span class="mi">10</span><span class="p">),</span> <span class="n">m</span> <span class="o">></span> <span class="mi">100</span><span class="p">)</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">mc</span><span class="p">(</span><span class="n">m</span><span class="p">,</span> <span class="n">n</span><span class="p">),</span> <span class="p">[</span><span class="n">m</span> <span class="o"><=</span> <span class="mi">100</span><span class="p">,</span> <span class="n">mc</span><span class="p">(</span><span class="n">m</span><span class="o">+</span><span class="mi">11</span><span class="p">,</span><span class="n">p</span><span class="p">),</span><span class="n">mc</span><span class="p">(</span><span class="n">p</span><span class="p">,</span><span class="n">n</span><span class="p">)])</span>
|
||||
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">mc</span><span class="p">(</span><span class="n">m</span><span class="p">,</span><span class="n">n</span><span class="p">),</span><span class="n">n</span> <span class="o"><</span> <span class="mi">90</span><span class="p">))</span>
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">get_answer</span><span class="p">()</span>
|
||||
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">mc</span><span class="p">(</span><span class="n">m</span><span class="p">,</span><span class="n">n</span><span class="p">),</span><span class="n">n</span> <span class="o"><</span> <span class="mi">91</span><span class="p">))</span>
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">get_answer</span><span class="p">()</span>
|
||||
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">mc</span><span class="p">(</span><span class="n">m</span><span class="p">,</span><span class="n">n</span><span class="p">),</span><span class="n">n</span> <span class="o"><</span> <span class="mi">92</span><span class="p">))</span>
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">get_answer</span><span class="p">()</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
The first two queries are unsatisfiable. The PDR engine produces the same proof of unsatisfiability.
|
||||
The proof is an inductive invariant for each recursive predicate. The PDR engine introduces a
|
||||
special query predicate for the query.
|
||||
|
||||
<h3>Bakery</h3>
|
||||
|
||||
<p>
|
||||
We can also prove invariants of reactive systems. It is convenient to encode reactive systems
|
||||
as guarded transition systems. It is perhaps for some not as convenient to directly encode
|
||||
guarded transitions as recursive Horn clauses. But it is fairly easy to write a translator
|
||||
from guarded transition systems to recursive Horn clauses. We illustrate a translator
|
||||
and Lamport's two process Bakery algorithm in the next example.
|
||||
</p>
|
||||
|
||||
<example pref="fixedpoint.9"><html><body>
|
||||
<div class="highlight"><pre><span class="n">set_option</span><span class="p">(</span><span class="n">relevancy</span><span class="o">=</span><span class="mi">0</span><span class="p">,</span><span class="n">verbose</span><span class="o">=</span><span class="mi">1</span><span class="p">)</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">flatten</span><span class="p">(</span><span class="n">l</span><span class="p">):</span>
|
||||
<span class="k">return</span> <span class="p">[</span><span class="n">s</span> <span class="k">for</span> <span class="n">t</span> <span class="ow">in</span> <span class="n">l</span> <span class="k">for</span> <span class="n">s</span> <span class="ow">in</span> <span class="n">t</span><span class="p">]</span>
|
||||
|
||||
|
||||
<span class="k">class</span> <span class="nc">TransitionSystem</span><span class="p">():</span>
|
||||
<span class="k">def</span> <span class="nf">__init__</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">initial</span><span class="p">,</span> <span class="n">transitions</span><span class="p">,</span> <span class="n">vars1</span><span class="p">):</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">fp</span> <span class="o">=</span> <span class="n">Fixedpoint</span><span class="p">()</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">initial</span> <span class="o">=</span> <span class="n">initial</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">transitions</span> <span class="o">=</span> <span class="n">transitions</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">vars1</span> <span class="o">=</span> <span class="n">vars1</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">declare_rels</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
|
||||
<span class="n">B</span> <span class="o">=</span> <span class="n">BoolSort</span><span class="p">()</span>
|
||||
<span class="n">var_sorts</span> <span class="o">=</span> <span class="p">[</span> <span class="n">v</span><span class="o">.</span><span class="n">sort</span><span class="p">()</span> <span class="k">for</span> <span class="n">v</span> <span class="ow">in</span> <span class="bp">self</span><span class="o">.</span><span class="n">vars1</span> <span class="p">]</span>
|
||||
<span class="n">state_sorts</span> <span class="o">=</span> <span class="n">var_sorts</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">state_vals</span> <span class="o">=</span> <span class="p">[</span> <span class="n">v</span> <span class="k">for</span> <span class="n">v</span> <span class="ow">in</span> <span class="bp">self</span><span class="o">.</span><span class="n">vars1</span> <span class="p">]</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</span> <span class="o">=</span> <span class="n">state_sorts</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">var_sorts</span> <span class="o">=</span> <span class="n">var_sorts</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">state</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'state'</span><span class="p">,</span> <span class="n">state_sorts</span> <span class="o">+</span> <span class="p">[</span> <span class="n">B</span> <span class="p">])</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">step</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'step'</span><span class="p">,</span> <span class="n">state_sorts</span> <span class="o">+</span> <span class="n">state_sorts</span> <span class="o">+</span> <span class="p">[</span> <span class="n">B</span> <span class="p">])</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">fp</span><span class="o">.</span><span class="n">register_relation</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">state</span><span class="p">)</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">fp</span><span class="o">.</span><span class="n">register_relation</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">step</span><span class="p">)</span>
|
||||
|
||||
<span class="c"># Set of reachable states are transitive closure of step.</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">state0</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
|
||||
<span class="n">idx</span> <span class="o">=</span> <span class="nb">range</span><span class="p">(</span><span class="nb">len</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</span><span class="p">))</span>
|
||||
<span class="k">return</span> <span class="bp">self</span><span class="o">.</span><span class="n">state</span><span class="p">([</span><span class="n">Var</span><span class="p">(</span><span class="n">i</span><span class="p">,</span><span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</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="n">idx</span><span class="p">])</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">state1</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
|
||||
<span class="n">n</span> <span class="o">=</span> <span class="nb">len</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</span><span class="p">)</span>
|
||||
<span class="k">return</span> <span class="bp">self</span><span class="o">.</span><span class="n">state</span><span class="p">([</span><span class="n">Var</span><span class="p">(</span><span class="n">i</span><span class="o">+</span><span class="n">n</span><span class="p">,</span> <span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</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="n">n</span><span class="p">)])</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">rho</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
|
||||
<span class="n">n</span> <span class="o">=</span> <span class="nb">len</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</span><span class="p">)</span>
|
||||
<span class="n">args1</span> <span class="o">=</span> <span class="p">[</span> <span class="n">Var</span><span class="p">(</span><span class="n">i</span><span class="p">,</span><span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</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="n">n</span><span class="p">)</span> <span class="p">]</span>
|
||||
<span class="n">args2</span> <span class="o">=</span> <span class="p">[</span> <span class="n">Var</span><span class="p">(</span><span class="n">i</span><span class="o">+</span><span class="n">n</span><span class="p">,</span><span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</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="n">n</span><span class="p">)</span> <span class="p">]</span>
|
||||
<span class="n">args</span> <span class="o">=</span> <span class="n">args1</span> <span class="o">+</span> <span class="n">args2</span>
|
||||
<span class="k">return</span> <span class="bp">self</span><span class="o">.</span><span class="n">step</span><span class="p">(</span><span class="n">args</span><span class="p">)</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">declare_reachability</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">state1</span><span class="p">(),</span> <span class="p">[</span><span class="bp">self</span><span class="o">.</span><span class="n">state0</span><span class="p">(),</span> <span class="bp">self</span><span class="o">.</span><span class="n">rho</span><span class="p">()])</span>
|
||||
|
||||
|
||||
<span class="c"># Define transition relation</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">abstract</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">e</span><span class="p">):</span>
|
||||
<span class="n">n</span> <span class="o">=</span> <span class="nb">len</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</span><span class="p">)</span>
|
||||
<span class="n">sub</span> <span class="o">=</span> <span class="p">[(</span><span class="bp">self</span><span class="o">.</span><span class="n">state_vals</span><span class="p">[</span><span class="n">i</span><span class="p">],</span> <span class="n">Var</span><span class="p">(</span><span class="n">i</span><span class="p">,</span><span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</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="n">n</span><span class="p">)]</span>
|
||||
<span class="k">return</span> <span class="n">substitute</span><span class="p">(</span><span class="n">e</span><span class="p">,</span> <span class="n">sub</span><span class="p">)</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">declare_transition</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">tr</span><span class="p">):</span>
|
||||
<span class="n">len_s</span> <span class="o">=</span> <span class="nb">len</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</span><span class="p">)</span>
|
||||
<span class="n">effect</span> <span class="o">=</span> <span class="n">tr</span><span class="p">[</span><span class="s">"effect"</span><span class="p">]</span>
|
||||
<span class="n">vars1</span> <span class="o">=</span> <span class="p">[</span><span class="n">Var</span><span class="p">(</span><span class="n">i</span><span class="p">,</span><span class="bp">self</span><span class="o">.</span><span class="n">state_sorts</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="n">len_s</span><span class="p">)]</span> <span class="o">+</span> <span class="n">effect</span>
|
||||
<span class="n">rho1</span> <span class="o">=</span> <span class="bp">self</span><span class="o">.</span><span class="n">abstract</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">step</span><span class="p">(</span><span class="n">vars1</span><span class="p">))</span>
|
||||
<span class="n">guard</span> <span class="o">=</span> <span class="bp">self</span><span class="o">.</span><span class="n">abstract</span><span class="p">(</span><span class="n">tr</span><span class="p">[</span><span class="s">"guard"</span><span class="p">])</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">rho1</span><span class="p">,</span> <span class="n">guard</span><span class="p">)</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">declare_transitions</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
|
||||
<span class="k">for</span> <span class="n">t</span> <span class="ow">in</span> <span class="bp">self</span><span class="o">.</span><span class="n">transitions</span><span class="p">:</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">declare_transition</span><span class="p">(</span><span class="n">t</span><span class="p">)</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">declare_initial</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">state0</span><span class="p">(),[</span><span class="bp">self</span><span class="o">.</span><span class="n">abstract</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">initial</span><span class="p">)])</span>
|
||||
|
||||
<span class="k">def</span> <span class="nf">query</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">query</span><span class="p">):</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">declare_rels</span><span class="p">()</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">declare_initial</span><span class="p">()</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">declare_reachability</span><span class="p">()</span>
|
||||
<span class="bp">self</span><span class="o">.</span><span class="n">declare_transitions</span><span class="p">()</span>
|
||||
<span class="n">query</span> <span class="o">=</span> <span class="n">And</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">state0</span><span class="p">(),</span> <span class="bp">self</span><span class="o">.</span><span class="n">abstract</span><span class="p">(</span><span class="n">query</span><span class="p">))</span>
|
||||
<span class="k">print</span> <span class="bp">self</span><span class="o">.</span><span class="n">fp</span>
|
||||
<span class="k">print</span> <span class="n">query</span>
|
||||
<span class="k">print</span> <span class="bp">self</span><span class="o">.</span><span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">query</span><span class="p">)</span>
|
||||
<span class="k">print</span> <span class="bp">self</span><span class="o">.</span><span class="n">fp</span><span class="o">.</span><span class="n">get_answer</span><span class="p">()</span>
|
||||
<span class="c"># print self.fp.statistics()</span>
|
||||
|
||||
|
||||
<span class="n">L</span> <span class="o">=</span> <span class="n">Datatype</span><span class="p">(</span><span class="s">'L'</span><span class="p">)</span>
|
||||
<span class="n">L</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'L0'</span><span class="p">)</span>
|
||||
<span class="n">L</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'L1'</span><span class="p">)</span>
|
||||
<span class="n">L</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'L2'</span><span class="p">)</span>
|
||||
<span class="n">L</span> <span class="o">=</span> <span class="n">L</span><span class="o">.</span><span class="n">create</span><span class="p">()</span>
|
||||
<span class="n">L0</span> <span class="o">=</span> <span class="n">L</span><span class="o">.</span><span class="n">L0</span>
|
||||
<span class="n">L1</span> <span class="o">=</span> <span class="n">L</span><span class="o">.</span><span class="n">L1</span>
|
||||
<span class="n">L2</span> <span class="o">=</span> <span class="n">L</span><span class="o">.</span><span class="n">L2</span>
|
||||
|
||||
|
||||
<span class="n">y0</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y0'</span><span class="p">)</span>
|
||||
<span class="n">y1</span> <span class="o">=</span> <span class="n">Int</span><span class="p">(</span><span class="s">'y1'</span><span class="p">)</span>
|
||||
<span class="n">l</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'l'</span><span class="p">,</span> <span class="n">L</span><span class="p">)</span>
|
||||
<span class="n">m</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'m'</span><span class="p">,</span> <span class="n">L</span><span class="p">)</span>
|
||||
|
||||
|
||||
<span class="n">t1</span> <span class="o">=</span> <span class="p">{</span> <span class="s">"guard"</span> <span class="p">:</span> <span class="n">l</span> <span class="o">==</span> <span class="n">L0</span><span class="p">,</span>
|
||||
<span class="s">"effect"</span> <span class="p">:</span> <span class="p">[</span> <span class="n">L1</span><span class="p">,</span> <span class="n">y1</span> <span class="o">+</span> <span class="mi">1</span><span class="p">,</span> <span class="n">m</span><span class="p">,</span> <span class="n">y1</span> <span class="p">]</span> <span class="p">}</span>
|
||||
<span class="n">t2</span> <span class="o">=</span> <span class="p">{</span> <span class="s">"guard"</span> <span class="p">:</span> <span class="n">And</span><span class="p">(</span><span class="n">l</span> <span class="o">==</span> <span class="n">L1</span><span class="p">,</span> <span class="n">Or</span><span class="p">([</span><span class="n">y0</span> <span class="o"><=</span> <span class="n">y1</span><span class="p">,</span> <span class="n">y1</span> <span class="o">==</span> <span class="mi">0</span><span class="p">])),</span>
|
||||
<span class="s">"effect"</span> <span class="p">:</span> <span class="p">[</span> <span class="n">L2</span><span class="p">,</span> <span class="n">y0</span><span class="p">,</span> <span class="n">m</span><span class="p">,</span> <span class="n">y1</span> <span class="p">]</span> <span class="p">}</span>
|
||||
<span class="n">t3</span> <span class="o">=</span> <span class="p">{</span> <span class="s">"guard"</span> <span class="p">:</span> <span class="n">l</span> <span class="o">==</span> <span class="n">L2</span><span class="p">,</span>
|
||||
<span class="s">"effect"</span> <span class="p">:</span> <span class="p">[</span> <span class="n">L0</span><span class="p">,</span> <span class="n">IntVal</span><span class="p">(</span><span class="mi">0</span><span class="p">),</span> <span class="n">m</span><span class="p">,</span> <span class="n">y1</span> <span class="p">]}</span>
|
||||
<span class="n">s1</span> <span class="o">=</span> <span class="p">{</span> <span class="s">"guard"</span> <span class="p">:</span> <span class="n">m</span> <span class="o">==</span> <span class="n">L0</span><span class="p">,</span>
|
||||
<span class="s">"effect"</span> <span class="p">:</span> <span class="p">[</span> <span class="n">l</span><span class="p">,</span> <span class="n">y0</span><span class="p">,</span> <span class="n">L1</span><span class="p">,</span> <span class="n">y0</span> <span class="o">+</span> <span class="mi">1</span> <span class="p">]</span> <span class="p">}</span>
|
||||
<span class="n">s2</span> <span class="o">=</span> <span class="p">{</span> <span class="s">"guard"</span> <span class="p">:</span> <span class="n">And</span><span class="p">(</span><span class="n">m</span> <span class="o">==</span> <span class="n">L1</span><span class="p">,</span> <span class="n">Or</span><span class="p">([</span><span class="n">y1</span> <span class="o"><=</span> <span class="n">y0</span><span class="p">,</span> <span class="n">y0</span> <span class="o">==</span> <span class="mi">0</span><span class="p">])),</span>
|
||||
<span class="s">"effect"</span> <span class="p">:</span> <span class="p">[</span> <span class="n">l</span><span class="p">,</span> <span class="n">y0</span><span class="p">,</span> <span class="n">L2</span><span class="p">,</span> <span class="n">y1</span> <span class="p">]</span> <span class="p">}</span>
|
||||
<span class="n">s3</span> <span class="o">=</span> <span class="p">{</span> <span class="s">"guard"</span> <span class="p">:</span> <span class="n">m</span> <span class="o">==</span> <span class="n">L2</span><span class="p">,</span>
|
||||
<span class="s">"effect"</span> <span class="p">:</span> <span class="p">[</span> <span class="n">l</span><span class="p">,</span> <span class="n">y0</span><span class="p">,</span> <span class="n">L0</span><span class="p">,</span> <span class="n">IntVal</span><span class="p">(</span><span class="mi">0</span><span class="p">)</span> <span class="p">]}</span>
|
||||
|
||||
|
||||
<span class="n">ptr</span> <span class="o">=</span> <span class="n">TransitionSystem</span><span class="p">(</span> <span class="n">And</span><span class="p">(</span><span class="n">l</span> <span class="o">==</span> <span class="n">L0</span><span class="p">,</span> <span class="n">y0</span> <span class="o">==</span> <span class="mi">0</span><span class="p">,</span> <span class="n">m</span> <span class="o">==</span> <span class="n">L0</span><span class="p">,</span> <span class="n">y1</span> <span class="o">==</span> <span class="mi">0</span><span class="p">),</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> <span class="n">s1</span><span class="p">,</span> <span class="n">s2</span><span class="p">,</span> <span class="n">s3</span><span class="p">],</span>
|
||||
<span class="p">[</span><span class="n">l</span><span class="p">,</span> <span class="n">y0</span><span class="p">,</span> <span class="n">m</span><span class="p">,</span> <span class="n">y1</span><span class="p">])</span>
|
||||
|
||||
<span class="n">ptr</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">And</span><span class="p">([</span><span class="n">l</span> <span class="o">==</span> <span class="n">L2</span><span class="p">,</span> <span class="n">m</span> <span class="o">==</span> <span class="n">L2</span> <span class="p">]))</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
The rather verbose (and in no way minimal) inductive invariants are produced as answers.
|
||||
|
||||
<h3>Functional Programs</h3>
|
||||
We can also verify some properties of functional programs using Z3's
|
||||
generalized PDR. Let us here consider an example from
|
||||
<a href="http://www.kb.is.s.u-tokyo.ac.jp/~uhiro/">
|
||||
<em>Predicate Abstraction and CEGAR for Higher-Order Model
|
||||
Checking, Kobayashi et.al. PLDI 2011</em></a>.
|
||||
We encode functional programs by taking a suitable operational
|
||||
semantics and encoding an evaluator that is specialized to
|
||||
the program being verified (we don't encode a general purpose
|
||||
evaluator, you should partial evaluate it to help verification).
|
||||
We use algebraic data-types to encode the current closure that is
|
||||
being evaluated.
|
||||
|
||||
<example pref="fixedpoint.10"><html><body>
|
||||
<div class="highlight"><pre><span class="c"># let max max2 x y z = max2 (max2 x y) z</span>
|
||||
<span class="c"># let f x y = if x > y then x else y</span>
|
||||
<span class="c"># assert (f (max f x y z) x) = (max f x y z)</span>
|
||||
|
||||
|
||||
<span class="n">Expr</span> <span class="o">=</span> <span class="n">Datatype</span><span class="p">(</span><span class="s">'Expr'</span><span class="p">)</span>
|
||||
<span class="n">Expr</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'Max'</span><span class="p">)</span>
|
||||
<span class="n">Expr</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'f'</span><span class="p">)</span>
|
||||
<span class="n">Expr</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'I'</span><span class="p">,</span> <span class="p">(</span><span class="s">'i'</span><span class="p">,</span> <span class="n">IntSort</span><span class="p">()))</span>
|
||||
<span class="n">Expr</span><span class="o">.</span><span class="n">declare</span><span class="p">(</span><span class="s">'App'</span><span class="p">,</span> <span class="p">(</span><span class="s">'fn'</span><span class="p">,</span><span class="n">Expr</span><span class="p">),(</span><span class="s">'arg'</span><span class="p">,</span><span class="n">Expr</span><span class="p">))</span>
|
||||
<span class="n">Expr</span> <span class="o">=</span> <span class="n">Expr</span><span class="o">.</span><span class="n">create</span><span class="p">()</span>
|
||||
<span class="n">Max</span> <span class="o">=</span> <span class="n">Expr</span><span class="o">.</span><span class="n">Max</span>
|
||||
<span class="n">I</span> <span class="o">=</span> <span class="n">Expr</span><span class="o">.</span><span class="n">I</span>
|
||||
<span class="n">App</span> <span class="o">=</span> <span class="n">Expr</span><span class="o">.</span><span class="n">App</span>
|
||||
<span class="n">f</span> <span class="o">=</span> <span class="n">Expr</span><span class="o">.</span><span class="n">f</span>
|
||||
<span class="n">Eval</span> <span class="o">=</span> <span class="n">Function</span><span class="p">(</span><span class="s">'Eval'</span><span class="p">,</span><span class="n">Expr</span><span class="p">,</span><span class="n">Expr</span><span class="p">,</span><span class="n">Expr</span><span class="p">,</span><span class="n">BoolSort</span><span class="p">())</span>
|
||||
|
||||
<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">Expr</span><span class="p">)</span>
|
||||
<span class="n">y</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'y'</span><span class="p">,</span><span class="n">Expr</span><span class="p">)</span>
|
||||
<span class="n">z</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'z'</span><span class="p">,</span><span class="n">Expr</span><span class="p">)</span>
|
||||
<span class="n">r1</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'r1'</span><span class="p">,</span><span class="n">Expr</span><span class="p">)</span>
|
||||
<span class="n">r2</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'r2'</span><span class="p">,</span><span class="n">Expr</span><span class="p">)</span>
|
||||
<span class="nb">max</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'max'</span><span class="p">,</span><span class="n">Expr</span><span class="p">)</span>
|
||||
<span class="n">xi</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'xi'</span><span class="p">,</span><span class="n">IntSort</span><span class="p">())</span>
|
||||
<span class="n">yi</span> <span class="o">=</span> <span class="n">Const</span><span class="p">(</span><span class="s">'yi'</span><span class="p">,</span><span class="n">IntSort</span><span class="p">())</span>
|
||||
|
||||
<span class="n">fp</span> <span class="o">=</span> <span class="n">Fixedpoint</span><span class="p">()</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">register_relation</span><span class="p">(</span><span class="n">Eval</span><span class="p">)</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">declare_var</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">r1</span><span class="p">,</span><span class="n">r2</span><span class="p">,</span><span class="nb">max</span><span class="p">,</span><span class="n">xi</span><span class="p">,</span><span class="n">yi</span><span class="p">)</span>
|
||||
|
||||
<span class="c"># Max max x y z = max (max x y) z</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">Eval</span><span class="p">(</span><span class="n">App</span><span class="p">(</span><span class="n">App</span><span class="p">(</span><span class="n">App</span><span class="p">(</span><span class="n">Max</span><span class="p">,</span><span class="nb">max</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">r2</span><span class="p">),</span>
|
||||
<span class="p">[</span><span class="n">Eval</span><span class="p">(</span><span class="n">App</span><span class="p">(</span><span class="nb">max</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">r1</span><span class="p">),</span>
|
||||
<span class="n">Eval</span><span class="p">(</span><span class="n">App</span><span class="p">(</span><span class="nb">max</span><span class="p">,</span><span class="n">r1</span><span class="p">),</span><span class="n">z</span><span class="p">,</span><span class="n">r2</span><span class="p">)])</span>
|
||||
|
||||
<span class="c"># f x y = x if x >= y</span>
|
||||
<span class="c"># f x y = y if x < y</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">Eval</span><span class="p">(</span><span class="n">App</span><span class="p">(</span><span class="n">f</span><span class="p">,</span><span class="n">I</span><span class="p">(</span><span class="n">xi</span><span class="p">)),</span><span class="n">I</span><span class="p">(</span><span class="n">yi</span><span class="p">),</span><span class="n">I</span><span class="p">(</span><span class="n">xi</span><span class="p">)),</span><span class="n">xi</span> <span class="o">>=</span> <span class="n">yi</span><span class="p">)</span>
|
||||
<span class="n">fp</span><span class="o">.</span><span class="n">rule</span><span class="p">(</span><span class="n">Eval</span><span class="p">(</span><span class="n">App</span><span class="p">(</span><span class="n">f</span><span class="p">,</span><span class="n">I</span><span class="p">(</span><span class="n">xi</span><span class="p">)),</span><span class="n">I</span><span class="p">(</span><span class="n">yi</span><span class="p">),</span><span class="n">I</span><span class="p">(</span><span class="n">yi</span><span class="p">)),</span><span class="n">xi</span> <span class="o"><</span> <span class="n">yi</span><span class="p">)</span>
|
||||
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">query</span><span class="p">(</span><span class="n">And</span><span class="p">(</span><span class="n">Eval</span><span class="p">(</span><span class="n">App</span><span class="p">(</span><span class="n">App</span><span class="p">(</span><span class="n">App</span><span class="p">(</span><span class="n">Max</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="n">z</span><span class="p">,</span><span class="n">r1</span><span class="p">),</span>
|
||||
<span class="n">Eval</span><span class="p">(</span><span class="n">App</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">r1</span><span class="p">,</span><span class="n">r2</span><span class="p">),</span>
|
||||
<span class="n">r1</span> <span class="o">!=</span> <span class="n">r2</span><span class="p">))</span>
|
||||
|
||||
<span class="k">print</span> <span class="n">fp</span><span class="o">.</span><span class="n">get_answer</span><span class="p">()</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
|
||||
</body>
|
||||
</html>
|
||||
1101
examples/python/tutorial/html/guide-examples.htm
Normal file
1101
examples/python/tutorial/html/guide-examples.htm
Normal file
File diff suppressed because it is too large
Load diff
1
examples/python/tutorial/html/index.html
Normal file
1
examples/python/tutorial/html/index.html
Normal file
|
|
@ -0,0 +1 @@
|
|||
<html><body><script>location.replace("guide-examples.htm")</script></body></html>
|
||||
350
examples/python/tutorial/html/strategies-examples.htm
Normal file
350
examples/python/tutorial/html/strategies-examples.htm
Normal file
|
|
@ -0,0 +1,350 @@
|
|||
<html>
|
||||
<head>
|
||||
<title>Z3Py Strategies</title>
|
||||
<link rel="StyleSheet" href="style.css" type="text/css">
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<h1>Strategies</h1>
|
||||
|
||||
<p>
|
||||
High-performance solvers, such as Z3, contain many tightly integrated, handcrafted heuristic
|
||||
combinations of algorithmic proof methods. While these heuristic
|
||||
combinations tend to be highly tuned for known classes of problems,
|
||||
they may easily perform very badly on new classes of problems.
|
||||
This issue is becoming increasingly pressing
|
||||
as solvers begin to gain the attention of practitioners in diverse areas of science and engineering.
|
||||
In many cases, changes to the solver heuristics can make a
|
||||
tremendous difference.
|
||||
</p>
|
||||
|
||||
<p>
|
||||
In this tutorial we show how to create custom strategies using the basic building blocks
|
||||
available in Z3. Z3Py and Z3 4.0 implement the ideas proposed in this <a target="_blank" href="http://research.microsoft.com/en-us/um/people/leonardo/strategy.pdf">article</a>.
|
||||
</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>Introduction</h2>
|
||||
|
||||
<p>
|
||||
Z3 implements a methodology for orchestrating reasoning
|
||||
engines where "big" symbolic reasoning steps are represented as
|
||||
functions known as <b>tactics</b>, and tactics are composed using
|
||||
combinators known as <b>tacticals</b>. Tactics process sets of
|
||||
formulas called <b>Goals</b>.
|
||||
</p>
|
||||
|
||||
<p>
|
||||
When a tactic is applied to some goal <tt>G</tt>, four different outcomes
|
||||
are possible. The tactic succeeds in showing <tt>G</tt> to be satisfiable (i.e., feasible);
|
||||
succeeds in showing <tt>G</tt> to be unsatisfiable (i.e., infeasible); produces a sequence of subgoals; or fails.
|
||||
When reducing a goal <tt>G</tt> to a sequence of subgoals <tt>G1</tt>, ...,
|
||||
<tt>Gn</tt>, we face the problem of model conversion.
|
||||
A <b>model converter</b> construct a model for <tt>G</tt>
|
||||
using a model for some subgoal <tt>Gi</tt>.
|
||||
</p>
|
||||
|
||||
<p>In the following example, we create a goal <tt>g</tt> consisting of three formulas, and a tactic <tt>t</tt>
|
||||
composed of two built-in tactics: <tt>simplify</tt> and <tt>solve-eqs</tt>. The tactic <tt>simplify</tt>
|
||||
apply transformations equivalent to the ones found in the command <tt>simplify</tt>. The tactic <tt>solver-eqs</tt>
|
||||
eliminate variables using Gaussian elimination. Actually, <tt>solve-eqs</tt> is not restricted only to linear arithmetic.
|
||||
It can also eliminate arbitrary variables. Then, combinator <tt>Then</tt> applies <tt>simplify</tt> to the input goal
|
||||
and <tt>solve-eqs</tt> to each subgoal produced by <tt>simplify</tt>. In this example, only one subgoal is produced.
|
||||
</p>
|
||||
|
||||
<example pref="tactic.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">Reals</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
|
||||
<span class="n">g</span> <span class="o">=</span> <span class="n">Goal</span><span class="p">()</span>
|
||||
<span class="n">g</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">0</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="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="k">print</span> <span class="n">g</span>
|
||||
|
||||
<span class="n">t1</span> <span class="o">=</span> <span class="n">Tactic</span><span class="p">(</span><span class="s">'simplify'</span><span class="p">)</span>
|
||||
<span class="n">t2</span> <span class="o">=</span> <span class="n">Tactic</span><span class="p">(</span><span class="s">'solve-eqs'</span><span class="p">)</span>
|
||||
<span class="n">t</span> <span class="o">=</span> <span class="n">Then</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="k">print</span> <span class="n">t</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<p>In the example above, variable <tt>x</tt> is eliminated, and is not present the resultant goal.
|
||||
</p>
|
||||
|
||||
<p>In Z3, we say a <b>clause</b> is any constraint of the form <tt>Or(f_1, ..., f_n)</tt>.
|
||||
The tactic <tt>split-clause</tt> will select a clause <tt>Or(f_1, ..., f_n)</tt> in the input goal, and split it
|
||||
<tt>n</tt> subgoals. One for each subformula <tt>f_i</tt>.
|
||||
</p>
|
||||
|
||||
<example pref="tactic.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">Reals</span><span class="p">(</span><span class="s">'x y'</span><span class="p">)</span>
|
||||
<span class="n">g</span> <span class="o">=</span> <span class="n">Goal</span><span class="p">()</span>
|
||||
<span class="n">g</span><span class="o">.</span><span class="n">add</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="mi">0</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">==</span> <span class="n">y</span> <span class="o">+</span> <span class="mi">1</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="n">t</span> <span class="o">=</span> <span class="n">Tactic</span><span class="p">(</span><span class="s">'split-clause'</span><span class="p">)</span>
|
||||
<span class="n">r</span> <span class="o">=</span> <span class="n">t</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
<span class="k">for</span> <span class="n">g</span> <span class="ow">in</span> <span class="n">r</span><span class="p">:</span>
|
||||
<span class="k">print</span> <span class="n">g</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<h2>Tactics</h2>
|
||||
|
||||
<p>Z3 comes equipped with many built-in tactics.
|
||||
The command <tt>describe_tactics()</tt> provides a short description of all built-in tactics.
|
||||
</p>
|
||||
|
||||
<example pref="tactic.3"><html><body>
|
||||
<div class="highlight"><pre><span class="n">describe_tactics</span><span class="p">()</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<p>Z3Py comes equipped with the following tactic combinators (aka tacticals):
|
||||
</p>
|
||||
|
||||
<ul>
|
||||
<li> <tt>Then(t, s)</tt>
|
||||
applies <tt>t</tt> to the input goal and <tt>s</tt>
|
||||
to every subgoal produced by <tt>t</tt>.
|
||||
</li>
|
||||
<li> <tt>OrElse(t, s)</tt>
|
||||
first applies <tt>t</tt> to the given goal,
|
||||
if it fails then returns the result of <tt>s</tt> applied to the given goal.
|
||||
</li>
|
||||
<li> <tt>Repeat(t)</tt> Keep applying the given tactic until no subgoal is modified by it.
|
||||
</li>
|
||||
<li> <tt>Repeat(t, n)</tt> Keep applying the given tactic until no subgoal is modified by it, or
|
||||
the number of iterations is greater than <tt>n</tt>.
|
||||
</li>
|
||||
<li> <tt>TryFor(t, ms)</tt> Apply tactic <tt>t</tt> to the input goal, if it does not return in
|
||||
<tt>ms</tt> millisenconds, it fails.
|
||||
</li>
|
||||
<li> <tt>With(t, params)</tt> Apply the given tactic using the given parameters.
|
||||
</li>
|
||||
</ul>
|
||||
|
||||
<p>The following example demonstrate how to use these combinators.</p>
|
||||
|
||||
<example pref="tactic.4"><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">g</span> <span class="o">=</span> <span class="n">Goal</span><span class="p">()</span>
|
||||
<span class="n">g</span><span class="o">.</span><span class="n">add</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="mi">0</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="n">Or</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="n">y</span> <span class="o">==</span> <span class="mi">1</span><span class="p">),</span>
|
||||
<span class="n">Or</span><span class="p">(</span><span class="n">z</span> <span class="o">==</span> <span class="mi">0</span><span class="p">,</span> <span class="n">z</span> <span class="o">==</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">+</span> <span class="n">z</span> <span class="o">></span> <span class="mi">2</span><span class="p">)</span>
|
||||
|
||||
<span class="c"># Split all clauses"</span>
|
||||
<span class="n">split_all</span> <span class="o">=</span> <span class="n">Repeat</span><span class="p">(</span><span class="n">OrElse</span><span class="p">(</span><span class="n">Tactic</span><span class="p">(</span><span class="s">'split-clause'</span><span class="p">),</span>
|
||||
<span class="n">Tactic</span><span class="p">(</span><span class="s">'skip'</span><span class="p">)))</span>
|
||||
<span class="k">print</span> <span class="n">split_all</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
|
||||
<span class="n">split_at_most_2</span> <span class="o">=</span> <span class="n">Repeat</span><span class="p">(</span><span class="n">OrElse</span><span class="p">(</span><span class="n">Tactic</span><span class="p">(</span><span class="s">'split-clause'</span><span class="p">),</span>
|
||||
<span class="n">Tactic</span><span class="p">(</span><span class="s">'skip'</span><span class="p">)),</span>
|
||||
<span class="mi">1</span><span class="p">)</span>
|
||||
<span class="k">print</span> <span class="n">split_at_most_2</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
|
||||
<span class="c"># Split all clauses and solve equations</span>
|
||||
<span class="n">split_solve</span> <span class="o">=</span> <span class="n">Then</span><span class="p">(</span><span class="n">Repeat</span><span class="p">(</span><span class="n">OrElse</span><span class="p">(</span><span class="n">Tactic</span><span class="p">(</span><span class="s">'split-clause'</span><span class="p">),</span>
|
||||
<span class="n">Tactic</span><span class="p">(</span><span class="s">'skip'</span><span class="p">))),</span>
|
||||
<span class="n">Tactic</span><span class="p">(</span><span class="s">'solve-eqs'</span><span class="p">))</span>
|
||||
|
||||
<span class="k">print</span> <span class="n">split_solve</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<p>In the tactic <tt>split_solver</tt>, the tactic <tt>solve-eqs</tt> discharges all but one goal.
|
||||
Note that, this tactic generates one goal: the empty goal which is trivially satisfiable (i.e., feasible) </p>
|
||||
|
||||
<p>The list of subgoals can be easily traversed using the Python <tt>for</tt> statement.</p>
|
||||
|
||||
<example pref="tactic.5"><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">g</span> <span class="o">=</span> <span class="n">Goal</span><span class="p">()</span>
|
||||
<span class="n">g</span><span class="o">.</span><span class="n">add</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="mi">0</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="n">Or</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="n">y</span> <span class="o">==</span> <span class="mi">1</span><span class="p">),</span>
|
||||
<span class="n">Or</span><span class="p">(</span><span class="n">z</span> <span class="o">==</span> <span class="mi">0</span><span class="p">,</span> <span class="n">z</span> <span class="o">==</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">+</span> <span class="n">z</span> <span class="o">></span> <span class="mi">2</span><span class="p">)</span>
|
||||
|
||||
<span class="c"># Split all clauses"</span>
|
||||
<span class="n">split_all</span> <span class="o">=</span> <span class="n">Repeat</span><span class="p">(</span><span class="n">OrElse</span><span class="p">(</span><span class="n">Tactic</span><span class="p">(</span><span class="s">'split-clause'</span><span class="p">),</span>
|
||||
<span class="n">Tactic</span><span class="p">(</span><span class="s">'skip'</span><span class="p">)))</span>
|
||||
<span class="k">for</span> <span class="n">s</span> <span class="ow">in</span> <span class="n">split_all</span><span class="p">(</span><span class="n">g</span><span class="p">):</span>
|
||||
<span class="k">print</span> <span class="n">s</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<p>A tactic can be converted into a solver object using the method <tt>solver()</tt>.
|
||||
If the tactic produces the empty goal, then the associated solver returns <tt>sat</tt>.
|
||||
If the tactic produces a single goal containing <tt>False</tt>, then the solver returns <tt>unsat</tt>.
|
||||
Otherwise, it returns <tt>unknown</tt>.
|
||||
</p>
|
||||
|
||||
<example pref="tactic.6"><html><body>
|
||||
<div class="highlight"><pre><span class="n">bv_solver</span> <span class="o">=</span> <span class="n">Then</span><span class="p">(</span><span class="s">'simplify'</span><span class="p">,</span>
|
||||
<span class="s">'solve-eqs'</span><span class="p">,</span>
|
||||
<span class="s">'bit-blast'</span><span class="p">,</span>
|
||||
<span class="s">'sat'</span><span class="p">)</span><span class="o">.</span><span class="n">solver</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">BitVecs</span><span class="p">(</span><span class="s">'x y'</span><span class="p">,</span> <span class="mi">16</span><span class="p">)</span>
|
||||
<span class="n">solve_using</span><span class="p">(</span><span class="n">bv_solver</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">13</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>In the example above, the tactic <tt>bv_solver</tt> implements a basic bit-vector solver using equation solving,
|
||||
bit-blasting, and a propositional SAT solver. Note that, the command <tt>Tactic</tt> is suppressed.
|
||||
All Z3Py combinators automatically invoke <tt>Tactic</tt> command if the argument is a string.
|
||||
Finally, the command <tt>solve_using</tt> is a variant of the <tt>solve</tt> command where the first
|
||||
argument specifies the solver to be used.
|
||||
</p>
|
||||
|
||||
<p>In the following example, we use the solver API directly instead of the command <tt>solve_using</tt>.
|
||||
We use the combinator <tt>With</tt> to configure our little solver. We also include the tactic <tt>aig</tt>
|
||||
which tries to compress Boolean formulas using And-Inverted Graphs.
|
||||
</p>
|
||||
|
||||
<example pref="tactic.7"><html><body>
|
||||
<div class="highlight"><pre><span class="n">bv_solver</span> <span class="o">=</span> <span class="n">Then</span><span class="p">(</span><span class="n">With</span><span class="p">(</span><span class="s">'simplify'</span><span class="p">,</span> <span class="n">mul2concat</span><span class="o">=</span><span class="bp">True</span><span class="p">),</span>
|
||||
<span class="s">'solve-eqs'</span><span class="p">,</span>
|
||||
<span class="s">'bit-blast'</span><span class="p">,</span>
|
||||
<span class="s">'aig'</span><span class="p">,</span>
|
||||
<span class="s">'sat'</span><span class="p">)</span><span class="o">.</span><span class="n">solver</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">BitVecs</span><span class="p">(</span><span class="s">'x y'</span><span class="p">,</span> <span class="mi">16</span><span class="p">)</span>
|
||||
<span class="n">bv_solver</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">32</span> <span class="o">+</span> <span class="n">y</span> <span class="o">==</span> <span class="mi">13</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">10</span><span class="p">,</span> <span class="n">y</span> <span class="o">></span> <span class="o">-</span><span class="mi">100</span><span class="p">)</span>
|
||||
<span class="k">print</span> <span class="n">bv_solver</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">bv_solver</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="n">x</span><span class="o">*</span><span class="mi">32</span> <span class="o">+</span> <span class="n">y</span><span class="p">,</span> <span class="s">"=="</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="o">*</span><span class="mi">32</span> <span class="o">+</span> <span class="n">y</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="p">,</span> <span class="s">"=="</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="o">&</span> <span class="n">y</span><span class="p">)</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<p>The tactic <tt>smt</tt> wraps the main solver in Z3 as a tactic.</p>
|
||||
|
||||
<example pref="tactic.8"><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">s</span> <span class="o">=</span> <span class="n">Tactic</span><span class="p">(</span><span class="s">'smt'</span><span class="p">)</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">></span> <span class="n">y</span> <span class="o">+</span> <span class="mi">1</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="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>Now, we show how to implement a solver for integer arithmetic using SAT. The solver is complete
|
||||
only for problems where every variable has a lower and upper bound.
|
||||
</p>
|
||||
|
||||
<example pref="tactic.9"><html><body>
|
||||
<div class="highlight"><pre><span class="n">s</span> <span class="o">=</span> <span class="n">Then</span><span class="p">(</span><span class="n">With</span><span class="p">(</span><span class="s">'simplify'</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="n">som</span><span class="o">=</span><span class="bp">True</span><span class="p">),</span>
|
||||
<span class="s">'normalize-bounds'</span><span class="p">,</span> <span class="s">'lia2pb'</span><span class="p">,</span> <span class="s">'pb2bv'</span><span class="p">,</span>
|
||||
<span class="s">'bit-blast'</span><span class="p">,</span> <span class="s">'sat'</span><span class="p">)</span><span class="o">.</span><span class="n">solver</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">Ints</span><span class="p">(</span><span class="s">'x y z'</span><span class="p">)</span>
|
||||
<span class="n">solve_using</span><span class="p">(</span><span class="n">s</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"><</span> <span class="mi">10</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="n">y</span> <span class="o"><</span> <span class="mi">10</span><span class="p">,</span>
|
||||
<span class="n">z</span> <span class="o">></span> <span class="mi">0</span><span class="p">,</span> <span class="n">z</span> <span class="o"><</span> <span class="mi">10</span><span class="p">,</span>
|
||||
<span class="mi">3</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="n">z</span><span class="p">)</span>
|
||||
<span class="c"># It fails on the next example (it is unbounded)</span>
|
||||
<span class="n">s</span><span class="o">.</span><span class="n">reset</span><span class="p">()</span>
|
||||
<span class="n">solve_using</span><span class="p">(</span><span class="n">s</span><span class="p">,</span> <span class="mi">3</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="n">z</span><span class="p">)</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<p>
|
||||
Tactics can be combined with solvers. For example, we can apply a tactic to a goal, produced a set of subgoals,
|
||||
then select one of the subgoals and solve it using a solver. The next example demonstrates how to do that, and how to
|
||||
use model converters to convert a model for a subgoal into a model for the original goal.
|
||||
</p>
|
||||
|
||||
<example pref="tactic.10"><html><body>
|
||||
<div class="highlight"><pre><span class="n">t</span> <span class="o">=</span> <span class="n">Then</span><span class="p">(</span><span class="s">'simplify'</span><span class="p">,</span>
|
||||
<span class="s">'normalize-bounds'</span><span class="p">,</span>
|
||||
<span class="s">'solve-eqs'</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">Ints</span><span class="p">(</span><span class="s">'x y z'</span><span class="p">)</span>
|
||||
<span class="n">g</span> <span class="o">=</span> <span class="n">Goal</span><span class="p">()</span>
|
||||
<span class="n">g</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="n">x</span> <span class="o">+</span> <span class="mi">3</span><span class="p">,</span> <span class="n">z</span> <span class="o">></span> <span class="n">y</span><span class="p">)</span>
|
||||
|
||||
<span class="n">r</span> <span class="o">=</span> <span class="n">t</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
<span class="c"># r contains only one subgoal</span>
|
||||
<span class="k">print</span> <span class="n">r</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">r</span><span class="p">[</span><span class="mi">0</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="c"># Model for the subgoal</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="c"># Model for the original goal</span>
|
||||
<span class="k">print</span> <span class="n">r</span><span class="o">.</span><span class="n">convert_model</span><span class="p">(</span><span class="n">s</span><span class="o">.</span><span class="n">model</span><span class="p">())</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<h2>Probes</h2>
|
||||
|
||||
<p>
|
||||
<b>Probes</b> (aka formula measures) are evaluated over goals.
|
||||
Boolean expressions over them can be built using relational operators and Boolean connectives.
|
||||
The tactic <tt>FailIf(cond)</tt> fails if the given goal does not satisfy the condition <tt>cond</tt>.
|
||||
Many numeric and Boolean measures are available in Z3Py. The command <tt>describe_probes()</tt> provides the list of
|
||||
all built-in probes.
|
||||
</p>
|
||||
|
||||
<example pref="probe.1"><html><body>
|
||||
<div class="highlight"><pre><span class="n">describe_probes</span><span class="p">()</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<p>In the following example, we build a simple tactic using <tt>FailIf</tt>. It also shows that a probe can be applied directly
|
||||
to a goal.</p>
|
||||
|
||||
<example pref="probe.2"><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">g</span> <span class="o">=</span> <span class="n">Goal</span><span class="p">()</span>
|
||||
<span class="n">g</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="n">y</span> <span class="o">+</span> <span class="n">z</span> <span class="o">></span> <span class="mi">0</span><span class="p">)</span>
|
||||
|
||||
<span class="n">p</span> <span class="o">=</span> <span class="n">Probe</span><span class="p">(</span><span class="s">'num-consts'</span><span class="p">)</span>
|
||||
<span class="k">print</span> <span class="s">"num-consts:"</span><span class="p">,</span> <span class="n">p</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
|
||||
<span class="n">t</span> <span class="o">=</span> <span class="n">FailIf</span><span class="p">(</span><span class="n">p</span> <span class="o">></span> <span class="mi">2</span><span class="p">)</span>
|
||||
<span class="k">try</span><span class="p">:</span>
|
||||
<span class="n">t</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
<span class="k">except</span> <span class="n">Z3Exception</span><span class="p">:</span>
|
||||
<span class="k">print</span> <span class="s">"tactic failed"</span>
|
||||
|
||||
<span class="k">print</span> <span class="s">"trying again..."</span>
|
||||
<span class="n">g</span> <span class="o">=</span> <span class="n">Goal</span><span class="p">()</span>
|
||||
<span class="n">g</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="n">y</span> <span class="o">></span> <span class="mi">0</span><span class="p">)</span>
|
||||
<span class="k">print</span> <span class="n">t</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
<p>Z3Py also provides the combinator (tactical) <tt>If(p, t1, t2)</tt> which is a shorthand for:</p>
|
||||
|
||||
<pre>OrElse(Then(FailIf(Not(p)), t1), t2)</pre>
|
||||
|
||||
<p>The combinator <tt>When(p, t)</tt> is a shorthand for:</p>
|
||||
|
||||
<pre>If(p, t, 'skip')</pre>
|
||||
|
||||
<p>The tactic <tt>skip</tt> just returns the input goal.
|
||||
The following example demonstrates how to use the <tt>If</tt> combinator.</p>
|
||||
|
||||
<example pref="probe.3"><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">g</span> <span class="o">=</span> <span class="n">Goal</span><span class="p">()</span>
|
||||
<span class="n">g</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">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">0</span><span class="p">)</span>
|
||||
|
||||
<span class="n">p</span> <span class="o">=</span> <span class="n">Probe</span><span class="p">(</span><span class="s">'num-consts'</span><span class="p">)</span>
|
||||
<span class="n">t</span> <span class="o">=</span> <span class="n">If</span><span class="p">(</span><span class="n">p</span> <span class="o">></span> <span class="mi">2</span><span class="p">,</span> <span class="s">'simplify'</span><span class="p">,</span> <span class="s">'factor'</span><span class="p">)</span>
|
||||
|
||||
<span class="k">print</span> <span class="n">t</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
|
||||
<span class="n">g</span> <span class="o">=</span> <span class="n">Goal</span><span class="p">()</span>
|
||||
<span class="n">g</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="n">x</span> <span class="o">+</span> <span class="n">y</span> <span class="o">+</span> <span class="n">z</span> <span class="o">>=</span> <span class="mi">0</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">0</span><span class="p">)</span>
|
||||
|
||||
<span class="k">print</span> <span class="n">t</span><span class="p">(</span><span class="n">g</span><span class="p">)</span>
|
||||
</pre></div>
|
||||
</body></html></example>
|
||||
|
||||
</body>
|
||||
</html>
|
||||
Loading…
Reference in a new issue