Z3定量化された式の変数の数を数えて

Question

私は数式（Z3pyの定量化された式）ですべての変数を収集しようとしています。小さな例

w, x, y, z = Bools('w x y z') 
fml = And(ForAll(x, ForAll(y, And(x, y))), ForAll(z, ForAll(w, And(z, w)))) 

varSet = traverse(fml) 

iが横断するために使用するコードは

def traverse(e): 
    r = set() 
    def collect(e): 
    if is_quantifier(e): 
     # Lets assume there is only one type of quantifier 
     if e.is_forall(): 
      collect(e.body()) 
    else: 
     if (is_and(e)): 
      n = e.num_args() 
      for i in range(n): 
       collect(e.arg(i)) 
     if (is_or(e)): 
      n = e.num_args() 
      for i in range(n): 
       collect(e.arg(i)) 
     if (is_not(e)): 
      collect(e.arg(0)) 
     if (is_var(e)): 
      r.add(e) 
    collect(e) 
    return r 

と私は取得してい：セット（[ヴァー（0）、ヴァー（1）]）を。これはZ3がDe Bruijn indexを使用しているためです。これを避けて、所望のセットを得ることができるか：セット（[Var（0）、Var（1）、Var（2）、Var（3）]）。

Answer 1

コードは正しいです。この例ではVar(2)またはVar(3)はありません。 2つの最上位の量指定子があり、それぞれのde-Bruijnインデックスは0と1です。これらの2つの量子は、別の量指定子の本体内には現れないので、混乱することはありません。