寻找SMT Z3使用程序(如DbC)和开源替代Z3的实用示例？

Question

我对SMT Z3使用(如DbC)的代码和开源替代工具的实际示例很感兴趣，并寻找实例。因此，事实上，我对类似的Z3正式解决工具感兴趣，但是：

• 它必须是开源的
• 提供低级别(API)和高级(文本脚本)交互。
• 支持SMT-LIB
• 适合(可用)的工具/编写语言如Java，python，ruby，Vala，而不是Haskell
• 具有稳定(实用)的工具，如按合同设计(DbC)、静态类型验证等。

根据SMT-LIB主页(详见bit.ly包)，2010年SMT解决方案的列表是：“Alt、Barcelogic、Beaver、Boolector、CVC3、DPT、MathSAT、OpenSMT、SatEEn、Spear、STP、刀剑、UCLID、veriT、Yices、Z3”。

请给出任何在实践中使用它们的反馈(代码示例是最好的)？

最后，关于将其与GHC可能性进行比较的任何信息都是有用的，但只有在有实现实例(而不是语言“特性”)的情况下才有用。

关于Z3的更多快速信息，这里是http://bit.ly/bundles/ewiger/1

Answer 1

据我所知，CVC3最接近您的需求，因为它：

1. 有一个与Z3相似的功能集。
2. 有一个BSD风格许可
3. 是许多现有项目的底层解决者。

CVC3为C++和Java提供了绑定，可能还有其他语言。一般来说，我认为API比(文本) 输入语言更难使用。这有一个额外的好处，如果您坚持使用SMT 2语言，那么您以后可能会切换到另一个工具，如果需要的话。在SMT-LIB网站上有大量示例可用。

Answer 2

您已经询问了Z3的开源替代方案：

根据2011-08年SMT-Wikipedia的数据，我们有：

基于这些措施，似乎最有活力、组织最完善的项目是OpenSMT、STP和CVC4。

我只是检查这个东西-到目前为止，这三个似乎都是合理的，加上较老的CVC ->，我指的是CVC3。