如何解决如何在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的任何值都将满足您的约束。它们只是求解器在约束变量时一直跟踪的内容,可能与您的想法无关。最好显示您尝试过的内容以及在询问堆栈溢出问题时获得的内容。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。