Z3统计中的变量数

我试图找到Z3统计中变量的数量，但找不到任何指示。可以帮助您了解以下哪项统计数据是变量数量。Z3统计中的变量数

请注意我正在寻找变量的数量而不是子句的数量。

(:added-eqs     9977 
:binary-propagations   9922 
:conflicts     367 
:decisions     132793 
:del-clause     244104 
:final-checks    30 
:lazy-quant-instantiations 334 
:max-generation    11 
:max-memory     15.36 
:memory      4.29 
:minimized-lits    2 
:missed-quant-instantiations 49 
:mk-clause     245835 
:num-allocs     2987116.00 
:propagations    108837 
:quant-instantiations  124407 
:restarts     17 
:rlimit-count    13420765)

来源

2015-11-17 Moody

你是什么意思的“变量”：这可能，如果你招行？ SMT程序中明确声明的符号？如果是这样，请使用grep。宣布的符号加实例化的量化变量？如果是这样，每次发生不同路径（不同路径）上发生的等价实例是否应该被计数？ –

Z3不显示搜索期间创建的布尔变量的数量。从注释下

st.update("mk bool var", m_stats.m_num_mk_bool_var);

在文件src/SMT/smt_context_pp.cpp到上面的意见，重新编译，等等

来源

2015-11-19 20:56:23

Z3统计中的变量数

回答

相关问题