z3求解器

(Updated: )

介绍

z3是一个开源的约束求解器，在处理一些给定一定约束条件求解我们需要的一组特定解的时候非常有效 ### 安装 

1
pip install z3-solver
### 示例 
1
2
3
4
5
from z3 import *
x = Int('x')#定义整型
y = Int('y')
solve(x > 10, y == x + 2, y < 15)#在约束条件较少的情况下solve可以直接帮我们找到一组对应解，并且也只会返回一组对应解
print(solve)
### 常用示例 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
from z3 import *

x = Int('x')
y = Real('y')
z = BitVec('z', 32)
p = bool('p')

s = z3.solver()#创建一个求解器，也就是一组约束的集合
s.add(x + y == 10, x - y == 5)#添加约束条件
print(s.check())#检查是否有解
z3.sat #约束可以被满足
z3.unsat #约束不被满足

print(s.model())#输出解，只有一组对应解