寻找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-Ergo,Barcelogic,Beaver,Boolector,CVC3,DPT,MathSAT,OpenSMT,SatEEn,Spear,STP,SWORD, 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-LIB2 语言，以后有必要时可以切换到不同的工具。SMT-LIB 网站上提供了大量示例。