（：VAR 0）Z3数量詞の体内に

Question

私はZ3 OCamlのAPIの数量詞の身体、その文字列である

(exists ((u_1 Int)) (= u_1 x5)) 

はQuantifier.get_bodyによって、私は発現を得る例えば数量詞を取得すると

(= (:var 0) x5) 

この式では、u_1の名前は新しく変わった変数に変更されているようですが、式の種類（：var 0）とそれをどのように戻すかはわかりませんそのボディとそのバインドされた変数からQuantifierを再構築したいときには、u_1を使用します。

誰も解決策を提案できますか？どうもありがとうございました。

Answer 1

私は解決策を得ました。式

(:var 0) 

は、VAR_ASTの式です。あなたは、インデックスで

Quantifier.get_index e 

により、例えばそのインデックス、0を得ることができ、その後

AST.is_var (Expr.ast_of_expr e) 

により確認することができ、簡単にそのバインドされた変数に式eを一致させることができます。量限定子の束縛変数のリストは、次の式で得られることに注意してください。

Quantifier.get_bound_variable_names