2012-03-29 10 views
1

私のプログラムは、Z3_open_log()とのすべてのz3インタラクションのログを作成します。次に、別のプログラムで、私はZ3_parse_z3_file()でそれを読み返します。これは、入力に加えられたすべてのアサーションの結合を私に与えます。私は2つの主張を持っているとしましょう:a1とa2。次に、z3ファイルを解析することによって、(とa1 a2)を取得します。Z3ファイルを読む

私はテストしたいです(と(a1ではなく)a2)。どのようにすれば、私は2つの主張の組み合わせを取得するだけで、それを行うことができますか?私は、ASTにナビゲートして、それが結合であるかどうかを確認し、それを反復できるAPI内の関数を見つけることができませんでした。

私が行かなければならない方法なら、あなたはどのような方法をお勧めしますか?

事前にお礼ありがとうございます。

AG

+1

APIを使用して簡単にZ3 ASTを歩くことができます。ここに1つの例がありますhttp://stackoverflow.com/questions/8862109/how-to-find-out-if-a-z3-ast-corresponds-to-a-clause – pad

答えて

1

上記のコメントで既に説明したように、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は既にオンラインで利用可能です。ここでは一例です。ここで

http://rise4fun.com/Z3Py/Cp

は、それぞれの子どもを抽出し、(and a1 a2)を構築し、(and (not a1) a2)を構築する別の例です。

http://rise4fun.com/Z3Py/8h

次のチュートリアルでは、新しいZ3のAPIを取り上げます。

http://rise4fun.com/Z3Py/tutorial/guide

Z3 4.0が間もなくリリースされます。

+0

フィードバックをいただきありがとうございますパッド)。もし私が新しい言語に慣れなければならないなら、私はOCamlを試してみました。特に、この種の機能的なもののためです。あなたはOCamlの互換性を止めていますか? – Heyji

+0

いいえ、OCaml APIはまだサポートされていますが、C API上の単なる薄いレイヤーです。私たちは将来的にはより良いOCaml APIを用意する予定ですが、これは次のリリースでは起こりません。 Python APIを使用する主な動機は、新しいユーザーグループに到達すること、 Pythonは科学者にとって非常に人気があり、いくつかのコンピュータ代数システムにはPythonインタフェースがあります。もちろん、Pythonはスクリプティングにも最適ですが、SMT 2.0ではなくZ3Pyを本質的に使用できます。私はPythonの大ファンではありませんでしたが、私はそれが私の上で成長したと言わなければなりません:-)言語は本当に素敵なものです。 –