Z3

什么是Z3

Z3是一个微软出品的开源约束求解器。

from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print(s.check())
print(s.model())