概述

  最近做逆向题，有很多线性方程需要用该库进行求解，故写篇博客记录一下。

z3库的安装

$ pip install z3
# 上面命令失败的话可以尝试
$ pip install z3_solver

申明求解变量范围

from z3 import *

# a为整数解，Ints用于一次性申请多个
a = Int("a")
a, b = Ints("a b")

# 有理数解
a = Real("a")
a, b = Reals("a b")

# 位向量，用于求解与/或/移位等位运算
# 第二个参数表示位数
a = BitVec("a", 8)
a, b = BitVecs("a b", 8)

增加方程约束与求解

from z3 import *

a, b = Ints("a b")
s = Solver()
equs = [a+b==10, a-b==6]
s.add(equs)
print(s.check())   # sat代表有解，unsat代表无解
print(s.model())

"""
sat
[a = 8, b = 2]
"""

总结

不忘初心，砥砺前行！