Z3-Solver

创建声明

x = Int('x')       #声明整数
x = Real('x')      #声明实数
x = Bool('x')      #声明布尔类型
x = BitVec('x', 8) #声明位向量类型
a, b, c = Reals('a b c')  #批量声明

//Int类型无法使用& | ~计算

常用API

1. 创建约束求解器

solver = Solver()

2. 添加约束条件

solver.add()

3. 判断解是否存在

if(solver.check() == sat)

4. 求解

print(solver.model())