一 安装：
z3是由微软公司开发的一个优秀的SMT求解器（也就定理证明器），它能够检查逻辑表达式的可满足性。
我是在windows下pyCharm 里面自己添加包 包名为z3-slover（不是z3）
二 使用：
库内函数：
1.创建一个解的声明对象：
a = Solver()
2.添加条件：
s.add(判断公式)
3.判断是否有解：
s.check()
如果有解 则反回sate 反之 返回 unsate
4.返回最后的解：
result=s.modul() print(result)
5.声明不同类型的未知数：
a, s, d = Ints('a s d')#创建一个‘int’类型的对象，但其实运算时候是'ArithRef'类型，
#并且无法使用按位运算
x = Real('x') #创建一个有理数类型的变量。
y = Real('y')
z3库最牛逼的来了:上面两个就是比正常多元未知数复杂了点，求解按位运算才是这个库最吊的！
BitVecs(name,bv,ctx=None),创建一个有多变量的位向量，name是名字，bv表示大小
#a,b,c=s=BitVecs('a b c',32)
Bitvex(name,bv,ctx=None),创建一个位向量，name是他的名字，bv表示大小
BitVecSort(bv,ctx=None),创建一个指定大小的位向量
BitVecVal(val,bv,ctx=None),创建一个位向量，有初始值，没名字
三：例题
大概使用流程：
from z3 import *
a, b, c=BitVecs('a b c',32)
d, e, f=BitVecs('d e f',32)
g, h, i=BitVecs('g h i',32)
key=[a,b,c,d,e,f,g,h]
s = Solver()
s.add()
check = s.check()
print(check)
model = s.model()
print(model)
