【置顶】Z3 API IN PYTHON 中文文档 （官方文档翻译）

发表于 更新于 分类于 阅读次数：

Z3是Microsoft Research开发的高性能定理证明器。 Z3用于许多应用中，例如：软件/硬件验证和测试，约束求解，混合系统分析，安全性，生物学（计算机分析）以及几何问题。

本文内容：

  • z3安装， 无权限安装

  • Z3 API IN PYTHON 的翻译 + 解读

英文版原文见：https://ericpony.github.io/z3py-tutorial/guide-examples.htm

Z3是Microsoft Research开发的高性能定理证明器。 Z3用于许多应用中，例如：软件/硬件验证和测试，约束求解，混合系统分析，安全性，生物学（计算机分析）以及几何问题。

本教程演示了Z3Py的主要功能：Python中的Z3 API。阅读本教程不需要Python背景。但是，在某些时候学习Python是有用的，并且有很多优秀的免费资源可以用于这样做（Python Tutorial）。

Z3发行版还包含C，.Net和OCaml API。 Z3Py的源代码可在Z3发行版中找到，随意修改以满足您的需求。源代码还演示了如何在Z3 4.0中使用新功能。其他Z3的前端包括Scala ^ Z3和SBV。

安装攻略

详细地址： https://github.com/angr/angr-z3

这里具体讲一下z3如何在linux类系统下安装，以及如果没有权限，如何安装

下载安装包

我这里用到git直接下载，当然其他方法也可以

1
git clone https://github.com/angr/angr-z3.git

安装

1
cd z3

注意，如果要开通python功能，在下一步要很注意！！

1
python scripts/mk_make.py --prefix=想安装到的目录 --python --pypkgdir=你的python地址
  • 想安装到的目录 = /home/bella

这个目录一般是根目录，这样在根目录及其下属的目录都能用；特别是在服务器上，一定要加这个prefix，不然也安装不到根目录

  • 你的python地址= /home/bella/lib/python-2.7/site-packages

这个python地址，一般在用户目录的lib中，如果不在，就找一下在哪里，总之最后要落实到具体的python包的site-packages文件夹下。

注：地址写进去的时候不用加引号，直接按照上面的模式，把内容和路径换成自己的即可

1
2
3
cd build
make
make install

make这一步会花费比较长的时间，不要着急

如果这一步安装失败，则说明make 或 GCC/Clang没安装好，需重新配备。

最后如果提示“z3安装成功”的英语字样，则安装成功。

试验：

z3的文件夹内有一个examples/python，里面有一些.py的文件可以试验，使用方法：

切换到那个目录下：

1
python3 example.py

如果运行成功，显示：

1
2
sat
[y = 3/2, x = 4]

则表示成功

Getting Started 快速入门

让我们从以下简单的例子开始：

解不等式

输入：

1
2
3
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

输出：

1
[y = 0, x = 7]

函数Int（’x’）创建了一个名为 x 的整数变量。函数solve解决了一个约束系统。 上面的例子用到了两个变量x和y，以及三个约束条件。 Z3Py像Python使用=进行赋值。 运算符<，<=，>，> =，==和！=用于比较。 在上面的例子中，表达式x + 2 * y == 7是一个Z3约束。 Z3可以解决和紧缩公式。

Simplify

下面的例子展示了如何使用Z3公式/表达式简化器。

输入：

1
2
3
4
5
x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))

输出：

1
2
3
3 + 3*x + y
Not(y <= -2)
And(x >= 2, 2*x**2 + y**2 >= 3)

数学符号

默认情况下，Z3Py（网页版）使用数学符号显示公式和表达式。 像往常一样，∧是逻辑和，∨是逻辑或，等等。 命令set_option(html_mode = False)使得所有公式和表达式以Z3Py表示法显示。 这也是Z3发行版随附Z3Py版本的默认模式。

输入：

1
2
3
4
5
6
7
8
9
x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1

set_option(html_mode=False)
print x**2 + y**2 >= 1

set_option(html_mode=True)
print x**2 + y**2 >= 1

输出：

1
2
3
x**2 + y**2 >= 1
x**2 + y**2 >= 1
x<sup>2</sup> + y<sup>2</sup> &ge; 1

表达式分析

Z3提供遍历表达式的函数。

输入：

