Z3约束器使用流程
目录z3基本数据类型
Int #整型
Bool #布尔型
Array #数组
BitVec('a',8) #char型
其中BitVec可以是特定大小的数据类型，不一定是8，例如C语言中的int型可以用BitVec(a',32)表示
例如:x = Int('x') #这个int不是c/c++中的那个四字节，而仅仅只代表整数
y = Real(y') #实数变量(数学中的那个实数)
z = BitVec('z',8) #char型
m = BitVec('m',32) #int型
n = Bool('n') #定义布尔型
初始化未知数序列
flag =[BitVec('x%d'%i,8) for i in range(32)] #char型序列
flag= [Int('%d'%i) for i in range(32)] #int型整数序列
flag =[BitVec('x%d'%i,32) for i in range(32)] #int型序列
z3求解四步骤
1.创建约束求解器
s = Solver()
Solver()命令会创建一个通用求解器，创建后我们可以添加我们的约束条件，进行下一步的求解
添加约束
2.s.add
add0命令用来添加约束条件，通常在solver()命令之后，添加的约束条件通常是一个逻辑等式
3.判断解是否存在
if s.check( )==sat:
该函数通常用来判断在添加完约束条件后，来检测解的情况，有解的时候会回显sat，无解的时候会
unsat
4.求解
print(s.model( ))
在存在解的时候，该函数会将每个限制条件所对应的解集的交集，进而得出正解
CTF中的Z3模板
from z3 import *
s=Solver()
flag = [BitVec(('x%d' % i), 8) for i in range(len(flag))]
for i in range(0, len(flag))
s.add(flag[i] <= 127)
s.add(flag[i] >= 32)
#中间添加程序的加密正向算法
if s.check() == sat:
model = s.model()
string = [chr(model[flag[i]].as_long()) for i in range(len(flag))]
print("".join(string))
exit()