1

したがって、量指定子を表す式で呼び出される Z3_get_quantifier_bound_name を使用して、量指定子の境界に関連付けられた名前を取得できます。しかし、量化されたサブフォーミュラの AST をトラバースしているとします。その時点でインデックスの名前にアクセスすることは可能ですか? ありがとうございました。

if (z3_expr.is_var())
{
    // is it possible at this point to get the name of the quantified variable, 
    // which was associated with it at quantifier creation?
}
4

1 に答える 1

1

変数である式には、名前が直接関連付けられていません。名前にアクセスする方法は、途中でトラバースされた量指定子からの名前のスタックを維持することです。したがって、シンボルのベクトル (スタック/リスト) を維持し、量指定子をトラバースするたびに、バインドされた名前を量指定子からベクトルにプッシュします。量指定子のトラバースが完了したら、名前をポップする必要があります。

次の API を使用して、バインドされた変数の名前にアクセスします。

 unsigned Z3_API Z3_get_quantifier_num_bound(__in Z3_context c, __in Z3_ast a);

 Z3_symbol Z3_API Z3_get_quantifier_bound_name(__in Z3_context c, __in Z3_ast a, unsigned i);

数量化された変数のインデックスは右から左に並べられることに注意してください。したがって、Z3_get_quantifier_num_bound(context, expr) が 2 を返し、x = Z3_get_quantifier_bound_name(context, expr, 0) y = Z3_get_quantifier_bound_name(context, expr, 1) の場合、y はインデックス 0 を持ち、x はインデックス 1 を持ちます。

于 2012-11-13T08:44:23.607 に答える