Z3 统计中的变量数答案

【问题标题】：Number of variables in Z3 statisticsZ3 统计中的变量数
【发布时间】：2015-11-17 15:19:22
【问题描述】：

我试图在 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)

【问题讨论】：

“变量”是什么意思？ SMT 程序中明确声明的符号？如果是这样，请使用 grep。声明的符号加上实例化的量化变量？如果是这样，在不同路径（析取）上发生的等效实例化应该在每次发生时都计算，还是只计算一次？

标签： z3 smt z3py

【解决方案1】：

Z3 不公开搜索期间创建的布尔变量的数量。如果你移动这条线，它可以：

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

在文件src/smt/smt_context_pp.cpp中从注释下方到注释上方，重新编译等

【讨论】：