z3 - 如何在 SMT 2.0 中定义返回 4 个参数的最小值的函数

Question

我想在 SMT 2.0 中定义一个函数，它返回 4 个整数值中的最小值。

Answer 1

该min4函数（4 个整数值的最小值）可以在 SMT 2.0 语言中定义为：

(define-fun min2 ((a Int) (b Int)) Int
    (ite (<= a b) a b))

(define-fun min3 ((a Int) (b Int) (c Int)) Int
    (min2 a (min2 b c)))

(define-fun min4 ((a Int) (b Int) (c Int) (d Int)) Int
    (min2 a (min3 b c d)))

以下链接包含使用此功能的示例： http ://rise4fun.com/Z3/wuyU

在 SMT 2.0 中，define-fun本质上是一个宏定义。SMT 2.0 语言不支持期望任意数量参数的函数的定义。您可以考虑为 SMT 求解器使用编程 API，例如Scala^Z3、SBV和Z3Py。它们比 SMT 2.0 更方便使用。这是 Z3Py 中的相同示例：http: //rise4fun.com/Z3Py/2vy