我在检测优化问题的无限性时遇到困难。如示例和此处的一些答案所述,无界优化问题的打印结果等于“oo”之类的东西,必须对其进行解释(通过字符串比较?)。
我的问题是:有什么方法可以使用 API 来检测吗?
我已经搜索了一段时间,唯一的函数可能会做我想做的事情是 Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t)
返回一些 Z3_ast
对象.问题是:这是正确的方法吗?如何从 Z3_ast
对象中获取无界属性?
最佳答案
目前没有内置的方法来提取无界值或无穷小。 优化引擎在表示最大/最小值时使用称为“epsilon”(实数类型)和“oo”(实数或整数类型)的临时常量 是无界的或严格限制的。这些常量没有内置识别器,并且正式地,它们不属于 Reals 域。它们属于扩展字段。因此,正式地说,我将不得不在不同的数字字段上返回一个表达式,或者返回一个三重数字(epsilon、标准数字、无限)。例如,标准数字 5.6 将表示为 (0, 5.6, 0),刚好低于 5.6 的数字表示为 (-1, 5.6, 0),+无穷大的数字表示为 (0, 0, 1).返回三个值而不是一个值似乎不是更令人满意的解决方案,就像返回一个表达式一样。我将其留给用户对返回的表达式进行后处理,并确实匹配符号“oo”和“epsilon”以在需要时分解值。
关于c++ - Z3优化: detect unboundedness via API,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/38693378/