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

Question

多亏了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和{}的值是77和{}

最好的方法是什么？在

目前，我的方法是：

^{pr2}$

输出是77，如预期：）

谢谢

Answer 1

你这里的用法非常脆弱。行：

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

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

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

既然您已经有了其他生成SMTLib的东西，为什么不坚持这种格式呢？可以使用SMTLib的eval命令从模型中提取任意值。或者，在z3py中重新编码所有的东西，然后直接使用这些工具。此外，还不清楚为什么要首先将a和{}建模为数组：似乎您只对这些数组的第[0]元素感兴趣？如果是这样，只需使用32位向量而不是数组。在

Answer 2

如原问题所示，数组的模型值是将索引映射到值的函数。因此，a的一个示例值是[3 -> 1, else -> 1]，它是将索引3映射为值{}，并将所有其他索引映射到值{}。在