理解Z3中绑定变量的索引

Question

我试图了解绑定变量是如何编入索引的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有一个mkBoundapi用于创建带有index和sort作为参数的绑定变量.我不确定我应该将哪个值传递给index参数.所以,我想知道以下内容:

如果我有两个公式phi1,并phi2用最大变量绑定的索引n1和n2,这将是指数x的ForAll(x, And(phi1, phi2))

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

Answer 1

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)