首页 文章

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

提问于
浏览 次
5

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

  • 它必须是开源的

  • 提供低级（API）和高级（文本脚本）交互

  • 支持SMT-LIB

  • 适合（可用）工具/用/ Java语言编写，如Java，python，ruby，Vala，而不是Haskell

  • 具有基于它的稳定（可在实践中使用）工具，如 Contract 设计（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

.net constraint-programming sat-solvers z3

2 回答

  • 3

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

    • 具有与Z3类似的功能集 .

    • 有BSD-style license

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

    对于C和Java，CVC3有bindings，可能还有其他语言 . 一般来说，我认为API比（textual）input language更难使用 . 这样做的另一个好处是，如果您坚持使用SMT-LIB2语言，如果有必要，您可以稍后切换到其他工具 . SMT-LIB website上提供了大量示例 .

    回复于
  • 3

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

    根据2011年至2011年的SMT-Wikipedia，我们有：

    基于这些措施，看起来最活跃，组织良好的项目是OpenSMT，STP和CVC4 .

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

    回复于

相关问题