python - Z3py - 求解数组变量约束时生成的函数 k!0

Question

在我们的研究事件中，我们正在研究 z3py(Z3 v4.4.2 的 Python API)中的数组。
我们想知道为什么 z3 提供的数组函数比要求的多。例如，这里弹出 k!0:

>>> A = Array('A', IntSort(), IntSort())
>>> solve(A[0] == 0)
[A = [0 -> 0, else -> 0], k!0 = [0 -> 0, else -> 0]]

z3似乎使用了k!0作为辅助函数，但我们在文档中没有找到任何内容。
有这方面的引用吗？

Answer 1

Z3 创建一个从 Int(数组索引)到值的函数 k!0 并将其转换为数组。虽然它没有打印在 Python 绑定(bind)中，但这可以从 Z3 REPL 中看到。

这在数组模型小节http://rise4fun.com/Z3/tutorialcontent/guide#h26中进行了简要描述。 .

(declare-const a1 (Array Int Int))
(assert (= (select a1 0) 0))
(check-sat)
;=> sat

(get-model)
;=> (model 
;     (define-fun a1 () (Array Int Int)
;       (_ as-array k!0))
;     (define-fun k!0 ((x!0 Int)) Int
;       (ite (= x!0 0) 0
;         0))
;   )