如何从 z3 模型中获取数组的示例值？答案

【问题标题】：How get an example value from a z3 model for arrays?如何从 z3 模型中获取数组的示例值？
【发布时间】：2018-11-13 07:08:21
【问题描述】：

感谢this question 我知道如何以更简单的方式查看模型。此时我怎样才能得到 a 和 another 的预期值？

如果可能的话，我想要使用 pyz3 的示例代码。

澄清：

有以下 smt 文件：

(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  (=  true (=  (_ bv77 32) (concat  (select  a (_ bv3 32) 
) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) 
(select  a (_ bv0 32) ) ) ) ) ) ) (=  true (=  (_ bv12 32) (concat  
(select  another (_ bv3 32) ) (concat  (select  another (_ bv2 32) ) 
(concat  (select  another (_ bv1 32) ) (select  another (_ bv0 32) ) ) 
) ) ) ) ) )

我想要 a 和 another 的值是 77 和 12

最好的方法是什么？

目前我的做法是：

import z3
import binascii

z3.set_param('model_compress', False)
s = z3.Solver()
s.from_file("first.smt")

s.check()

m = s.model()

print(m)


a = m[m.decls()[0]]

print(a)

b = bytearray(a.num_entries())

for x in range(a.num_entries()):
    index = a.entry(x).as_list()[0]
    value = a.entry(x).as_list()[1]

    print(index, value)
    b[a.num_entries()-index.as_long()-1] = value.as_long()

expected = int(binascii.hexlify(b),16)

print(expected)

正如预期的那样，输出是77 :)

谢谢

【问题讨论】：

“预期”是什么意思？
我怀疑您可能正在尝试获取该值并将其转换为 Python 对象？您可以进一步编程吗？如果是这种情况，请发布您尝试过的内容以及遇到的问题。提取数组对象通常并不容易，但也许您一开始就不需要它们。（您通常可以避开数组中的单个元素；但这当然很大程度上取决于您要解决的问题。）
嗨 Levent，我已经更新了这个问题。我希望这能澄清我的疑虑。再次感谢

标签： python z3 z3py

【解决方案1】：

如原始问题所示，数组的模型值是将索引映射到值的函数。因此，a 的示例值是 [3 -> 1, else -> 1]，它是将索引 3 映射到值 1 以及将所有其他索引映射到值 1 的函数。

【讨论】：

嗨克里斯托夫，我已经更新了这个问题。我希望这会有所帮助

【解决方案2】：

你在这里的那种用法是非常脆弱的。行：

a = m[m.decls()[0]]

假设模型将在第一个槽中具有a 值。它可能适用于这个特定的 SMT 文件；但不能保证它会一直保持。

您的代码可以简化。但我认为这忽略了这不是使用 z3 的正确方法这一点。我建议要么只使用 SMTLib，要么直接在 z3py 中编码。混合这两个接口只会增加混乱而没有明显的好处，而且正如我所提到的，这将非常脆弱。

因为您似乎已经有其他东西生成 SMTLib；为什么不坚持这种格式？您可以使用 SMTLib 的 eval 命令从模型中提取任意值。或者，在 z3py 中重新编码所有内容，并直接使用这些工具。此外，尚不清楚为什么要将 a 和 another 建模为数组开始：似乎您只对这些数组的第 [0]'th 元素感兴趣？如果是这种情况，只需使用 32 位向量而不是数组即可。

【讨论】：