Python z3_python z3多线程

Z3

这学期好忙，之前学的都没时间做记录
今天看一个师傅在GitHub上的WP看到了这个库，之后大概学了一下，了解到这个库是用来解决带限制条件的方程组，在密码学中要用到的语法也比较少，简单记录一下
r00ta.

初始化

单独定义一个变量时，Int表示整数，Real表示有理数，BitVec表示位向量。
在末尾加 ”s"可以用来同时定义多个变量，注意使用BitVec时需要加位数。

求解

.Solver()创造一个求解器，用于之后添加限制条件
.add()进行添加限制条件
.check()用于判断是否有解，有解返回sat，无解返回unsat
.model()在有解时返回解

举例：

from z3 import *
x=Int('x')
a,b,c=BitVecs('a b c',10)
s=Solver()
s.add(a-b == 17)
s.add(a+c == 25)
s.add(c-b == 12)
print(s.check())
print(s.model())
1
2
3
4
5
6
7
8
9

结果：

sat
[b = 510, c = 522, a = 527]
1
2

z3语法链接