5

我对 SMT Z3 使用（如 DbC）的实际示例感兴趣并寻找该工具的代码和开源替代品。所以，其实我对类似的Z3形式求解工具很感兴趣，但是：

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

根据 SMT-LIB 主页（详见 bit.ly bundle），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

4

2 回答 2

3

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

  1. 具有类似于 Z3 的功能集。
  2. 拥有BSD 风格的许可证
  3. 是许多现有项目的基础求解器。

CVC3绑定了 C++ 和 Java，可能还有其他语言。总的来说，我认为 API 比（文本）输入语言更难使用。这有一个额外的好处，如果您坚持使用 SMT-LIB2 语言，您可以稍后在必要时切换到不同的工具。SMT-LIB 网站上提供了大量示例示例。

于 2011-01-16T16:17:25.077 回答
3

您询问过 Z3 的开源替代方案：

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

根据这些衡量标准，最活跃、组织最完善的项目似乎是 OpenSMT、STP 和 CVC4。

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

于 2011-09-01T18:53:44.430 回答