模型QF_AUFBV查詢缺少陣列

Question

我有以下查詢（使用SMT-LIB V1.0標準寫入）：

(benchmark gametime 
:status unknown 
:logic QF_AUFBV 
:extrafuns ((x BitVec[32])) 
:extrafuns ((a Array[32:32])) 
:extrapreds ((constraint1)) 
:extrapreds ((constraint0)) 
:formula 
(flet ($x37 (and (iff constraint0 (= (select a bv0[32]) bv0[32])) (iff constraint1 (= x bv1[32])))) 
(and $x37 (and constraint0 constraint1))) 
) 

（該查詢是有點冗餘，但是它自動生成）

通過Z3運行這一點，並要求一個模式，我收到以下內容：

a -> as-array[k!0] 
constraint1 -> true 
x -> bv1[32] 
constraint0 -> true 
k!0 -> { 
    bv0[32] -> bv0[32] 
    else -> bv0[32] 
} 

這是偉大的，因爲我有「A」和「X」的價值觀，視需要。然而，另一個查詢是類似的，除了一個小的變化：

(benchmark gametime 
:status unknown 
:logic QF_AUFBV 
:extrafuns ((x BitVec[32])) 
:extrafuns ((a Array[32:32])) 
:extrapreds ((constraint1)) 
:extrapreds ((constraint0)) 
:formula 
(flet ($x37 (and (iff constraint0 (**bvuge** (select a bv0[32]) bv0[32])) (iff constraint1 (= x bv1[32])))) 
(and $x37 (and constraint0 constraint1))) 
) 

的變化是強調了：什麼是一個平等的，現在是一個「bvuge」檢查。我從Z3收到以下型號：

constraint1 -> true 
x -> bv1[32] 
constraint0 -> true 

我沒有「a」的賦值了。這是故意的嗎？如果變量不存在於模型中，我應該假設是否有「默認」值？ （例如，這裏默認值是數組「a」在任何地方都是零）。

對於什麼是值得的，只有在操作是「bvuge」時纔會出現此問題。其他人（「bvsge」，「bvugt」，「bvsgt」，「bvult」，「bvslt」，「bvule」，「bvsle」）似乎工作。

Answer 1

我沒有「a」的賦值了。這是故意的嗎？

是的，這是故意的。數組的任何值都將滿足公式。 這是因爲constraint0：

(bvuge (select a bv0[32]) bv0[32])) 

等同於真實的。在無符號比較下，任何位矢量值都大於或等於0。 所以'a'的值是不關心的。