哪些统计数据表明Z3有效运行？ [英] Which statistics indicate an efficient run of Z3?

问题描述

SMTLib2指令（get-info all-statistics）显示几个数字，例如

The SMTLib2 directive (get-info all-statistics) displays several numbers, e.g.

num. conflicts:     4
num. propagations:  0 (binary: 0)
num. qa. inst:      23

为了测试不同的公理和编码，我想知道哪些数字适当地声明一个Z3跑步比另一个更好/更有效。

In order to test different axiomatisations and encodings I'd like to know which of those numbers are appropriate to declare that one Z3 run is better/more efficient than another.

从名称中猜出，我会说 num。 QA。 inst - 量词实例的数量是一个很好的指标（较低=更好），但是其他的呢？

Guessing from the names I'd say that num. qa. inst - the number of quantifier instantiations - is a good indicator (lower = better), but what about the others?

推荐答案

量化器实例化的数量是检查您的公理化是否产生太多实例的一个很好的措施。您也可以使用QI_PROFILE = true。它将为每个量词产生统计。您可以使用以下属性：qid给定量器一个名称。您也可以使用DEFAULT_QID = true，Z3将根据行号生成一个名称。 QI_PROFILE_FREQ =将在生成每个实例后显示统计信息。这些选项可用于检测实例循环。

Number of quantifier instantiations is a good measure for checking whether your axiomatisation is producing too many instances or not. You can also use QI_PROFILE=true. It will produce statistics for each quantifier. You can use the attribute :qid to give a name to a quantifier. You may also use DEFAULT_QID=true, and Z3 will produce a name based on line numbers. QI_PROFILE_FREQ= will display the statistics after every instances are generated. These options are useful for detecting instantiations loops.

num。conflict对于估计Z3遍历的搜索空间的大小很有用。我们可以说，如果搜索空间的大小较小，公理化是更好的。

"num. conflicts" is useful for estimating the size of the search space traversed by Z3. We may say an axiomatisation is "better" if the size of the search space is smaller.

干杯，
狮子座

Cheers, Leo

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