如何在 Z3(Py) 中输出多个 Skolem 函数

Question

我在 Z3-Py 中使用 Skolem 函数。在接下来的几行中，我描述了 Skolem 函数，它满足在整数上解释的公式 Forall x. Exists y. (x>=2) --> (y>1) /\ (y<=x)：

x = Int('x')

skolem = Function('skolem', IntSort(), IntSort())

ct_0 = (x >= 2)
ct_1 = (skolem(x) > 1)
ct_2 = (skolem(x) <= x)

phi = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))

s = Solver()
s.add(phi)
print(s.check())
print(s.model())

据我所知，它可能输出唯一的“模型”：y=2（即f(x)=2）。打印如下：

sat
[skolem = [else -> 2]]

我有一个初步的问题：为什么函数使用else？我想这是因为如果先行词(x>=2)成立，“它只会被激活”。但是，如果激活的不是else分支（输出2），而是if分支，那么哪个是函数的共同域？

但现在我的实际问题来了.我解决了相同的公式，但解释了实数：

x = Real('x')

skolem = Function('skolem', RealSort(), RealSort())

ct_0 = (x >= 2.0)
ct_1 = (skolem(x) > 1.0)
ct_2 = (skolem(x) <= x)

phi = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))

s = Solver()
s.add(phi)
print(s.check())
print(s.model())

这输出...相同的 Skolem 函数！这是正确的吗？

万一是，它仍然很好奇，因为它本可以选择许多其他的；例如，y=1.5。然后，我想为 Z3 请求另一个 Skolem 函数，所以我继续处理，就好像我在请求 5 个新模型：

phi = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))

s = Solver()
s.add(phi)
for i in range(0,5):
  if s.check() == sat:
    m = s.model()
    print(m)
    s.add(Not(m))

但我收到以下错误：Z3Exception: True, False or Z3 Boolean expression expected. Received [skolem = [else -> 2]] of type <class 'z3.z3.ModelRef'>. 我的意思是，我看到 Z3 期望布尔值用于否定（这很明显呵呵），所以我如何编码“我将此 Skolem 函数的否定添加到公式中”这一事实，即，我想找到另一个 Skolem 函数？

Answer 1

在你的循环中，你试图添加你的模型m的否定；但这不是Not(m) 的意思。事实上，Not(m) 是没有意义的：Not 操作布尔值，而不是模型；这是你得到的奇怪错误。

做你想达到的目标；简单地断言你想要一个不同的 skolem 函数：

from z3 import *

x = Real('x')

skolem = Function('skolem', RealSort(), RealSort())

ct_0 = (x >= 2)
ct_1 = (skolem(x) > 1)
ct_2 = (skolem(x) <= 2)

phi = ForAll([x], Implies(ct_0, And(ct_1,ct_2)))

s = Solver()
s.add(phi)

for i in range(0, 5):
  if s.check() == sat:
    m = s.model()
    print(m)
    s.add(skolem(x) != i)

这打印：

[skolem = [else -> 2]]
[x = 0, skolem = [else -> If(2 <= Var(0), 2, 1/2)]]
[x = 0, skolem = [else -> If(2 <= Var(0), 2, 1/2)]]
[x = 0, skolem = [else -> If(2 <= Var(0), 3/2, 1/2)]]
[x = 0, skolem = [else -> If(2 <= Var(0), 3/2, 1/2)]]

现在这有点难以阅读，但我认为你可以理解。函数模型只是带有 else 子句的有限映射，这就是有限函数。 Var 调用引用其参数。我没有详细查看 z3 提供的定义以确保它们是好的，但我没有理由怀疑为什么不这样做。看看你能不能自己解决这个问题；这是一个有价值的练习！如果有任何不清楚的地方，请随时提出进一步的问题。