Z3 中的统计数据 [英] Statistics in Z3

问题描述

我正在使用 Z3 的 Java API，我想从求解器获取一些统计信息，例如求解时间、变量/符号的数量、内存使用情况.此处的帖子(Z3py:如何获取来自公式的变量列表?) 声称 Python 中有一个实用程序实现，但我想知道是否有任何用于 JavaAPI 的实现.

I am using Java API of Z3 and I would like to get some statistics from the solver such as solving time, number of variables/symbols, memory usage. The post here (Z3py: how to get the list of variables from a formula?) claims that there is a utility implementation in Python but I was wondering if there is any for JavaAPI.

谢谢.

推荐答案

那些特定的实用程序是对 Z3 的外部贡献，仅适用于 Python API.不过应该可以在 Java 中遵循相同的想法.

Those particular utilities are an external contribution to Z3 and only available for the Python API. It should be possible to follow the same ideas in Java though.

Solver 对象有一个名为 getStatistics() 的函数，它返回 Statistics 对象，它本质上是一个键/值对的集合.请注意，不报告零值统计值(例如，另见讨论此处).

The Solver object has a function called getStatistics() that returns Statistics object, which is essentially a collection of key/value pairs. Note that zero-valued statistical values are not reported (see e.g., also the discussion here).

目前没有关于报告的统计值(或跟踪它们的精度)的文档，因此应谨慎对待所有这些值.

There is currently no documentation for the statistical values reported (or the precision with which they are tracked), so all these values should be treated with care.

另请参阅以下相关问题:

See also the following related questions:

Z3 统计数据的解释

如何解释统计数据 Z3

哪些统计数据表明 Z3 有效运行?

这篇关于Z3 中的统计数据的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！