HORN子句Z3文檔

Question

我想使用Z3（集合邏輯HORN）的HORN邏輯對某些命令程序進行編碼，但卻遇到了定義子句（使用SMT2）的一些困難。誰能告訴我在哪裏可以找到Z3這個功能的良好文檔來源？

Answer 1

好吧，當涉及到在喇叭子句中「編碼」一個程序時，還有更多。 首先你需要檢查一個合適的證明規則：程序是否有遞歸函數，你應該做函數摘要嗎？等等。

關於這個問題有幾篇論文，但我不認爲有任何關於VC gen的教程。 您可能還想看看Horn SMT格式中的一些基準以獲得靈感：https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/

隨意問您是否有特定問題。