Z3Py的Lambda函数

Question

我的目标是在Z3Py中找到一个构造，它允许我：(1)将命题写成变量的函数。在理论上，如果我定义P(x) =x< 3，那么代码应该允许我访问其他变量u的P(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_()存储“未知”而不存储“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是一个内部自由变量生成函数。这不是一个应该来回传递给z3的对象；实际上，我认为您正在成为z3松散类型性质的牺牲品；这是一个完全没有意义的构造。长话短说，您不应该在自己的代码中查看P.body()或I.body()。在这个上下文中，我会忽略unknown结果；输入或多或少是毫无意义的，z3给出了一个毫无意义的答案。一个更好的系统应该对此进行检查和抱怨；但这并不是Z3的Python的强项。

(2)如果使用正则函数，这根本不是一个问题；因为您只是在Python级别上执行常规应用程序。您也可以通过直接调用lambda绑定值来应用它，但您需要使用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函数的使用，它通过每次调用时提供唯一的名称来避免名称冲突。