Z3 API in Python

Z3 is a high performance theorem prover developed at Microsoft Research. 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.

This tutorial demonstrates the main capabilities of Z3Py: the Z3 API in Python. 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 (Python Tutorial).

The Z3 distribution also contains the C, .Net and OCaml 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 Scala^Z3 and SBV.

Please send feedback, comments and/or corrections to leonardo@microsoft.com. Your comments are very valuable.

Boolean Logic

Z3 supports Boolean operators: And, Or, Not, Implies (implication), If (if-then-else). Bi-implications are represented using equality ==. The following example shows how to solve a simple set of Boolean constraints.

p = Bool('p') 

q = Bool('q')

r = Bool('r')

solve(Implies(p, q), r == Not(q), Or(Not(p), r))

The Python Boolean constants True and False can be used to build Z3 Boolean expressions.

p = Bool('p') 

q = Bool('q')

print(And(p, q, True))

print(simplify(And(p, q, True)))

print(simplify(And(p, False)))

The following example uses a combination of polynomial and Boolean constraints.

p = Bool('p')

x = Real('x')

solve(Or(x 10), Or(p, x**2 == 2), Not(p))

The question is

we have to convert this code in python

from z3 import * p = Bool('p') 

q = Bool ('q')

r = Bool ('r')

solve(Implies(p, q), r == Not(q), Or(Not(p), r)

this is the output for my question.

[q = False, p = False, r = True]

And(p, q, True)

And(p, q)

False

[x = -1.4142135623?, p = False]

That what I have

back to classroom run requirements.txt main.py from z3 import* 1 NM+in ON p = Bool('p') q = Bool('a') r = Bool('r') solve(Implies(p, q), r == Not(a), Or(Not(p), r)) Python 3.7.4 (default, Jul 9 2019, 00:06:43) (GCC 6.3.0 20170516) on linux back to classroom run requirements.txt main.py from z3 import* 1 NM+in ON p = Bool('p') q = Bool('a') r = Bool('r') solve(Implies(p, q), r == Not(a), Or(Not(p), r)) Python 3.7.4 (default, Jul 9 2019, 00:06:43) (GCC 6.3.0 20170516) on linux