Z3中的Horn子句

Question

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

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

据我所知，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“分支用于内部开发，此分支的状态可能会波动。我在你的第二个问题上得到了答案"sat“。

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

(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)))) 

相反，你会得到一个(很难读懂的)证明。