Z3优化:通过接口检测未绑定
Z3优化:通过接口检测未绑定
提问于 2016-08-01 15:41:30
我在检测优化问题的无界性时遇到了困难。如示例和这里的一些答案所述，无界优化问题的打印结果等于"oo“之类的东西，必须解释(通过字符串比较？)。
我的问题是:有没有办法使用API来检测这种情况？
我已经搜索了一段时间，唯一能做我想做的事情的函数是Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t)，它返回一些Z3_ast对象。问题是:这是正确的方法吗?如何从Z3_ast对象中获取无界属性？
回答 1
Stack Overflow用户
回答已采纳
发布于 2016-08-03 00:17:40
目前还没有内置的方法来提取无界值或无穷小。当表示无界或严格界限的最大/最小时，优化引擎使用称为"epsilon“(类型为Real)和"oo”(类型为Real或Integer)的即席常量。这些常量没有内置的识别器，从形式上讲，它们不属于Reals域。它们属于扩展字段。因此，在形式上，我必须在不同的数字字段上返回一个表达式，或者返回相当于数字三元组(epsilon，标准数字，无限)的内容。例如，标准数字5.6将表示为(0，5.6，0)，恰好低于5.6的数字表示为(-1，5.6，0)，+无穷大的数字为(0，0，1)。返回三个值而不是一个值对我来说并不是一个更令人满意的解决方案。我让用户对返回的表达式进行后处理，如果他们需要的话，可以匹配符号"oo“和"epsilon”来分解这些值。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/38693378
复制相关文章
相似问题
腾讯云开发者
