C/C++ 用の smt-lib または同様の API を使用して、ユーザー理論プラグインの入力を解析することは可能ですか? たとえば、ユーザー理論の例「test_user_theory.c」では、入力ファイルで文字列変数と定数文字列を (ビット ベクトルに分割せずに) 宣言する方法を教えてください。前もって感謝します。
質問する
160 次
1 に答える
3
関数z3_parse_smtlib_string、z3_parse_smtlib_file、z3_parse_smtlib2_stringをz3_parse_smtlib2_file使用すると、ユーザーは任意のシンボルを特定の並べ替えと宣言にバインドできます。したがって、有限数のシンボルを理論プラグインで定義された宣言に接続できます。一部の理論では任意の数の関数/定数の宣言と並べ替えを定義しているため、これは完全な解決策ではありません。たとえば、算術理論では0、1、2、 などの記号が定義されています。配列理論では、並べ替えの「無限」数が定義されています。
Theory プラグイン API は現在廃止されていることに注意してください。Z3 ソース コードが利用可能になり、Z3 定理証明器の拡張機能を実際のコード ベース内に直接実装できます。Z3 ソース コードはhttp://z3.codeplex.comで入手できます。将来のリリースで理論プラグイン API を削除する予定です。
于 2012-10-03T17:43:18.867 に答える