1
2
3
4
5
6
7
8
9
x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name:  ", n.decl().name()

输出：

1
2
3
4
5
6
num args:  2
children:  [x + y, 3]
1st child: x + y
2nd child: 3
operator:  >=
op name:   >=

数学运算

Z3提供了所有基本的数学运算。 Z3Py使用Python语言的相同运算符优先级。 像Python一样，**是幂运算。 Z3可以求解非线性多项式约束。

输入：

1
2
3
x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)

输出：

1
[x = 1/8, y = 2]

其中，Real('x')创建实际变量x。 Z3Py可以表示任意大的整数，有理数（如上例）和无理代数。 一个无理数代数是具有整数系数的多项式的根。 在内部，Z3精确地代表了所有这些数字。 无理数以十进制表示形式显示，以便读取结果。

精度设置

set_option用于配置Z3环境。 它用于设置全局配置选项，如结果如何显示。 选项set_option(precision = 30)设置显示结果时使用的小数位数。 这个？ 标记在1.2599210498？ 中表示输出被截断。

输入：

1
2
3
4
5
6
7
x = Real('x')
y = Real('y')
solve(x**2 + y**2 == 3, x**3 == 2)

set_option(precision=30)
print "Solving, and displaying result with 30 decimal places"
solve(x**2 + y**2 == 3, x**3 == 2)

输出：

1
2
3
4
[x = 1.2599210498?, y = -1.1885280594?]
Solving, and displaying result with 30 decimal places
[x = 1.259921049894873164767210607278?,
 y = -1.188528059421316533710369365015?]

以下示例演示了一个常见的错误。 表达式1/3是一个Python整数，而不是Z3有理数。 该示例还显示了在Z3Py中创建有理数的不同方法。 程序Q（num，den）创建一个Z3有理数，其中num是分子，den是分母。 RealVal(1)创建一个表示数字1的Z3实数。

输入：

1
2
3
4
5
6
7
8
9
print 1/3
print RealVal(1)/3
print Q(1,3)

x = Real('x')
print x + 1/3
print x + Q(1,3)
print x + "1/3"
print x + 0.25

输出：

1
2
3
4
5
6
7
0
1/3
1/3
x + 0
x + 1/3
x + 1/3
x + 1/4

有理数也可以用十进制表示法显示。

输入：

1
2
3
4
5
6
7
8
x = Real('x')
solve(3*x == 1)

set_option(rational_to_decimal=True)
solve(3*x == 1)

set_option(precision=30)
solve(3*x == 1)

输出：

1
2
3
[x = 1/3]
[x = 0.3333333333?]
[x = 0.333333333333333333333333333333?]

不可满足 / 无解

约束系统也可能没有解决方案。 在这种情况下，我们说这个系统是不可满足的。

输入：

1
2
x = Real('x')
solve(x > 4, x < 0)

输出：

1
no solution

注释

像在Python中一样，注释以＃开头，并在行尾结束。 Z3Py不支持跨越多行的评论。

1
2
3
# This is a comment
x = Real('x') # comment: creating x
print x**2 + 2*x + 2  # comment: printing polynomial

BOOL LOGIC 布尔逻辑

Z3支持布尔运算符：And, Or, Not, Implies (implication), If (if-then-else)。双蕴含符号用==表示。 以下示例显示如何解决一组简单的布尔约束。

输入：

1
2
3
4
p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(Implies(p, q), r == Not(q), Or(Not(p), r))

输出：

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

True、False in Python

Python布尔常量True和False可用于构建Z3布尔表达式。

输入：

1
2
3
4
5
p = Bool('p')
q = Bool('q')
print And(p, q, True)
print simplify(And(p, q, True))
print simplify(And(p, False))

输出：

1
2
3
And(p, q, True)
And(p, q)
False

多项式与布尔组合

以下示例使用多项式和布尔约束的组合。

输入：

1
2
3
p = Bool('p')
x = Real('x')
solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))

输出：

1
[x = -1.4142135623?, p = False]

因为solve中的三个assert都要满足，所以Not(p)推出p = False， 所以x**2 == 2要成立，所以x = +- sqrt(2)。又因为x > 10不可能，所以就是x < 5，也就是正负根号2都可以，只输出一个解即可，所以输出负根号2.

SOLVERS 求解器

