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

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

我可以加载它并检查它是否是sat。此时我如何获得a和another的示例值？在

^{pr2}$

谢谢

Answer 1

默认情况下，Z3为数组生成Lambda抽象；这些抽象很有用，但是很难看到模型中发生了什么。我建议关闭它，在python程序中放入以下行：

z3.set_param('model_compress', False)

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

这样，如果在程序中打印模型，则可以得到：

^{pr2}$

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