Z3 QBVF問題

Question

跟進到先前的討論：Z3: Extracting existential model-values

有沒有之間的差異：

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y)))) 

而且

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(declare-fun y() (_ BitVec 16)) 
(assert (bvuge y (sx y))) 

至於Z3是什麼呢？也就是說，我仍然會自動爲後者獲取QBVF解算器嗎？

此外，在實驗我發現，如果我發出：

(eval (sx #x8000)) 

一個(check-sat)電話後，它工作正常（這是偉大的）。什麼是更好的是，如果我還可以說：

(eval (sx (get-value (y)))) 

唉，該查詢Z3抱怨說，它是一個invalid function application。有沒有辦法以這種方式使用eval函數？

謝謝！

Answer 1

腳本

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y)))) 

和

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(declare-fun y() (_ BitVec 16)) 
(assert (bvuge y (sx y))) 

是不等價的。第二個是實際上equisatisfiable到

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (exists ((y (_ BitVec 16))) (bvuge y (sx y)))) 

關於eval命令，可以引用任何未解釋的常量和函數符號。因此，你可以這樣寫：

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(declare-fun y() (_ BitVec 16)) 
(assert (bvuge y (sx y))) 
(check-sat) 
(eval (sx y)) 

命令(eval (sx y))不會爲第一個腳本工作，因爲y是一個普遍的變量。