HORN 条款 Z3 文档

【问题标题】：HORN Clause Z3 DocumentationHORN 条款 Z3 文档
【发布时间】：2014-02-15 12:10:16
【问题描述】：

我正在尝试使用 Z3 的 HORN 逻辑（set-logic HORN）对一些命令式程序进行编码，但在定义子句时遇到了一些困难（使用 SMT2）。谁能告诉我在哪里可以找到有关 Z3 的此功能的良好文档来源？

【问题讨论】：

标签： z3

【解决方案1】：

嗯，当涉及到在喇叭子句中“编码”程序时，还有更多内容。首先你需要检查一个适当的证明规则：程序是否有递归函数，你应该做函数摘要吗？等等。

关于这个主题有几篇论文，但我认为没有任何关于 VC gen 的教程。您可能还想查看一些 Horn SMT 格式的基准以获取灵感：https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/

如果您有具体问题，请随时提问。

【讨论】：