Z3优化:通过API检测无界性

Z3 optimization: detect unboundedness via API

本文关键字：检测 API 优化通过 Z3 更新时间：2023-10-16

我在检测优化问题的无界性时遇到了困难。正如这里的例子和一些答案所述，无界优化问题的打印结果等于"oo"，必须进行解释（通过字符串比较？）。

我的问题是：有没有什么方法可以使用API来检测这一点？

我已经搜索了一段时间，唯一可以做我想做的事情的函数是Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t)，它返回一些Z3_ast对象。问题是：这是正确的方法吗？我如何从Z3_ast对象中获得无界属性？

目前没有内置的方法来提取无界值或无穷小。当表示最大/最小值时，优化引擎使用称为"epsilon"（Real类型）和"oo"（Real或Integer类型）的特殊常量是无界的或处于严格的界。这些常量没有内置的识别器，从形式上讲，它们不属于Reals的域。它们属于一个扩展字段。因此，从形式上讲，我必须在不同的数字字段上返回一个表达式，或者返回相当于三重数字的值（epsilon，标准数字，无穷大）。例如，标准数字5.6将被表示为（0，5.6，0），并且刚好在5.6以下的数字被表示为"-1，5.6，O"，并且+无穷大的数字是（0，0，1）。对我来说，返回三个值而不是一个值似乎并不能像返回一个表达式那样令人满意。我让用户对返回的表达式进行后处理，如果需要的话，可以对符号"oo"answers"epsilon"进行匹配，以分解值。