Z3Py 的 Lambda 函数

Question

我的目标是在 Z3Py 中找到一个结构，它允许我： (1) 将命题写成变量的函数。例如，理论上，如果我定义 P(x) = x < 3，那么代码应该允许我访问 P(u) 以获取其他变量 u。 (2) 而Z3应该能够解决并找到这样一个构造的模型。

我认为 Z3 的 'Lambda' 功能在理论上是有道理的。但是，对于这种构造，我不能执行 (1) 或 (2)。作为一个具体的例子，假设我有以下代码：

u, x = Ints('u x')
P = Lambda( [x], x < 5 )
I = Lambda ([x], x < 3)
C1 = Not(Implies(P.body(), I.body() ))
s = Solver()
s.add(C1)
r = s.check()
print(r.__repr__())
s.add( Implies(P(u), u == 2) )

运行此代码获取输出：

unknown
Traceback (most recent call last):
  File "testfile.py", line 20, in <module>
    s.add( Implies(P(u), u == 2) )
TypeError: 'QuantifierRef' object is not callable

这里有两个问题需要解决：

(1) 为什么 r._ repr_() 存储了 'unknown' 而不是 'sat' 即为什么 Z3 没有解决这个系统？

(2) 在最后一行中，如何从 P 中获取谓词 u < 5，即在 lambda 演算术语中，如何将函数应用于 Z3Py 中的变量？显然 P(u) 不起作用。

Answer 1

对于这种建模，您应该简单地使用常规 python 函数：

from z3 import *

def P(x):
    return x < 5

def I(x):
    return x < 3

然后，要证明 Q(x) => P(x)，您需要使用量词：

dummy = Int('dummy')
C1 = ForAll([dummy], Implies(I(dummy), P(dummy)))
prove(C1)

这会打印：

proved

关于您的具体问题：

(1) 添加 Implies(P.body(), Q.body()) 意味着完全不同的东西。如果你运行:

from z3 import *
x = Int('x')
P = Lambda( [x], x < 5 )
I = Lambda( [x], x < 3 )
s = Solver()
s.add(Implies(P.body(), I.body()))
print(s.sexpr())

您会看到它打印：

(assert (=> (< (:var 0) 5) (< (:var 0) 3)))

其中 :var 是内部 free-variable 生成函数。这不是您应该来回传递给 z3 的对象；事实上，我认为您正在成为 z3 松散类型特性的受害者；这根本不是一个真正有意义的结构。长话短说，您永远不应该在自己的代码中查看 P.body() 或 I.body()。在这种情况下，我会忽略 unknown 结果；输入或多或少没有意义，z3 吐出一个无意义的答案。一个更好的系统应该对此进行检查和抱怨；但这不是 z3 的强项 Python API.

(2) 如果您使用常规函数，这根本不是问题；因为您只是在 Python 级别进行常规应用。您可以通过直接调用它来应用 lambda-bound 值，尽管您需要符号 P[u]。（Lambda 类似于 z3 中的数组。）所以，类似于：

from z3 import *

u, x = Ints('u x')
P = Lambda([x], x < 5)
I = Lambda([x], x < 3)
s = Solver()
s.add(Implies(P[u], u == 2))
print(s.check())
print(s.model())

将打印：

sat
[u = 2]

我想这就是你要找的。

多个参数

如果您想为具有多个参数的 lambda 建模，最简单的方法是将其视为嵌套结构。也就是说，您在每个索引处存储一个新的 lambda。这是一个例子：

from z3 import *

dummy1 = FreshInt()
dummy2 = FreshInt()
P = Lambda([dummy1], Lambda([dummy2], dummy1 < dummy2))

s = Solver()

x, y = Ints('x y')
s = Solver()
s.add(P[x][y])
print(s.check())
print(s.model())

这会打印：

sat
[y = 1, x = 0]

注意，上面还演示了FreshInt函数的使用，它通过在每次调用时提供一个唯一的名称来避免name-clashes。

Z3Py 的 Lambda 函数

Lambda Functions for Z3Py

z3

z3py

多个参数