更改Z3 fixepoint查询订单变更

Question

我试图找出为什么换查询订单可以修改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与斐波那契数总是正infered不变的矛盾。

如果查询的顺序是

(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））将非常感激。谢谢！

Answer 1

它有点侵略性假定所有约束是 UTVPI（每单位不等式两变量）。 UTVPI模式通常比通用线性算法快 。它削减 候选人不变量的搜索空间下降到UTVPI公式和使用基于流 决策程序的约束。另一方面，它可能错过不能在UTVPI片段中表示的不变量。默认情况下， 的PDR引擎检查公式都属于UTVPI在这种情况下， 它切换到UTVPI模式。

您可以通过选项来禁用UTVPI模式。

fixedpoint.pdr.utvpi =假

我将努力使开关更优美。感谢这个例子。