-
Notifications
You must be signed in to change notification settings - Fork 20
/
Copy pathadvanced-examples.htm
864 lines (732 loc) · 84.1 KB
/
advanced-examples.htm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
<html>
<head>
<title>Z3Py Advanced</title>
<link rel="StyleSheet" href="style.css" type="text/css">
</head>
<body>
<h3><div style="display: flex; justify-content: space-between; margin-left: 30%; margin-right: 30%;">
<a href="guide-examples.htm">Basics</a> <a href="strategies-examples.htm">Strategies</a> <a href="fixpoint-examples.htm">Fixpoints</a> <a href="advanced-examples.htm">Advanced</a> <a target="_blank" href="http://z3prover.github.io/api/html/namespacez3py.html">Z3py API</a> <a target="_blank" href="https://z3prover.github.io/api/html/z3.html">Z3 API</a>
</div></h3>
<h1>Advanced Topics</h1>
<p>
Please send feedback, comments and/or corrections to <a href="mailto:[email protected]">[email protected]</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>