Z3の量子トラバースの理解

Question

z3の定量化された数式をトラバースすることを理解しようとしています（私はz3pyを使用しています）。定量化された変数をどのようにピックアップするか分かりません。たとえば、以下のコードでは、私はと同じ式とエラーを表示しようとしています。私はZ3はド・ブラン・インデックスを使用し、私はヴァール（1、BoolSort（））のようなものを取得する必要があることを知るようになった少し検索して

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 

。私は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)