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

Question

私は、このツールのコードとオープンソースの代替案を使ってSMT Z3の使い方（DbCなど）の実用例を探しています。それは低レベル（API）とハイレベル（テキストスクリプト）の相互作用の両方 を提供し、オープンソース

でなければなりません

• ：だから、実際には、私は同様のZ3正式な解決ツールに興味がありますが、
• サポートSMT-LIB
• 適した（使用可能）は、JavaやPython、ルビー、Valaの、そしてない Haskellのような言語のために/で書かれたツール/中
• それに基づいて安定した（実際に使用可能な）ツール、等を有しています契約による設計（DbC）、静的型検証など
01 SMT-LIBのホームページによると

（bit.ly詳細については、バンドルを参照）2010 SMTソルバーのリストです： 「Altキーエルゴ、Barcelogic、ビーバー、Boolector、CVC3、DPT、MathSAT、OpenSMT、朱子織、スピア、STP、SWORD、UCLID、veriT、Yices、Z3。 "

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

最後に、GHCの可能性との比較に関する情報は有用ですが、実装例（言語「機能」ではなく）がある場合にのみ役立ちます。私の知る限り、ここでhttp://bit.ly/bundles/ewiger/1

Answer 1

Z3に

より迅速な情報は、CVC3はそのことで、要件に最も接近する：

1. はZ3のに似ている機能セットを持っています。
2. ありBSD-style license
3. 既存のプロジェクトの根底にあるソルバーです。

CVC3はC++とJava、おそらく他の言語ではbindingsです。一般的に、APIは（テキスト）input languageよりもはるかに使いにくいと思います。 SMT-LIB2言語を使用すると、後で必要になったときに別のツールに切り替えることができるという利点があります。多くのサンプルサンプルがSMT-LIB websiteにあります。あなたはZ3にオープンソースの代替案について尋ねてきました

Answer 2

：

は2011-08でSMT-Wikipediaによると、私たちは持っている：これらの措置に基づいて

を、最も活気がよく組織と思われますプロジェクトはOpenSMT、STP、CVC4です。

私はちょうどこれをチェックしています - これまでのところ、3つはすべて合理的で、古いCVC - >私はCVC3を意味します。