私のプログラムは、Z3_open_log（）とのすべてのz3インタラクションのログを作成します。次に、別のプログラムで、私はZ3_parse_z3_file（）でそれを読み返します。これは、入力に加えられたすべてのアサーションの結合を私に与えます。私は2つの主張を持っているとしましょう：a1とa2。次に、z3ファイルを解析することによって、（とa1 a2）を取得します。Z3ファイルを読む
私はテストしたいです（と（a1ではなく）a2）。どのようにすれば、私は2つの主張の組み合わせを取得するだけで、それを行うことができますか？私は、ASTにナビゲートして、それが結合であるかどうかを確認し、それを反復できるAPI内の関数を見つけることができませんでした。
私が行かなければならない方法なら、あなたはどのような方法をお勧めしますか？
事前にお礼ありがとうございます。
AG
上記のコメントで既に説明したように、APIを使用してZ3 ASTをトラバースすることができます。 それは、私はいくつかのコメントがあると言われています。
ロギングはデバッグのためのものです。主に問題のあるトレースを報告するために使用されます。 Z3 4.0には新しいロギングメカニズムがあります。すべてのAPIを記録し、ホストアプリケーションとZ3の間のやりとりを忠実に再現できるようにします。
Z3 4.0では、Z3のローレベルとシンプルフォーマットが廃止されました。 Z3はまだそれらのためのいくつかの限られたサポートを持っています。
Z3 4.0には、新しいC、C++、.NET、Python APIがあります。 C APIは下位互換性がありますが、廃止予定のいくつかのプロシージャをマークしました。新しいAPIを使用してASTをトラバースして操作する方がはるかに簡単です。 Python APIは既にオンラインで利用可能です。ここでは一例です。ここで
は、それぞれの子どもを抽出し、(and a1 a2)を構築し、(and (not a1) a2)を構築する別の例です。
次のチュートリアルでは、新しいZ3のAPIを取り上げます。
http://rise4fun.com/Z3Py/tutorial/guide
Z3 4.0が間もなくリリースされます。
フィードバックをいただきありがとうございますパッド）。もし私が新しい言語に慣れなければならないなら、私はOCamlを試してみました。特に、この種の機能的なもののためです。あなたはOCamlの互換性を止めていますか？ – Heyji
いいえ、OCaml APIはまだサポートされていますが、C API上の単なる薄いレイヤーです。私たちは将来的にはより良いOCaml APIを用意する予定ですが、これは次のリリースでは起こりません。 Python APIを使用する主な動機は、新しいユーザーグループに到達すること、 Pythonは科学者にとって非常に人気があり、いくつかのコンピュータ代数システムにはPythonインタフェースがあります。もちろん、Pythonはスクリプティングにも最適ですが、SMT 2.0ではなくZ3Pyを本質的に使用できます。私はPythonの大ファンではありませんでしたが、私はそれが私の上で成長したと言わなければなりません:-)言語は本当に素敵なものです。 –
APIを使用して簡単にZ3 ASTを歩くことができます。ここに1つの例がありますhttp://stackoverflow.com/questions/8862109/how-to-find-out-if-a-z3-ast-corresponds-to-a-clause – pad