如何在Z3 java API中得到上下界？

Question

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

Answer 1

您应该使用Handle对象来访问边界。相关函数如下：

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

Z3附带了一个java optimize示例，它可以访问optimize类中的Handle。请参见：

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

只需遵循该示例并进一步调用getLower和getUpper，如下所示：

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

mx.getLower()
mx.getUpper()

请注意，优化中的最小/最大值并不总是可靠的，它们也不意味着任何大于最小值和小于最大值的值都将满足您的约束。它们仅仅是求解器在约束变量时所跟踪的内容，并且可能不是您所想的。最好是在提出堆栈溢出问题时显示您尝试过的内容和获得的内容。