Z3提供了不同的求解器。 在前面的例子中使用的命令solve是使用Z3求解器API实现的。 该实现可以在Z3发行版的z3.py文件中找到。

以下示例演示了基本的Solver API。

pop / push 断言堆栈

输入：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
x = Int('x')
y = Int('y')

s = Solver()
print s

s.add(x > 10, y == x + 2)
print s
print "Solving constraints in the solver s ..."
print s.check()

print "Create a new scope..."
s.push()
s.add(y < 11)
print s
print "Solving updated set of constraints..."
print s.check()

print "Restoring state..."
s.pop()
print s
print "Solving restored set of constraints..."
print s.check()

输出：

1
2
3
4
5
6
7
8
9
10
11
12
[]
[x > 10, y == x + 2]
Solving constraints in the solver s ...
sat
Create a new scope...
[x > 10, y == x + 2, y < 11]
Solving updated set of constraints...
unsat
Restoring state...
[x > 10, y == x + 2]
Solving restored set of constraints...
sat

可以看到，一开始求解器为空，后来加上两个断言之后，求解器的context就有了那两个断言。check求解器得到结果。sat 意味着满足（satisfied）。接下来创建了一个新的范围，可以看到新增了一个断言，这时候check的结果就是unsat，意味着不可满足（unsatisfied）. 再把新增的assert 弹出（pop）之后，可以看到又sat了。

Solver()命令创建一个通用求解器。约束可以使用方法add添加。方法check()解决了断言的约束。如果找到解决方案，结果是sat（满足）。如果不存在解决方案，结果unsat（不可满足）。我们也可以说，所声明的约束系统是不可行的(infeasible)。最后，求解器可能无法解决约束系统并返回unknown（未知）。

在一些应用中，我们想要探索几个共享几个约束的类似问题。我们可以使用push和pop命令来做到这一点。每个求解器维护一堆断言。命令push通过保存当前堆栈大小来创建一个新的作用域。命令pop删除它与匹配推送之间执行的任何断言。检查方法始终对求解器断言堆栈的内容进行操作。

只能求解非线形多项式约束

以下示例显示了Z3无法解决的示例。求解器在这种情况下返回未知数。回想一下，Z3可以求解非线性多项式约束，但2 ** x不是一个多项式。

输入：

1
2
3
4
x = Real('x')
s = Solver()
s.add(2**x == 3)
print s.check()

输出：

1
unknown

遍历 / 性能统计

以下示例显示如何遍历断言解析器中的约束，以及如何收集检查方法的性能统计信息。

输入：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
x = Real('x')
y = Real('y')
s = Solver()
s.add(x > 1, y > 1, Or(x + y > 3, x - y < 2))
print "asserted constraints..."
for c in s.assertions():
    print c

print s.check()
print "statistics for the last check method..."
print s.statistics()
# Traversing statistics
for k, v in s.statistics():
    print "%s : %s" % (k, v)

输出：

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
asserted constraints...
x > 1
y > 1
Or(x + y > 3, x - y < 2)
sat
statistics for the last check method...
(:arith-iterations    1
 :arith-lower         1
 :arith-make-feasible 3
 :arith-max-columns   4
 :arith-max-rows      2
 :arith-pivots        1
 :arith-rows          4
 :arith-upper         3
 :decisions           2
 :final-checks        1
 :max-memory          3.05
 :memory              2.73
 :mk-bool-var         10
 :num-allocs          33724
 :rlimit-count        298)
mk bool var : 1
decisions : 2
final checks : 1
mk bool var : 5
arith-lower : 1
arith-upper : 3
arith-rows : 4
arith-iterations : 1
arith-pivots : 1
arith-make-feasible : 3
arith-max-columns : 4
arith-max-rows : 2
mk bool var : 1
mk bool var : 1
mk bool var : 1
mk bool var : 1
num allocs : 33736
rlimit count : 298
max memory : 3.05
memory : 2.73

当Z3找到一组已确定约束的解决方案时，check就会返回sat, 我们就可以说Z3满足了这些约束条件，这个解决方案是这组声明约束的model。model是使每个断言约束都为真的interpretation。（大致翻译：model 模型， interpretion：实例）

检查模型

以下示例显示了检查模型的基本方法。

输入：

1
2
3
4
5
6
7
8
9
10
11
x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
print s.check()

m = s.model()
print "x = %s" % m[x]

print "traversing model..."
for d in m.decls():
    print "%s = %s" % (d.name(), m[d])

输出：

1
2
3
4
5
6
sat
x = 3/2
traversing model...
z = 0
y = 2
x = 3/2

在上面的例子中，函数Reals('x y z')创建变量 x，y和z。 它是以下三句话的缩写：

1
2
3
x = Real('x')
y = Real('y')
z = Real('z')

注意Reals 加了s

表达式m [x]返回模型m中对x的解释。 表达式“％s=％s”％(d.name()，m [d])返回一个字符串，其中第一个％s被替换为d的名字（即d.name（）），第二个 ％s用文本表示d的解释（即m [d]）。 Z3Py在需要时自动将Z3对象转换为文本表示。(这是python的写法)

ARITHMETIC 算术

Z3支持实数和整数变量。 它们可以混合在一个单一的问题中。 和大多数编程语言一样，Z3Py会自动添加强制转换，在需要时将整数表达式转换为真正的表达式。

以下示例演示声明整数和实变量的不同方法。

整数/实数变量

输入：

1
2
3
4
5
6
x = Real('x')
y = Int('y')
a, b, c = Reals('a b c')
s, r = Ints('s r')
print x + y + 1 + (a + s)
print ToReal(y) + c

输出：

1
2
x + ToReal(y) + 1 + a + ToReal(s)
ToReal(y) + c

函数ToReal将整型表达式转换为实型表达式。

Z3Py支持所有基本的算术运算。

算数运算

输入：

1
2
3
4
5
6
a, b, c = Ints('a b c')
d, e = Reals('d e')
solve(a > b + 2,
      a == 2*c + 10,
      c + b <= 1000,
      d >= e)

输出：

1
[b = 0, c = 0, e = 0, d = 0, a = 10]

Simplify

simplify命令对Z3表达式应用简单的转换。

输入

1
2
3
4
5
6
7
x, y = Reals('x y')
# Put expression in sum-of-monomials form
t = simplify((x + y)**3, som=True)
print t
# Use power operator
t = simplify(t, mul_to_power=True)
print t

输出：

1
2
x*x*x + 3*x*x*y + 3*x*y*y + y*y*y
x**3 + 3*x**2*y + 3*x*y**2 + y**3

help_simplify

help_simplify() 命令打印所有可用的选项。 Z3Py允许用户以两种风格书写选项。 Z3内部选项名称以：开头，单词之间用 - 分隔。 这些选项可以在Z3Py中使用。 Z3Py还支持类似Python的名称，其中：被压缩并且被_替换。

以下示例演示如何使用这两种样式。

输入：

1
2
3
4
5
6
7
8
x, y = Reals('x y')
# Using Z3 native option names
print simplify(x == y + 2, ':arith-lhs', True)
# Using Z3Py option names
print simplify(x == y + 2, arith_lhs=True)

print "\nAll available options:"
help_simplify()

输出：

1
2
3
4
5
x + -1*y == 2
x + -1*y == 2

All available options:
# 省略了，内容太多，请读者自行打印

rith-lhs参数被设置成True（default：False），意味着所有参数都放在左手边，右手边只留下常数constant。

无理数、任意大

Z3Py支持任意大的数字。 以下示例演示如何使用较大的整数，有理数和无理数执行基本算术。 Z3Py仅支持代数无理数。 代数无理数对于呈现多项式约束系统的解是足够的。 Z3Py将始终以十进制符号显示无理数，因为它更便于阅读。 内部表示可以使用sexpr（）方法提取。 它以s表达式（Lisp-like）的形式显示数学公式和表达式的Z3内部表示。

输入：

1
2
3
4
5
6
7
8
x, y = Reals('x y')
solve(x + 10000000000000000000000 == y, y > 20000000000000000)

print Sqrt(2) + Sqrt(3)
print simplify(Sqrt(2) + Sqrt(3))
print simplify(Sqrt(2) + Sqrt(3)).sexpr()
# The sexpr() method is available for any Z3 expression
print (x + Sqrt(y) * 2).sexpr()

输出：

1
2
3
4
5
[y = 20000000000000001, x = -9999979999999999999999]
2**(1/2) + 3**(1/2)
3.1462643699?
(root-obj (+ (^ x 4) (* (- 10) (^ x 2)) 1) 4)
(+ x (* (^ y (/ 1.0 2.0)) 2.0))

