c++ - Z3优化: detect unboundedness via API

Question

我在检测优化问题的无限性时遇到困难。如示例和此处的一些答案所述，无界优化问题的打印结果等于“oo”之类的东西，必须对其进行解释(通过字符串比较？)。

我的问题是:有什么方法可以使用 API 来检测吗？

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

Answer 1

目前没有内置的方法来提取无界值或无穷小。优化引擎在表示最大/最小值时使用称为“epsilon”(实数类型)和“oo”(实数或整数类型)的临时常量是无界的或严格限制的。这些常量没有内置识别器，并且正式地，它们不属于 Reals 域。它们属于扩展字段。因此，正式地说，我将不得不在不同的数字字段上返回一个表达式，或者返回一个三重数字(epsilon、标准数字、无限)。例如，标准数字 5.6 将表示为 (0, 5.6, 0)，刚好低于 5.6 的数字表示为 (-1, 5.6, 0)，+无穷大的数字表示为 (0, 0, 1).返回三个值而不是一个值似乎不是更令人满意的解决方案，就像返回一个表达式一样。我将其留给用户对返回的表达式进行后处理，并确实匹配符号“oo”和“epsilon”以在需要时分解值。