Understanding Quantifier Passing in Z3

Question

I am trying to understand the passed quantitative formula in z3 (I am using z3py). I don’t know how to choose quantitative variables. For example, in the code below, I am trying to print the same formula and get an 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 a little searching, I found out that z3 uses the De Bruijn index, and I need 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 a while.

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)