英文:
How to get the upper bounds and lower bounds in Z3 java API?
问题
使用z3优化求解器时，特别是在约束条件复杂的情况下，需要模型的边界。我可以在Z3 Python API中找到上界（upper）和下界（lower）函数，但在Java API中似乎没有这些函数。你可以给出一些示例展示如何在Z3 Java API中获取模型边界吗？
英文:
When using the z3 optimizing solver, the bounds of models are required especially the constraints are complex. I can find the function upper and lower in the Z3 python api but not be available for the Java api. Could you take some examples showing how to get the model bounds in the Z3 java api?
答案1
得分: 0
你应该使用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()
请注意，优化中的最小/最大值并不总是可靠的，它们也不意味着大于最小值且小于最大值的任何值都将满足您的约束条件。它们只是求解器在对变量进行约束时跟踪的内容，可能并不是您考虑的内容。最好展示您尝试过什么，以及在向Stack Overflow提问时所得到的结果。
英文:
You should use the Handle object to access the bounds. The relevant functions are here:
https://github.com/Z3Prover/z3/blob/master/src/api/java/Optimize.java#L92-L103
Z3 comes with a java optimize example which does access the Handle inside the optimize class. See:
https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java#L2216-L2237
Simply follow that example and further call getLower and getUpper, something like:
Optimize.Handle mx = opt.MkMaximize(xExp);
mx.getLower()
mx.getUpper()
Note that min/max values in optimization is not always reliable, nor they mean anything larger than min and smaller than max will be satisfy your constraints. They are merely what the solver kept track of as it was constraining the variable, and might not be what you have in mind. It's best to show what you tried, and what you got when asking stack-overflow questions.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论