在Z3中将当前逻辑上下文打印为SMT-LIB文件

Question

我正在尝试调试一个使用SMT的程序，我想知道是否有一种方法可以打印当前的逻辑上下文，无论是从Z3内部还是通过给Z3一个命令，希望就像它是在SMTlib文件中读取的一样。

This question from 7 years ago似乎表明有一种方法可以做到这一点，但我在API文档中找不到它。

我的部分动机是，我试图调试我的程序是否因为它创建了一个难以解决的SMT问题而变慢，或者是不是因为其他原因而变慢。能够以SMT-LIB文件的形式查看当前上下文，并在命令行上的Z3中运行它，这将使这一点变得更容易。

Answer 1

不太清楚您所说的“逻辑上下文”是什么意思。如果您指的是用户为求解器提供的所有断言，则命令：

(get-assertions)

将以类似列表的S表达式的形式返回它；请参阅http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf的4.2.4节

但这听起来对您的目的没有用；毕竟，它将精确地返回您自己断言的所有内容。

如果您正在寻找求解器创建的所有学习引理、内部断言等的转储；我担心在SMTLib中无法做到这一点。您甚至可能无法使用编程性API来实现这一点。(尽管需要检查这一点。)这只能通过实际修改z3本身的源代码(开源的)，并添加相关的调试跟踪来实现。但是，这需要对z3的内部结构进行大量研究，除非您对z3代码库本身有深入的了解，否则不太可能有所帮助。

我发现运行z3 -v:10有时可以提供诊断信息；如果您看到它反复打印一些东西，这是一个很好的迹象，表明该区域出现了问题。但同样，它打印的内容和它的确切含义是猜测工作，除非您研究源代码本身。