5

私はこのツールに代わるコードとオープン ソースによる 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

4

2 に答える 2

3

Z3 のオープンソースの代替案について質問されました:

2011 年 8 月の SMT-Wikipediaによると、次のようになっています。

これらの測定に基づくと、最も活気があり、よく組織されたプロジェクトは、OpenSMT、STP、および CVC4 であると思われます。

私はこれをチェックしているだけです-これまでのところ、3つすべてが合理的で、古いCVCに加えて-> CVC3を意味します。

于 2011-09-01T18:53:44.430 に答える
3

私の知る限り、CVC3 は次の点で要件に最も近いものです。

  1. Z3 と同様の機能セットを備えています。
  2. BSD スタイルのライセンスを持っています
  3. 多くの既存プロジェクトの基礎となるソルバーです。

CVC3 には、C++ と Java、およびおそらく他の言語のバインディングがあります。一般に、API は (テキスト)入力言語よりもはるかに使いにくいと思います。これには、SMT-LIB2 言語を使い続けると、必要に応じて後で別のツールに切り替えることができるという追加の利点があります。SMT-LIBの Web サイト では、多数のサンプルを入手できます。

于 2011-01-16T16:17:25.077 に答える