我在Z3中得到以下统计信息.
(:added-eqs 24529
:binary-propagations 43837
:bv-bit2core 7115
:bv-conflicts 156
:bv-diseqs 10395
:bv-dynamic-diseqs 10028
:bv->core-eq 10401
:conflicts 409
:decisions 4840
:del-clause 84926
:final-checks 2
:max-generation 4
:memory 5.69
:minimized-lits 467
:mk-clause 88358
:propagations 90195
:quant-instantiations 3388
:restarts 3
:time 0.83)
我想知道每个结果行使用的指标.
你能帮助我吗？
免责声明:我觉得以正确的方式解释统计数据是一门艺术,Z3开发人员可能是唯一真正知道如何做到这一点的人.无论如何,这就是我所知道的......或者相信:
quant-instantiations表示实例化量词的数量.实例化越少越好,但是你当然不希望使你的模式/触发器过于严格,因为Z3然后将无法证明任何东西.
conflicts表示在理论子周期中发生的赋值,并且没有使公式成立.如果能够满足公式并且冲突的数量很高,那么它基本上意味着证明者尝试了许多不满足公式的任务,即证明者没有设法在目标的方向上探索搜索空间.
相关问题: