参考资料：

1. Z3 API IN PYTHON 中文文档

1. Z3安装

linux安装Z3

git clone https://github.com/angr/angr-z3.git
cd angr-z3
python scripts/mk_make.py
cd build
make
sudo make install

其中第三个命令有参数，自定义z3包的安装位置

python scripts/mk_make.py --prefix=/home/palmer --python --pypkgdir=/home/palmer/.local/lib/python2.7/site-packages

python scripts/mk_make.py --prefix=想安装到的目录 --python --pypkgdir=你的python第三方库地址
prefix 我设置的用户根目录
pypkgdir 去找python的包目录

2. Z3语句

2.1. Z3语句基础

2.2. Z3语句讲解

2.2.1. Z3简单使用例子

from z3 import *
x = Int('x')  #声明未知数，类型是整数类型Int
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)
# 输出 [y = 0, x = 7]

先定义了两个未知数x和y，类型是Z3内置的整数类型Int
solve() 函数会创造一个 solver，然后对括号中的约束条件进行求解，在 Z3 默认情况下只会找到满足条件的一组解。

2.2.2. 声明未知数

1. 声明整数x = Int('x')
2. 声明实数x = Real('x')
3. 声明布尔类型x = Bool('x')
   批量声明未知数加s
   例：

a, b, c = Reals('a b c')  #声明3个实数
x, y, z = Ints('x y z')   #声明3个整数

更改类型

1. IntVal() 返回Z3整数
2. RealVal() 返回Z3实数
3. RatVal() 返回Z3有理数值

2.2.3. simplify()函数—对表达式进行化简

>>> simplify(x + y + 2*x + 3)
3 + 3*x + y 

>>>> simplify(x < y + x + 2)
Not(y <= -2) 

>>>> simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
And(x >= 2, 2*x**2 + y**2 >= 3) 

>>>> simplify((x + 1)*(y + 1))
(1 + x)*(1 + y) 

>>>> simplify((x + 1)*(y + 1), som=True) # sum-of-monomials： 单项式的和
1 + x + y + x*y

>>>> t = simplify((x + y)**3, som=True) 
>>>> t
x*x*x + 3*x*x*y + 3*x*y*y + y*y*y

>>>> simplify(t, mul_to_power=True) # mul_to_power 将乘法 转换成乘方
x**3 + 2*y*x**2 + x**2*y + 3*x*y**2 + y**3

simplify(<表达式>)  #对表达式进行化简
simplify(<表达式>,som=True)   #sum-of-monomials： 单项式的和 将表达式转成单项式的和
simplify(<表达式>,mul_to_power=True)   # mul_to_power 将乘法转换为乘方

simplify() 函数用于对表达式进行化简，同时可以设置一些选项来满足不同的要求。
更多选项使用 help_simplify() 获得。

2.2.4. set_param()函数配置全局变量

>>> x = Real('x')
>>> y = Real('y')
>>> solve(x**2 + y**2 == 3, x**3 == 2)
[x = 1.2599210498?, y = -1.1885280594?]

>>> set_param(precision=30)
>>> solve(x**2 + y**2 == 3, x**3 == 2)
[x = 1.259921049894873164767210607278?, y = -1.188528059421316533710369365015?]

set_param(precision=30)  #保留30位的小数

set_param(rational_to_decimal=True) # 以十进制形式表示有理数

2.2.5. Q(a, b) 返回有理数 a/b

Q(a, b) 返回有理数 a/b

2.2.6. solver类系列

>>> from z3 import *
>>> x = Int('x')
>>> y = Int('y')
>>> s = Solver()
#创造一个通用solver
>>> type(s)
# Solver 类
<class ' Z3. z3. Solver'>

>>> s.add(x>10,y==x+2)  #添加约束到solver 中
>>> s
[x>10,y==x+2]
>>> s.check()   #检查solver中的约束 是否满足
sat   # satisfiable/满足

>>> s. push( )   #创建一个回溯点，即将当前栈的大小保存下来

>>> s.add(y < 11)
>>> s
[x>10,y==x+2，y<11]
>>> s.check()
unsat   # unsatisfiable/不满足
>>> s. pop(num=1)   #回溯num个点
>>> s
[x>10，y==X+2]
>>> s. check()
sat
>>> for C in s.assertions():
# assertions() 返回一个包含所有约束的AstVector

>>> s. statistics( )
# statistics() 返回最后一个check() 的统计信息
(   :max- memory	 6.26
	:memory  		 4.37
	:mk -bool -var	 1
	:num- al locs	331960806
	:rlimit-count 7016)
>>> m = s.model( )   # model() 返回最后一个check() 的model
>>> type(m)   # ModelRef 类
<class ' Z3. z3. ModelRef '>
>>> m
[x=11,y=13]
>>> for d in m.dec1s():   # decls()返回model包含了所有符号的列表
print("%S = %S" % (d.name()，m[d]))
x=11
y =13

3. Z3约束器使用流程

1. 创建变量
   例：

x = Int('x') 
y = Int('y')

2. 创建solver求解器
   例：s = Solver()
3. 添加约束条件
   例：s.add(x+y==10)
4. 检查solver中的约束是否满足
   例：s.check()
5. 利用model()输出运算结果
   例：s.model()