Z3Py中的Z3解f(x)> y引发异常

问题描述 投票:0回答:2

我正在尝试执行以下求解器:

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的新手,也许我理解错了。

python z3
2个回答
1
投票

正如克里斯托夫(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的常数函数;但至少类型正确。

这是您的追求吗?


0
投票

在我的问题中,函数参数是常量,因此不需要通用量词。我也忘记声明函数中使用的常量。

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")
© www.soinside.com 2019 - 2024. All rights reserved.