我正在尝试执行以下求解器:
solver = Solver()
f = z3.Function('f', IntSort(), IntSort())
y = z3.Int('y')
solver.add(f > y)
print(solver.check())
并且我收到以下异常:
z3.z3types.Z3Exception:Python值不能用作Z3整数
在此行:
solver.add(f > y)
我是Z3的新手,也许我理解错了。
正如克里斯托夫(Christoph)所述,您不能将函数与数字进行比较,无论该数字是大于/小于还是等于。这确实与z3无关。作为数学陈述意味着什么?
假设您要说的是希望f
对于可以接收的任何输入产生一个大于y
的值,则可以这样编码:
from z3 import *
s = Solver()
f = Function('f', IntSort(), IntSort())
y = Int('y')
x = Int('x')
s.add(ForAll([x], f(x) > y))
if s.check() == sat:
print(s.model())
else:
print("not sat")
这显示了相当有趣的模型:
[y = 0, f = [else -> 1]]
将y
设置为0
,并且f
始终返回1
的常数函数;但至少类型正确。
这是您的追求吗?
在我的问题中,函数参数是常量,因此不需要通用量词。我也忘记声明函数中使用的常量。
from z3 import *
s = Solver()
f = Function('f', IntSort(), IntSort())
y = Int('y')
x = Int('x')
z = Int('z')
s.add(f(x,z) > y)
if s.check() == sat:
print(s.model())
else:
print("not sat")