z3 - 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 假设 (Array Int Int) 是一种未解释的排序，并在生成的模型中为其提供解释。这是一个错误，我会在下一个版本中修复它。
同时，您可以使用以下方法之一来避免此错误:

指定包含数组理论的逻辑。示例:添加 (set-logic QF_AUFLIA)在你的例子的开头。

禁用自动配置(Z3 将安装所有可用的理论)。添加命令 (set-option :auto-config false) .