寻找SMT Z3用例（如DbC）和Z3开源替代品的实际例子？

Question

我对这个工具的代码和开源替代品感兴趣并寻找SMT Z3用法的实际例子（如DbC）。所以，实际上，我感兴趣的相似Z3正式的解决工具，但：

• 它必须是开源
• 提供低级别（API）和高级（文字脚本）的相互作用
• 支持SMT-LIB
• 合适的（可用）在写/学习语言如Java，Python和Ruby，瓦拉和不哈斯克尔工具/
• 具有基于其稳定的（在实践中使用）的工具，如按合同设计（DbC），静态类型验证等。

根据SMT-LIB主页（请参阅bit.ly捆绑的详细信息）的2010 SMT求解器的列表是： “ALT-人机工程学，Barcelogic，海狸，Boolector，CVC3，DPT，MathSAT，OpenSMT，缎， Spear，STP，SWORD，UCLID，veriT，Yices，Z3。“

请在实践中给出任何反馈意见（代码示例是最好的）？最后，关于它与GHC可能性的比较的任何信息都将是有用的，但只有在存在实现示例（而不是语言“特征”）的情况下才有用。在Z3

更快捷的信息在这里http://bit.ly/bundles/ewiger/1

Answer 1

据我所知，CVC3最接近你的要求，因为它：

1. 有一个功能集类似于Z3的。
2. 有一个BSD-style license
3. 是一些现有项目的基础求解器。

对于C++和Java以及其他语言，CVC3有bindings。一般来说，我认为API比（文本）input language更难使用。这还带来了额外的好处，如果您坚持使用SMT-LIB2语言，那么稍后您可以在需要时切换到其他工具。 SMT-LIB website提供了大量示例。

Answer 2

你问的开源替代品Z3：

据SMT-Wikipedia在2011-08，我们有：

根据这些措施，似乎最有活力的，井井有条项目是OpenSMT，STP和CVC4。

我只是检查这个东西 - 到目前为止，所有三个似乎是合理的，再加上旧的CVC - >我的意思是CVC3。