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

【问题标题】：Z3py - function k!0 generated when solving constraints on Array variablesZ3py - 解决数组变量约束时生成的函数 k!0
【发布时间】：2016-10-21 16:49:53
【问题描述】：

在我们的研究活动中，我们正在研究 z3py 中的数组（Z3 v4.4.2 的 Python API）。
我们想知道为什么 z3 提供了比要求的更多的 Array 函数。例如，这里弹出 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 作为辅助函数，但我们在文档中没有找到任何内容。
有这方面的参考吗？

【问题讨论】：

标签： python arrays z3 z3py

【解决方案1】：

Z3 从Int（数组索引）创建一个函数k!0 到值并将其转换为数组。虽然没有打印在 Python 绑定中，但从 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))
;   )

【讨论】：