显示 Z3 为量词推断的模式

Question

我想看看 Z3 在我的公式中对某些量词使用了什么模式。

这条评论表明这可能是可能的，但我找不到更多细节。

如何让 Z3 打印此信息？

Answer 1

根据 Christoph 的有用评论，我发现在调试模式下构建 Z3(在构建过程中将-d传递给mk_make.py(，然后在命令行上将-v:10传递给生成的 Z3 会打印推断的模式。