[Python知识库]CTF Re-Python z3库的使用

一 安装：

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)