z3模型中的數組術語的值

Question

我正在使用z3進行研究，並且遇到以下問題。我正在分析包含數組和未解釋函數的可滿足公式的模型。我想檢查特定的數組條目。

在z3指南的示例中，可以訪問這些值。
例如，對於像

(get-value ((select my_array 0))) 

一個問題得到的答案一樣

(((select my_array 0) 1)) 

表明的my_array在0位置的值是1。

不過，我得到的答案看起來像

(((select my_array 0) (select Array!val!0 0))) 

這是不是非常有幫助的。

此外，在模型的開頭我得到類似如下的塊：

;; universe for (Array Int Int): 
    ;; Array!val!10 Array!val!6 Array!val!0 Array!val!5 Array!val!9 Array!val!1 Array!val!11 Array!val!4 Array!val!2 Array!val!7 Array!val!3 Array!val!8 
    ;; ----------- 
    ;; definitions for universe elements: 
    (declare-fun Array!val!10() (Array Int Int)) 
    (declare-fun Array!val!6() (Array Int Int)) 
    (declare-fun Array!val!0() (Array Int Int)) 
    (declare-fun Array!val!5() (Array Int Int)) 
    (declare-fun Array!val!9() (Array Int Int)) 
    (declare-fun Array!val!1() (Array Int Int)) 
    (declare-fun Array!val!11() (Array Int Int)) 
    (declare-fun Array!val!4() (Array Int Int)) 
    (declare-fun Array!val!2() (Array Int Int)) 
    (declare-fun Array!val!7() (Array Int Int)) 
    (declare-fun Array!val!3() (Array Int Int)) 
    (declare-fun Array!val!8() (Array Int Int)) 
    ;; cardinality constraint: 
    (forall ((x (Array Int Int))) 
      (and (= x Array!val!10) 
       (= x Array!val!6) 
       (= x Array!val!0) 
       (= x Array!val!5) 
       (= x Array!val!9) 
       (= x Array!val!1) 
       (= x Array!val!11) 
       (= x Array!val!4) 
       (= x Array!val!2) 
       (= x Array!val!7) 
       (= x Array!val!3) 
       (= x Array!val!8))) 
    ;; ----------- 

我實在不明白這是什麼意思，但不知何故，這似乎與我的問題，作爲類似的塊而不是轉向指南中的簡單示例。有誰知道是什麼觸發了z3的這種行爲或如何避免它？

經過一番實驗後，我發現了一個「最小」的例子，表現出不希望的行爲。這似乎與在索引表達式中使用未解釋的函數有關。

(declare-fun my_function ((Int)(Int)) Int) 
(declare-fun my_array() (Array Int Int)) 

(assert 
    (= 
    (select my_array (my_function 0 1)) 
    (select my_array (my_function 1 0)) 
) 
) 

(check-sat) 
(get-model) 
(get-value ((select my_array (my_function 0 1)))) 
(get-value ((my_function 0 1))) 

Z3對此的反應是：

sat 
(model 
;; universe for (Array Int Int): 
;; Array!val!0 
;; ----------- 
;; definitions for universe elements: 
(declare-fun Array!val!0() (Array Int Int)) 
;; cardinality constraint: 
(forall ((x (Array Int Int))) (= x Array!val!0)) 
;; ----------- 
(define-fun my_array() (Array Int Int) 
Array!val!0) 
(define-fun my_function ((x!1 Int) (x!2 Int)) Int 
(ite (and (= x!1 0) (= x!2 1)) 2 
(ite (and (= x!1 1) (= x!2 0)) 3 
2))) 
) 
(((select my_array (my_function 0 1)) (select Array!val!0 2))) 
(((my_function 0 1) 2)) 

Answer 1

在SMT中， 「邏輯」 指定哪些理論可用於構建公式。例如，如果使用命令(set-logic QF_UFLIA)，則可以使用未解釋的函數和線性整數算術。未使用命令set-logic指定邏輯時。 Z3試圖自動爲用戶猜測邏輯，並且只「安裝」必要的理論。在你的例子中，Z3錯誤地猜測你的例子不需要數組理論。因此，(Array Int Int)被視爲未解釋的排序。 這就是爲什麼Z3假設（數組Int Int）是一個未解釋的排序，並在生成的模型中提供它的解釋。這是一個錯誤，我會在下一個版本中修復它。 在此期間，您可以使用以下方法之一來避免這個錯誤：

• 指定包含陣理論邏輯。示例：在示例的開頭添加(set-logic QF_AUFLIA)。

• 禁用自動配置（Z3將安裝所有可用的理論）。添加命令(set-option :auto-config false)。