理解 Z3 中绑定变量的索引 [英] Understanding the indexing of bound variables in Z3

问题描述

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

I am trying to understand how the bound variables are indexed in z3. Here in a snippet in z3py and the corresponding output. ( 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有不同的index.(0 and 1).如果我修改 f1 并带出 Exists，则 x 具有相同的索引(0).

In f1, why is the same bound variable x has different index.(0 and 1). If I modify the f1 and bring out the Exists, then x has the same index(0).

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

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

I have a FOL formula represented in a DSL in scala that I want to send to z3. Now ScalaZ3 has a mkBound api for creating bound variables that takes index and sort as arguments. I am not sure what value should I pass to the index argument. So, I would like to know the following:

如果我有两个公式 phi1 和 phi2，它们的最大绑定变量索引为 n1 和 n2，为x在ForAll(x, And(phi1, phi2))

If I have two formulas phi1 and phi2 with maximum bound variable indexes n1 and n2, what would be the index of x in ForAll(x, And(phi1, phi2))

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

Also, is there a way to show all the variables in an indexed form? f1.body() just shows me x in indexed form and not y. (I think the reason is that y is still bound in f1.body())

推荐答案

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

Z3 encodes bound variables using de Bruijn indices. The following wikipedia article describes de Bruijn indices in detail: http://en.wikipedia.org/wiki/De_Bruijn_index Remark: in the article above the indices start at 1, in Z3, they start at 0.

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

Regarding your second question, you can change the Z3 pretty printer. The Z3 distribution contains the source code of the Python API. The pretty printer is implemented in the file python\z3printer.py. You just need to replace the method:

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 漂亮的打印机，你也应该替换.

If you want to redefine the HTML pretty printer, you should also replace.

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)

这篇关于理解 Z3 中绑定变量的索引的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！