擅长:python、mysql、java
<p>你这里的用法非常脆弱。行:</p>
<pre><code>a = m[m.decls()[0]]
</code></pre>
<p>假设模型在第一个槽中有<code>a</code>值。它可能适用于这个特定的SMT文件;但不能保证它始终有效。在</p>
<p>你的代码可以简化。但我认为这忽略了一点,这不是使用z3的正确方法。我建议要么只使用SMTLib,要么直接用z3py编码。混合这两个接口只会增加混乱,没有明显的好处,正如我提到的,将是非常脆弱的。在</p>
<p>既然您已经有了其他生成SMTLib的东西,为什么不坚持这种格式呢?可以使用SMTLib的<code>eval</code>命令从模型中提取任意值。或者,在z3py中重新编码所有的东西,然后直接使用这些工具。此外,还不清楚为什么要首先将<code>a</code>和{<cd4>}建模为数组:似乎您只对这些数组的第<code>[0]</code>元素感兴趣?如果是这样,只需使用32位向量而不是数组。在</p>