我正在使用 Z3 的 Java API，我想从求解器获取一些统计数据，例如求解时间、变量/符号数量、内存使用情况。这里的帖子( Z3py: how to get the list of variables from a formula? )声称 Python 中有一个实用程序实现，但我想知道是否有 JavaAPI 的实用程序实现。
谢谢。
最佳答案
这些特定实用程序是 Z3 的外部贡献，仅适用于 Python API。不过，在 Java 中应该可以遵循相同的想法。
Solver 对象有一个名为 getStatistics() 的函数，该函数返回 Statistics 对象，该对象本质上是键/值对的集合。请注意，不会报告零值统计值(例如，另请参阅讨论 here )。
目前没有关于报告的统计值(或跟踪它们的精度)的文档，因此应谨慎对待所有这些值。
另请参阅以下相关问题:
Interpretation of Z3 Statistics
关于Z3中的统计，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/23064533/