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

Question

我目前正在处理数组，在某些情况下，Z3会在生成的模型中为它们返回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)返回：

((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 "")

因此，看起来这种行为目前确实在repo中恢复了。但是您是正确的，根据您使用的版本，您可能会得到lambda-output。

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