6

我试图了解绑定变量如何在z3. 这里有一个片段z3py和相应的输出。( http://rise4fun.com/Z3Py/plVw1 )

x, y = Ints('x y')
f1 = ForAll(x, And(x == 0, Exists(y, x == y)))
f2 = ForAll(x, Exists(y, And(x == 0, x == y)))
print f1.body()
print f2.body()

输出：

ν0 = 0 ∧ (∃y : ν1 = y)
y : ν1 = 0 ∧ ν1 = y

在f1中，为什么同一个绑定变量x有不同的索引。（0和1）。如果我修改f1并带出Exists，则x具有相同的索引（0）。

我想了解索引机制的原因：

我有一个 FOL 公式，用 scala 中的 DSL 表示，我想发送到z3. 现在ScalaZ3有一个mkBound用于创建将index和sort作为参数的绑定变量的 api。我不确定应该将什么值传递给index参数。所以，我想知道以下几点：

如果我有两个公式phi1并且phi2具有最大绑定变量索引n1和n2，那么 in 的索引是x多少ForAll(x, And(phi1, phi2))

另外，有没有办法以索引形式显示所有变量？f1.body()只是x以索引形式显示我，而不是y. （我认为原因是y仍然绑定在f1.body()）

4

1 回答 1

7

Z3 使用 de Bruijn 索引对绑定变量进行编码。以下维基百科文章详细描述了 de Bruijn 索引： http ://en.wikipedia.org/wiki/De_Bruijn_index 备注：在上面的文章中，索引从 1 开始，在 Z3 中，它们从 0 开始。

关于你的第二个问题，你可以更换 Z3 漂亮的打印机。Z3 发行版包含 Python API 的源代码。漂亮的打印机在文件中实现python\z3printer.py。您只需要替换方法：

def pp_var(self, a, d, xs):
    idx = z3.get_var_index(a)
    sz  = len(xs)
    if idx >= sz:
        return seq1('Var', (to_format(idx),))
    else:
        return to_format(xs[sz - idx - 1])

和

def pp_var(self, a, d, xs):
    idx = z3.get_var_index(a)
    return seq1('Var', (to_format(idx),))

如果你想重新定义 HTML 漂亮的打印机，你也应该替换。

def pp_var(self, a, d, xs):
    idx = z3.get_var_index(a)
    sz  = len(xs)
    if idx >= sz:
        # 957 is the greek letter nu
        return to_format('&#957;<sub>%s</sub>' % idx, 1)
    else:
        return to_format(xs[sz - idx - 1])

和

def pp_var(self, a, d, xs):
    idx = z3.get_var_index(a)
    return to_format('&#957;<sub>%s</sub>' % idx, 1)
于 2012-08-05T15:21:42.987 回答