了解Z3中遍历的量词

Question

我正在尝试了解Z3中的量化公式（我正在使用Z3PY）。不知道如何拾取量化变量。例如，在下面显示的代码中，我正在尝试打印相同的公式并获取错误。

from z3 import *
def traverse(e):
  if is_quantifier(e):
    var_list = []
    if e.is_forall():
        for i in range(e.num_vars()):
            var_list.append(e.var_name(i))
        return ForAll (var_list, traverse(e.body()))
x, y = Bools('x y')
fml =  ForAll(x, ForAll (y, And(x,y)))
same_formula = traverse( fml ) 
print same_formula

几乎没有搜索，我知道Z3使用de bruijn索引，我必须得到var（1，boolsort（））之类的东西。我可以想到使用var_sort（），但是如何使公式正确返回变量。在这里呆了一段时间。

Answer 1

var_list是字符串列表，但ForAll期望常数列表。另外，当它不是量词时，traverse应返回e。这是一个修改后的示例：

from z3 import *
def traverse(e):
  if is_quantifier(e):
    var_list = []
    if e.is_forall():
        for i in range(e.num_vars()):
            c = Const(e.var_name(i) + "-traversed", e.var_sort(i))
            var_list.append(c)
        return ForAll (var_list, traverse(e.body()))
  else:
    return e
x, y = Bools('x y')
fml =  ForAll(x, ForAll (y, And(x,y)))
same_formula = traverse( fml ) 
print(same_formula)