0

我试图找出为什么交换查询订单可能会修改 Z3 定点引擎的答案：

(declare-rel fib (Int Int))
(declare-rel q1 ())
(declare-rel q2 ())
(declare-var n Int)
(declare-var tmp1 Int)
(declare-var tmp2 Int)

(rule (=> (< n 2) (fib n 1)))
(rule (=> (and (>= n 2)
               (fib (- n 1) tmp1)
               (fib (- n 2) tmp2))
       (fib n (+ tmp1 tmp2))))

(rule (=> (< n 2) q1))
(rule (=> (and (fib n tmp1) (<= tmp1 0)) q2))

(query q1)
(query q2)

第一个查询q1是一个虚拟查询，只是向引擎询问一些事情。第二个查询q2与推断的不变量相矛盾，即斐波那契数始终为正。

如果查询的顺序是

(query q2)
(query q1)

一切正常，给出了正确的答案。但是在查询时交换它们会产生下一个错误q2：

(smt.diff_logic: non-diff logic expression (+ fib_1_1 fib_1_0 (* (- 1) fib_1_n)))
unknown

有人可以解释原因吗？是 Z3 问题还是我做错了什么？如果首先，任何有关工作的建议（我正在使用.NET API）将不胜感激。谢谢！

4

1 回答 1

1

假设所有约束都是 UTVPI（每个不等式的单元二变量），这有点激进。UTVPI 模式通常比一般线性算术更快。它将候选不变量的搜索空间缩减为 UTVPI 公式，并使用基于流的决策过程进行约束。另一方面，它可能会遗漏无法在 UTVPI 片段中表达的不变量。默认情况下，PDR 引擎会检查公式是否都属于 UTVPI，在这种情况下，它会切换到 UTVPI 模式。

您可以使用该选项禁用 UTVPI 模式。

fixedpoint.pdr.utvpi=false

我会尽量让切换更优雅。谢谢你的例子。

于 2016-07-26T17:19:13.080 回答