Understanding quantifier traversing in Z3

Question

I'm trying to understand traversing quantified formula in z3 (i'm using z3py). Have no idea how to pickup the quantified variables. For example in code shown below i'm trying to print the same formula and getting error.

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

With little search i got to know that z3 uses De Bruijn index and i have to get something like Var(1, BoolSort()). I can think of using var_sort() but how to get the formula to return the variable correctly. Stuck here for some time.

Answer 1

var_list is a list of strings, but ForAll expects a list of constants. Also, traverse should return e when it's not a quantifier. Here's a modified example:

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)