問題タブ [z3]

私はこのツールに代わるコードとオープン ソースによる SMT Z3 の使用法 (DbC など) の実用的な例に興味を持ち、探しています。実際、同様の Z3 形式解法ツールに興味がありますが、

• オープンソースでなければならない
• 低レベル (API) と高レベル (テキスト スクリプト) の両方の対話を提供する
• SMT-LIBをサポート
• Java、Python、Ruby、Vala 、およびHaskell以外の言語のツール/書き込み/言語に適している (使用可能)
• 契約による設計（DbC）、静的型検証など、それに基づく安定した（実際に使用できる）ツールがあります。

SMT-LIB ホームページ (詳細については bit.ly バンドルを参照) によると、2010 SMT ソルバーのリストは次のとおりです。 UCLID、veriT、Yices、Z3."

それらのいずれかを実際に使用することについてフィードバックをお寄せください (コード例が最適です)。

最後に、それとGHCの可能性との比較に関する情報は役に立ちますが、実装例(言語の「機能」ではない)がある場合に限ります。

Z3 に関する詳しい情報はこちらhttp://bit.ly/bundles/ewiger/1

Z3用の OCaml バージョンをコンパイルしようとしましたが、ビルドすると、常にエラーと警告が表示されます。

これらはいくつかのエラーです:

よくわかりません。実行しようとするbuild.cmdとエラーが発生します。誰かアイデアがありますか?

プロジェクトでZ3 SMT ソルバーを使用しようとしています。ただし、Visual Studio のバージョンが一致していないようで、問題が発生しました。私のVisual Studio 2008はそれを報告しています

参照されているコンポーネント 'Microsoft.Z3' が見つかりませんでした。

実際にはインストール ディレクトリ (C:\Program Files\Microsoft Research\Z3-2.19\bin) にあります。

プロジェクトがコンパイルされると、別の警告が表示されます

解決されたファイルは、イメージが悪いか、メタデータがないか、またはアクセスできません。ファイルまたはアセンブリ 'C:\Program Files\Microsoft Research\Z3-2.19\bin\Microsoft.Z3.dll' またはその依存関係の 1 つを読み込めませんでした。このアセンブリは、現在読み込まれているランタイムよりも新しいランタイムによってビルドされているため、読み込むことができません。

Context、TermなどのZ3関連タイプが見つからないという他のエラーとともに。

これは、Z3 の新しいバージョンが、私が持っていない新しいバージョンの dotNet Framework を使用してコンパイルされているためですか? この問題を解決するにはどうすればよいですか? 前もって感謝します！

PS: テストで使用したファイルは、以下に貼り付けたZ3 チュートリアル (pdf)の第 5 章からのものです。

更新: 古い .msi インストーラー ファイルを数回抽出した後、v4 未満の dotNet Framework を使用する Z3 の最新バージョンは Z3 2.11 であることがわかりました。その場合、VS2008 を当面更新する代わりに、使用することにします。

SMTLib2 ディレクティブ(get-info all-statistics)は、いくつかの数字を表示します。

さまざまな公理化とエンコーディングをテストするために、ある Z3 の実行が別の Z3 の実行よりも優れている/効率的であると宣言するのに適切な数値を知りたいです。

名前から推測するとnum. qa. inst、量指定子のインスタンス化の数は良い指標 (低いほど良い) ですが、他のものはどうでしょうか?

再帰関数を含むZ3 チュートリアルの例をいくつか試しています。次の例を試してみました。

1. フィボナッチ(セクション 8.3)
2. IsNat (セクション 8.3)
3. 誘導性(セクション 10.5)

Z3は、上記のすべての例でタイムアウトします。しかし、チュートリアルは、誘導のみが非終了であることを暗示しているようです。

Z3 は、再帰関数を含む式の充足可能性をチェックできますか? または帰納的な事実を処理できませんか?

誰かがZ3自体でZ3を証明しようとしましたか？

Z3を使用して、Z3が正しいことを証明することさえ可能ですか？

より理論的には、X自体を使用して、ツールXが正しいことを証明することは可能ですか？

Z3プログラムで次のルールを使用してs、sortの可能な唯一の値を作成していますS。

ただし、上記の式により、Z3は次のエラーを報告します。

特定の種類のドメインに単一の値のみがあることを確認する正しい方法は何ですか？

Z3スコープ（SMTLib2構文）にラベルを付けてから、特定のスコープにポップバックすることは可能ですか？例えば：

で2つのスコープをポップできることは知っています(pop 2)が、私のシナリオでは、これは、一致する必要があるプッシュポップペアの間に開いているまだ閉じられていないスコープの数を追跡する必要があることを意味します。つまり、Z3コンテキストを復元する必要があります。以前に存在していました(push foo)。

Z3 は Craig 内挿を生成できますか (少なくとも命題論理については?)。Z3のドキュメントには見つかりませんでした。

リアルタイムタスクシステムで取得したスケジュールのロバスト性を証明するために Z3 を使用しています。このスクリプトhttp://www.cs.ru.nl/~georgeta/script.smt2を確認すると、unsat 応答が返されます。ただし、PROOF_MODE=1 オプションを使用すると、応答は sat になります。前者の場合、何が問題になる可能性がありますか?