哪些统计数据表明 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.质量.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.conflicts" 可用于估计 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.

干杯，狮子座

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