Z3 中 Horn 子句的慢速不变推理答案

【问题标题】：slow invariant inference with Horn clauses in Z3Z3 中 Horn 子句的慢速不变推理
【发布时间】：2013-07-09 11:30:35
【问题描述】：

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

(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 秒。这似乎表明关于循环边界的二次行为。

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

【问题讨论】：

很好的例子，但问题是什么？
我做错了什么让它这么慢？我是否以非预期的方式使用它？
你没有做错任何事。这是一个很好的例子来说明抽象细化循环的性能在哪里很慢。例如，辅助不变量可以做得更好。

标签： z3

【解决方案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)

【讨论】：