寻找SMT Z3 Usecases（例如DBC）和Z3的开源替代方案的实例？ [关闭

Question

我对使用代码和该工具的开源替代方案的SMT Z3使用情况（如DBC）进行了感兴趣。因此，实际上，我对类似的Z3正式解决工具感兴趣，但是：

• 它必须是开源
• 提供低级（API）和高级（文本脚本）交互
• 支持SMT-LIB
• 合适的（可用）工具/写入/使用Java，Python，Ruby，Vala和语言的语言 不是 哈斯克尔
• 具有基于IT的稳定（实践中可用）工具，例如合同设计（DBC），静态类型验证等。

根据SMT-LIB主页（有关详细信息，请参见Bit.ly Bundle）2010 SMT求解器的列表是：“ Alt-Ergo，Barcelogic，Beaver，Boolector，Boolector，CVC3，DPT，Mathsat，Mathsat，Opensmt，Sateen，Sateen，Spear，Spear，STP，Sword，Sword，Sword，Sword，Sword，Sword，Sword，Sword，Sword，Sword，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网站.

Answer 2

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

根据 smt-wikipedia 在2011 - 08年，我们有：

基于这些措施，似乎最充满活力，组织良好的项目是OpenSMT，STP和CVC4。

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