z3 - VoidCC

z3

1熱

1答えて

私のプロジェクトにZ3 SMT solverを使用しようとしています。しかし、それは私の問題を引き起こしたVisual Studioのバージョンの不一致があるようです。私のVisual Studio 2008レポートその参照先のコンポーネント 'Microsoft.Z3'が見つかりませんでした。実際にインストールディレクトリ（C：\ Program Files \ Microsoft Rese

5熱

2答えて

SMT Z3ユースケース（DbCなど）とZ3のオープンソースの代替案の実例をお探しですか？

私は、このツールのコードとオープンソースの代替案を使ってSMT Z3の使い方（DbCなど）の実用例を探しています。それは低レベル（API）とハイレベル（テキストスクリプト）の相互作用の両方を提供し、オープンソースでなければなりません：だから、実際には、私は同様のZ3正式な解決ツールに興味がありますが、サポートSMT-LIB 適した（使用可能）は、JavaやPython、ルビー、Valaの、

4熱

1答えて

Z3は再帰関数を含む数式の充足可能性をチェックできますか？

私は再帰関数を含むa Z3 tutorialの例のいくつかを試しています。私は次の例を試しました。 Fibonacci（セクション8.3） IsNat（セクション8.3） Inductive（セクション10.5） Z3タイムアウト上記実施例の全てに。しかし、このチュートリアルでは、Inductiveだけが終了していないことを暗示しているようです。 Z3は、再帰関数を含む数式の充足可能性をチェックで

1熱

1答えて

Z3のソートのドメインを単一の値に制限する方法を教えてください。

my Z3 programに次の規則を使用して、sに、並べ替えSの唯一の可能な値を設定しています。 Z3: ERROR: WARNING: failed to find a pattern for quantifier (quantifier id: k!8) 特定の種類のドメインは単一の値のみを持っていることを確認するための正しい方法は何ですか？ (assert (forall ((t S)