0x00 前言

在做逆向题目时，很多线性方程需要用z3库进行求解，写篇博客具体了解一下

69104c0115c532f0107e5ca58a4a233.png

0x01 z3库的安装

1
2
3
pip install z3
or
pip install z3-solver

0x02 z3库的使用

  1. 创建一个解的声明对象：
1
s = Solver()
  1. 添加条件：
1
s.add(判断公式)
  1. 判断是否有解：
1
2
s.check()
# 若有解，则返回 sate/sat 反之则返回 unsate/unsat
  1. 返回最后的解：
1
2
3
result = s.modul()

print(result)
  1. 声明不同类型的未知数：
1
2
3
4
a, s, d = Ints('a s d')#创建一个‘int’类型的对象，但其实运算时候是'ArithRef'类型，
                       #并且无法使用按位运算
x = Real('x')#创建一个有理数类型的变量。
y = Real('y')
  1. 求解按位运算（⭐）：
1
2
3
4
5
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),创建一个位向量，有初始值，没名字
  1. 特殊代码：
1
2
numbers = [BitVec(chr(i), 8) for i in range(0, 4)]
声明一个数组