2

APIからZ3を使用しており、制約をデバッグする方法を探しています。コードがコンパイルされ、Z3が制約で実行されますが、制約に問題があります。Z3に与えた制約を調べて、何が間違っているか、何が欠けているかを判断したいと思っていますが、非常に読みやすい方法でこれを行う方法がわかりません。問題は、SMTLIB_DUMP_ASSERTIONSのような機能を使用しても、自由変数に意味のある名前が提供されないことです。同じ式を何度も再利用しているので、ほとんどすべてが生成された変数に拘束されます。

入力制約のファイルをダンプする方法はありますか？ここで、自由変数は私が割り当てた名前を持っていますか？フォーマットは特に気にしませんが、SMTLIB1または2がいいでしょう。

4

1 に答える 1

1

いいえ、Z3ASTプリンターによって変数が自動的に作成されるように名前を指定することはできません。考えられる解決策の1つは、独自のASTプリンターを作成することです。Z3ディストリビューションには、サンプルアプリケーションがありますexamples/c/test_capi.c。次の機能が含まれています。

void display_ast(Z3_context c, FILE * out, Z3_ast v)

簡単なASTプリンターを実装する方法を示しています。この例は非常に単純ですが、出発点です。

于 2011-10-04T14:55:16.347 に答える