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

Question

如何使用 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)

当然，smtlibv2 不知道“max”。
那么，如何做到这一点呢？

Answer 1

在 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 能够用函数体替换全称量词。