from z3 import *
#定义类型
x = Int('x')
y = Int('y')
z = Int('z')
#创建求解器
s = Solver()
#添加约束条件
s.add(y==2*x-7)
s.add(5*x+3*y+2*z==3)
s.add(3*x+z==7)
print s.check() #检测条件是否OK
print s.model() #列出求解结果
sat #列出求解满足条件值
标签：求解,Int,check,add,print,列出,Z3
来源： https://www.cnblogs.com/0xHack/p/11583731.html