Z3：禁用数组模型的 lambda 函数

Question

我目前正在使用数组，在某些情况下，Z3 returns 在生成的模型中为它们使用 lambda 函数。

我的代码示例：

(set-option :random-seed 0)
(set-option :produce-models true)
(set-option :produce-unsat-cores true)
; 
(set-info :status sat)
(declare-fun tmp_bv3 () (_ BitVec 4))
(declare-fun tmp_array2 () (Array (_ BitVec 4) Bool))
(declare-fun tmp_bool3 () Bool)
(declare-fun tmp_bool0 () Bool)
(assert
 (let ((?x564 (store tmp_array2 tmp_bv3 tmp_bool3)))
 (let (($x33 (bvult tmp_bv3 tmp_bv3)))
 (let ((?x237 (bvurem tmp_bv3 tmp_bv3)))
 (let ((?x24 (store tmp_array2 tmp_bv3 tmp_bool0)))
 (= (store ?x24 ?x237 $x33) ?x564))))))
(check-sat)

(get-value (tmp_array2 tmp_bv3 tmp_bool0 tmp_bool3 ))
(get-info :reason-unknown)

对于此示例，Z3 版本 4.8.6 返回以下模型：

((tmp_array2 ((as const (Array (_ BitVec 4) Bool)) false))
 (tmp_bv3 #x0)
 (tmp_bool0 false)
 (tmp_bool3 false))

和当前版本 (4.8.12) returns:

((tmp_array2 (lambda ((x!1 (_ BitVec 4))) (= x!1 #x0)))
 (tmp_bv3 #x0)
 (tmp_bool0 false)
 (tmp_bool3 false))

对于 Z3 返回结果的用例，我更喜欢 4.8.6 版返回的格式。因此我想知道是否存在禁用模型中的 lambda 函数的选项？

Answer 1

z3 围绕阵列打印的模型最近不断变化；不同的版本确实以不同的方式打印模型。（例如，参见 https://github.com/Z3Prover/z3/issues/5604）

如果我使用来自 GitHub master 的最新 z3 尝试你的程序，那么它会打印：

sat
((tmp_array2 ((as const (Array (_ BitVec 4) Bool)) false))
 (tmp_bv3 #x1)
 (tmp_bool0 false)
 (tmp_bool3 false))
(:reason-unknown "")

因此，看来此行为目前确实已在回购协议中恢复。但是你是对的，你可能会得到一个 lambda 输出，这取决于你使用的版本。

据我所知，没有可用于控制此行为的明确选项。如果你可以从 master (https://github.com/Z3Prover/z3) 编译，那将解决你的问题。如果没有，恐怕你不走运。您当然可以在他们的跟踪器中将此报告为问题，但由于最新的主人做了正确的事情，我想您会得到的答案将是“升级”。

Z3：禁用数组模型的 lambda 函数

Z3: disable lambda functions for array models

z3