我正在尝试使用Z3的HORN逻辑(set-logic HORN)对一些命令式程序进行编码,但是在定义子句时遇到了一些困难(使用SMT2).谁能告诉我在哪里可以找到Z3这个功能的良好文档来源？
小智 3
好吧，当涉及到用喇叭子句“编码”节目时，还有更多内容。首先你需要检查一个适当的证明规则：程序是否具有递归函数，是否应该进行函数总结？等等。
有一些关于这个主题的论文，但我认为没有任何关于 VC gen 的教程。您可能还想看看 Horn SMT 格式的一些基准测试以获取灵感：https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/
如果您有具体问题，请随时询问。