更改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 =假

我將努力使開關更優美。感謝這個例子。