z3 - Z3 中整数的 min 函数

Question

Z3 是否支持整数的 min 函数，即返回两个数字的最小值？我在 Z3 的网站上找不到它。

此外，它是否支持某种可以返回一组数字中最小值的函数？像这样：(assert (= y (min x1 x2 x3 x4 x5)))，其中 x 和 y 是整数。

谢谢。

Answer 1

min是即将到来的浮点理论的保留关键字。您可以使用该define-fun命令来定义宏min2（二进制）、min3（三进制）等。这是一个定义min2和min3的示例min4。

http://rise4fun.com/Z3/akWje

SMT 2.0 标准不支持具有任意数量参数的宏。如果您愿意，可以使用 Z3 API 之一来执行此操作。Python 前端非常灵活。这是 Z3Py 中的一个示例。

http://rise4fun.com/Z3Py/Vvp