c - Z3:提取数组解释

Question

如何使用 C API 提取 Z3 中数组的函数解释？当我使用以下实例查询 Rise4Fun 时:

(declare-fun arr () (Array Int Int))
(assert (= 5 (select arr 3)))
(check-sat)
(get-model)
(exit)

，我得到:

sat 
(model 
    (define-fun arr () (Array Int Int) (_ as-array k!0))
    (define-fun k!0 ((x!1 Int)) Int (ite (= x!1 3) 5 5))
)

是否可以仅使用 C API 提取 k!0 的函数解释？我尝试在数组常量声明以及 SAT 模型中为数组返回的术语上应用 Z3_model_get_func_interp ，但总是收到 Error: invalid argument .

Answer 1

是的，这是可能的。最近有人提出了一个非常类似的问题，可以在这里找到带有示例的答案:Read func interp of a z3 array from the z3 model