z3 - Z3 中 Horn 子句的慢速不变推理

Question

unstable我在 Z3/Horn （分支）中玩过以下示例

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((I Int)) (=> (and (<= I 1000) (inv I)) (inv (+ I 1)))))
(assert (forall ((I Int)) (=> (inv I) (<= I 10000))))
(check-sat)
(get-model)

推断不变量 x≤1001 需要 8.5s。这出乎意料的长……

如果我将 1000 替换为 1500，时间会增加到 19 秒，如果我将 1000 替换为 2000，则时间会增加到 34 秒。这似乎表明关于循环边界的二次行为。

我觉得奇怪的是，要花这么多时间来验证一个明显是归纳的断言……

Answer 1

结束这个问题的循环。首先，这是一个很好的例子来说明一些观点。

Z3 中的 PDR 引擎使用单一策略来生成中间断言。直观地说，它是基于近似不足的最强后置条件。它不会尝试在插值强度范围内进行搜索。如果应用魔术集变换（例如，反转转换系统），该示例会更快（立即）收敛：

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