量詞和數組在Z3

Question

Z3的答案爲「未知」時，給出了使用量詞在陣列驗證碼：

(declare-const ia Int) 
(declare-const ib Int) 
(declare-const la Int) 
(declare-const lb Int) 
(declare-const A (Array Int Int)) 
(declare-const a (Array Int Int)) 
(declare-const b (Array Int Int)) 

(assert 
    (exists 
     ((ia_1 Int) (ia_2 Int) (ib_1 Int) (la_0 Int) (lb_0 Int) (A_0 (Array Int Int)) (a_0 (Array Int Int)) (b_0 (Array Int Int))) 
     (and (= ia ia_2) (= ib ib_1) (= la la_0) (= lb lb_0) (= A A_0) (= a a_0) (= b b_0) (= ia_1 0) (= ib_1 0) (< ia_1 la_0) (< ib_1 lb_0) (< (select a_0 ia_1) (select b_0 ib_1)) (= ia_2 (+ ia_1 1))))) 

(assert 
    (not 
     (exists 
      ((ia_1 Int) (ib_1 Int) (la_0 Int) (lb_0 Int) (A_0 (Array Int Int)) (a_0 (Array Int Int)) (b_0 (Array Int Int))) 
      (and (= ia ia_1) (= ib ib_1) (= la la_0) (= lb lb_0) (= A A_0) (= a a_0) (= b b_0) (= ib_1 0))))) 

(check-sat) 

有沒有一種方法，以獲得正確的答案在這種情況下（「不飽和度」）？

編輯：如果向第二個連接添加例如約束(= ia_1 0)，則Z3正確回答「sat」。

Answer 1

這裏，「未知」是一個「正確的」答案。一般來說，數組上的量詞不是可確定的（至少不是在進一步的假設下）。 Z3放棄了這個例子，因爲它的默認量詞實例化試探法沒有選擇正確的實例化模式。欲瞭解更多信息，請參閱有關quantifiers in the Z3 tutorial的部分。

我們可以指定自己的實例化模式來幫助Z3，或者我們至少可以重述問題，以便啓發式自動找到正確的模式。在這種情況下，我成功通過重寫第二量詞像這樣：

(assert 
    (forall ((la_0 Int) (lb_0 Int) (A_0 (Array Int Int))) 
      (and 
       (= A A_0) 
       (= la la_0) 
       (= lb lb_0) 
       (forall ((b_0 (Array Int Int)) (ib_1 Int)) 
        (and 
         (= b b_0) 
         (= ib ib_1) 
         (= ib_1 0) 
         (forall ((a_0 (Array Int Int)) (ia_1 Int)) 
          (not (and (= ia ia_1) (= a a_0))))      
         ))))) 

用較少的參數每個子量詞，很可能是更好的，它會拿起一些有用的東西（我認爲），但當然是意志並不總是夠用的。