1

Z3 の Z3_ast のカスタム出力を C で書こうとしましたが、Z3_VAR_AST と Z3_FUNC_DECL_AST の Z3_ast_kind を管理する方法がわかりません。Z3_VAR_AST の Z3_sort (Z3_get_sort) を出力する方法しか知りません。私が持っているこの変数値についてアイデアはありません???. また、Z3_FUNC_DECL_AST については、関数名、パラメーターの数、およびパラメーターを取得できるアクセサーが見つかりませんでした。皆さん、私を助けてくれませんか? 乾杯

4

1 に答える 1

2

Z3ディストリビューションのファイル「python/z3printer.py」をご覧になることをお勧めします。Pythonでカスタムのきれいなプリンターを定義します。Z3 python APIは、CAPIの上の単なるレイヤーです。したがって、このプリンターをCに変換するのは簡単です。

についてZ3_VAR_ASTは、機能

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

変数のde-Brujinインデックスを返します。インデックスの意味はここで説明されています：http：//en.wikipedia.org/wiki/De_Bruijn_index 変数名は数量詞ASTに保存されます。名前はZ3とは無関係であることに注意してください。これらは、出力を適切にするためだけに保存​​されます。のコードはz3printer.py、変数名とのスタックを保持します。

に関してZ3_FUNC_DECL_ASTは、より扱いやすいですZ3_VAR_AST。この種のASTは実際にはZ3_func_declです。次に、次のAPIを使用して、必要な情報を抽出できます。

Z3_symbol Z3_API Z3_get_decl_name(__in Z3_context c, __in Z3_func_decl d);

Z3_decl_kind Z3_API Z3_get_decl_kind(__in Z3_context c, __in Z3_func_decl d);

unsigned Z3_API Z3_get_domain_size(__in Z3_context c, __in Z3_func_decl d);

unsigned Z3_API Z3_get_arity(__in Z3_context c, __in Z3_func_decl d);

Z3_sort Z3_API Z3_get_domain(__in Z3_context c, __in Z3_func_decl d, __in unsigned i);

この場合も、ファイルz3printer.pyはこれらすべての関数を使用します。

于 2012-06-28T21:02:23.600 に答える