如何在Z3 Java API中获得上限和下限？

问题描述

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

解决方法

您应该使用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

只需遵循该示例，然后进一步调用getLower和getUpper，例如：

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

mx.getLower()
mx.getUpper()

请注意，优化中的最小值/最大值并不总是可靠的，也不意味着大于min且小于max的任何值都将满足您的约束。它们只是求解器在约束变量时一直跟踪的内容，可能与您的想法无关。最好显示您尝试过的内容以及在询问堆栈溢出问题时获得的内容。