MACHINE ARITHMETIC 机器算术

现代CPU和主流编程语言使用固定大小的位向量进行算术运算。 机器算术在Z3Py中可用作位向量。 它们实现无符号和有符号二补数算术的精确语义。

位向量

以下示例演示如何创建位向量变量和常量。

函数BitVec('x'，16)在Z3中创建一个位向量变量，名称为x，具有16位。 为了方便起见，可以使用整型常量在Z3Py中创建位向量表达式。 函数BitVecVal(10,32)创建一个大小为32的位向量，其值为10。

输入：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
x = BitVec('x', 16)
y = BitVec('y', 16)
print x + 2
# Internal representation
print (x + 2).sexpr()

# -1 is equal to 65535 for 16-bit integers 
print simplify(x + y - 1)

# Creating bit-vector constants
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print simplify(a == b)

a = BitVecVal(-1, 32)
b = BitVecVal(65535, 32)
# -1 is not equal to 65535 for 32-bit integers 
print simplify(a == b)

输出：

1
2
3
4
5
x + 2
(bvadd x #x0002)
65535 + x + y
True
False

与诸如C，C ++，C＃，Java等编程语言相比，有符号和无符号的位向量之间没有区别。 相反，Z3提供了算术运算的特殊符号版本，无论位向量是有符号还是无符号都是有区别的。 在Z3Py中，运算符<，<=，>，> =，/，％和>>对应于有符号的版本。 相应的，无符号运算符是ULT，ULE，UGT，UGE，UDiv，URem和LShR。

输入：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)

solve(x + y == 2, x > 0, y > 0)

# Bit-wise operators
# & bit-wise and
# | bit-wise or
# ~ bit-wise not
solve(x & y == ~y)

solve(x < 0)

# using unsigned version of < 
solve(ULT(x, 0))

输出：

1
2
3
4
[y = 1, x = 1]
[y = 4294967295, x = 0]
[x = 4294967295]
no solution

位移运算

算子>>是算术右移，而<<是左移。 位移符号是左结合的。

输入：

1
2
3
4
5
6
7
8
9
# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)

solve(x >> 2 == 3)

solve(x << 2 == 3)

solve(x << 2 == 24)

输出：

1
2
3
[x = 12]
no solution
[x = 6]

FUNCTIONS 函数

在常见的编程语言中，函数具有副作用，可以抛出异常或永不返回。但在Z3中，函数是没有副作用的，并且是完全的。也就是说，它们是在所有输入值上定义的。比如除法函数。 Z3是基于一阶逻辑的。

给定一个约束，如x + y > 3，我们说x和y是变量。在许多教科书中，x和y被称为未解释的常量。也就是说，它们允许任何与约束x + y> 3一致的解释。

更确切地说，纯粹的一阶逻辑中的函数和常量符号是不解释的（uninterprete）、或自由的（free），这意味着没有附加先验解释。这与属于理论特征的函数形成对比，例如函数+具有固定的标准解释（它将两个数字相加）。不解释的函数和常量能够达到最大程度地灵活；它们允许任何与函数或常数约束相一致的解释。

为了说明未解释的函数和常量，让我们用一个例子来说明。

输入：

1
2
3
4
x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
solve(f(f(x)) == x, f(x) == y, x != y)

输出：

1
[x = 0, y = 1, f = [0 -> 1, 1 -> 0, else -> 1]]

设不解释的整数常量（又名变量）x，y；设f是一个不解释函数，它接受一个类型（又名 sort）整数的参数并生成一个整数值。这个例子说明了如何强制一个解释，其中f再次应用于x导致x，但是f应用于x不同于x。对于 f 的解（Interpretation）应该被解读为：

f（0）= 1，f（1）= 0，并且对于全部不同于0和1的a， f（a）=1。

在Z3中，我们也可以评估模型中的约束系统表达式。 以下示例显示如何使用评估方法。

输入：

1
2
3
4
5
6
7
8
9
x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
s = Solver()
s.add(f(f(x)) == x, f(x) == y, x != y)
print s.check()
m = s.model()
print "f(f(x)) =", m.evaluate(f(f(x)))
print "f(x)    =", m.evaluate(f(x))

输出：

1
2
3
sat
f(f(x)) = 0
f(x)    = 1