擅长:python、mysql、java
<p>我猜这是来自于这个人正在处理的同一个任务:<a href="https://stackoverflow.com/questions/68531787/z3py-symbolic-expressions-cannot-be-cast-to-concrete-boolean-values">z3py: Symbolic expressions cannot be cast to concrete Boolean values</a></p>
<p>在任何情况下,这都是您想要使用的功能:</p>
<pre class="lang-py prettyprint-override"><code># Return maximum of a vector; error if empty
def symMax(vs):
m = vs[0]
for v in vs[1:]:
m = If(v > m, v, m)
return m
</code></pre>
<p>长话短说,Python的<code>max</code>不处理符号值。您必须拥有自己版本的symbolic max并使用它。太糟糕了,z3py除了收到这个神秘的错误消息之外,没有办法告诉你</p>