3

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

但是， z3.codeplex.commaster上 Z3 源代码分支中的版本不支持此功能。由于 Z3 通过使用插值的 PDR 算法解决了这些 Horn 子句问题，因此我编译了支持.interpd8b31773b809(set-logic 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。

我究竟做错了什么？

4

1 回答 1

2

使用“不稳定”分支。“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))))

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

于 2013-07-05T17:00:28.467 回答