z3 - Pex からパス条件を SMT 2 形式で取得できますか?

Question

z3_logdir および z3_loglevel 環境変数を使用して、Pex がパス条件を *.z3 ファイル形式でログに記録するようにしています。pex にパス条件を SMT 2 形式で強制的にエクスポートさせる方法はありますか? または、.Z3 ファイル形式を SMT 2 に変換しますか?

Answer 1

Pex には、Z3 用の DLL (Microsoft.Z3.dll) が付属しています。これは Z3 バージョン 2.5 に対応します (これはhttp://research.microsoft.com/en-us/um/redmond/projects/z3/old/older_z3.htmlからダウンロードできます)。Z3 v 2.5 の API には、Z3 ファイルの内部形式への解析サポートが含まれており、これらを SMT-LIB(1) にダンプするための API 関数があります。SMT-LIB1 ベンチマークを SMT-LIB2 に変換するための新しいバージョンの Z3 およびその他のツールが存在します。