如何使用 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 中,您可以轻松定义一个宏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 在检查可满足性时能够用函数体替换通用量词。
你有abs
,并且根据基本数学max(a,b) = (a+b+abs(a-b))/2