时间戳

首页 > 解决方案 > 如何在 Z3 java API 中获取上限和下限？

java - 如何在 Z3 java API 中获取上限和下限？

问题描述

使用 z3 优化求解器时，需要模型的边界，尤其是约束很复杂。我可以在Z3 python api中找到函数upper和lower，但不适用于Java api。你能举一些例子来说明如何在 Z3 java api 中获取模型边界吗？

标签： javaz3bounds

解决方案

您应该使用该Handle对象来访问边界。相关功能在这里：

https://github.com/Z3Prover/z3/blob/master/src/api/java/Optimize.java#L92-L103

Z3 带有一个 java 优化示例，它可以访问Handle优化类的内部。看：

https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java#L2216-L2237

只需按照该示例并进一步调用getLowerand getUpper，例如：

Optimize.Handle mx = opt.MkMaximize(xExp);

mx.getLower()
mx.getUpper()

请注意，优化中的最小值/最大值并不总是可靠的，它们也不意味着任何大于最小值和小于最大值的值都将满足您的约束。它们只是求解器在约束变量时跟踪的内容，可能不是您所想的。最好展示你尝试了什么，以及在询问堆栈溢出问题时得到了什么。

推荐阅读