擅长:python、mysql、java
<p><code>max</code>不是一个公式,但您可以将此max函数用于您的用例:</p>
<pre class="lang-py prettyprint-override"><code>def z3_max(x, *elts):
if not elts:
return x
y = z3_max(*elts)
return If(x > y, x, y)
</code></pre>
<p>然后您可以将它与<code>z3_max(x, y, z)</code>一起使用。<br/>
如果你有一个变量列表<code>u = [x, y, z]</code>,你可以使用<code>z3_max(*u)</code></p>
<p>不过,可能还有其他更优雅的解决方案</p>