z3 - Z3 中的喇叭子句

Question

如果要分析的程序的语义作为 Horn 子句给出，Z3 现在支持求解归纳不变量(暗示所需的属性)。

master 中的版本z3.codeplex.com 上的 Z3 源代码分支但是不支持这个功能。由于 Z3 通过使用插值的 PDR 算法解决了这些 Horn 子句问题，因此我编译了 interp分支 ( d8b31773b809 )，它支持 (set-logic HORN) .

据我了解，Horn 子句问题是用表示不变量的未知谓词指定的，而 X×Y 上的谓词只是从 X×Y 到 Bool 的函数。到目前为止一切顺利。

我尝试的第一个例子只是为 for(int i=0; i<=10; i++) 推断归纳不变量的问题循环。

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((I Int)) (or (> I 10) (not (inv I)) (inv (+ I 1)))))
(check-sat)

到目前为止一切顺利，得到了 sat .现在刚刚添加(assert (not (inv 15))我得到了unsat .然后我尝试了

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (not (inv 15)))
(check-sat)

得到unsat .

我做错了什么？

Answer 1

使用“不稳定”分支。“interp”分支用于内部开发，该分支的状态可以波动。我在你的第二个问题上得到了“满意”的答案。

第一个问题的一个更有趣的版本是:

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((I Int)) (or (> I 10) (not (inv I)) (inv (+ I 1))))) 
(assert (forall ((I Int)) (=> (inv I) (<= I 11))))
(check-sat)
(get-model)

它产生明显的归纳不变量。如果将最后一个断言替换为

(assert (forall ((I Int)) (=> (inv I) (<= I 10)))) 

相反，您会得到一个(难以阅读的)证明。