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