如何从 Lambda 表达式中获取 aa 值？

Question

我正在 python 中试验 z3。我有以下模型：

(set-option :produce-models true)
(set-logic QF_AUFBV )
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun another () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (and  (=  false (=  (_ bv77 32) (concat  (select  a (_ bv3 32) ) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) (select  a (_ bv0 32) ) ) ) ) ) ) (=  false (=  (_ bv12 32) (concat  (select  another (_ bv3 32) ) (concat  (select  another (_ bv2 32) ) (concat  (select  another (_ bv1 32) ) (select  another (_ bv0 32) ) ) ) ) ) ) ) )

我可以加载它并检查它是否已坐。在这一点上，我如何获得aand的示例值another？

import z3
s = z3.Solver()
s.from_file("first.smt")
"""
s
[And(False ==
     (77 == Concat(a[3], Concat(a[2], Concat(a[1], a[0])))),
     False ==
     (12 ==
      Concat(another[3],
             Concat(another[2],
                    Concat(another[1], another[0])))))]
"""
s.check()
"""
sat
"""
m = s.model()
m
[a = Lambda(k!0, 1), another = Lambda(k!0, 1)] 

谢谢

Answer 1

Z3Lambda默认生成数组的抽象；这些很有用，但很难看出模型中发生了什么。我建议通过在 python 程序中添加以下行来关闭它：

z3.set_param('model_compress', False)

您应该在您之后立即执行此操作import z3。

这样，如果您在程序中打印模型，您将得到：

>>> m
[a = [3 -> 1, else -> 1],
 another = [1 -> 1, else -> 1],
 k!0 = [3 -> 1, else -> 1],
 k!1 = [1 -> 1, else -> 1]]

这应该更具可读性。（本质上是说a和another都是将所有内容映射到 1 的数组；尽管有点复杂。）