使用 Z3 和 SMT-LIB 获得最多两个值答案

【问题标题】：Use Z3 and SMT-LIB to get a maximum of two values使用 Z3 和 SMT-LIB 获得最多两个值
【发布时间】：2012-01-08 00:07:50
【问题描述】：

如何使用 smt-lib2 获得公式的最大值？

我想要这样的东西：

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (= x 2))
(assert (= y 4))
(assert (= z (max x y))
(check-sat)
(get-model)
(exit)

当然，'max' 对于 smtlibv2 是未知的。那么，如何做到这一点呢？

【问题讨论】：

标签： z3 smt

【解决方案1】：

你有 abs 和基本数学 max(a,b) = (a+b+abs(a-b))/2

【讨论】：

我知道这是怎么回事......但最后我想在两个以上的参数（浮点）上使用 max() 而不做这种变通方法。希望有更简单的解决方案；）谢谢。

【解决方案2】：

在 Z3 中，您可以轻松定义宏 max 并使用它来获取最多两个值：

(define-fun max ((x Int) (y Int)) Int
  (ite (< x y) y x))

使用未解释的函数对max 建模还有另一个技巧，这将有助于与 Z3 API 一起使用：

(declare-fun max (Int Int) Int)
(assert (forall ((x Int) (y Int))
    (= (max x y) (ite (< x y) y x))))

请注意，您必须设置(set-option :macro-finder true)，以便Z3在检查可满足性时能够将通用量词替换为函数体。

【讨论】：

快速说明：define-fun 是 SMT-LIB v2 标准的一部分。
谢谢...这确实很好。下一个问题是创建一个带有 n 个参数（如 +）的 max 函数。我无法让它与“List Int”一起使用。这是怎么做到的？
列表的最大值更复杂。 define-fun 只是宏，不允许递归。选项:macro-finder 不会检测到“递归宏”。您仍然可以为 max-int-list 编写“forall”公理。但是，Z3 不会是完整的。也就是说，它可能会返回“未知”。更准确地说，对于任何可满足的问题，以及可以通过 Z3 中使用的默认搜索限制解决的一些不可满足的问题，它将返回“未知”。在 Z3 的未来版本中，我们可能会扩展归纳数据类型过程以处理类似折叠的定义。