使用 Z3 和 SMT-LIB 获得最多两个值 [英] Use Z3 and SMT-LIB to get a maximum of two values
本文介绍了使用 Z3 和 SMT-LIB 获得最多两个值的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
如何使用 smt-lib2 获得公式的最大值?
How do I get the maximum of a formula using 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".那么,如何才能做到这一点?
Of course, 'max' is unknown to smtlibv2. So, how can this be done?
推荐答案
在 Z3 中,您可以轻松定义宏 max
并使用它来获取两个值的最大值:
In Z3, you can easily define a macro max
and use it for getting maximum of two values:
(define-fun max ((x Int) (y Int)) Int
(ite (< x y) y x))
还有一个使用未解释函数对 max
建模的技巧,这将有助于与 Z3 API 一起使用:
There is another trick to model max
using uninterpreted functions, which will be helpful to use with 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就可以在检查可满足性时用函数体替换全称量词.
Note that you have to set (set-option :macro-finder true)
, so Z3 is able to replace universal quantifiers with body of the function when checking satisfiability.
这篇关于使用 Z3 和 SMT-LIB 获得最多两个值的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文