.net - 正在寻找 SMT Z3 用例(如 DbC)和 Z3 的开源替代品的实际示例？

Question

关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。












想改善这个问题吗？更新问题，使其成为 on-topic对于堆栈溢出。

6年前关闭。




Improve this 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 最接近您的要求，因为它:

具有类似于 Z3 的功能集。

拥有 BSD-style license

是许多现有项目的基础求解器。

CVC3 有 bindings适用于 C++ 和 Java，可能还有其他语言。总的来说，我认为 API 比(文本) input language 难用得多。 .这有一个额外的好处，如果您坚持使用 SMT-LIB2 语言，那么以后可能会在必要时切换到不同的工具。 SMT-LIB website 上提供了大量示例。 .