在阅读了https://www.rise4fun.com/Z3/tutorial上的优秀教程后，我开始尝试 Z3 。但现在我想了解Z3 的 SMTLIB2 方言中可用的所有命令的概述。
不幸的是，我只找到了不同语言绑定的参考手册，但没有找到 SMTLIB2 本身的参考手册。
您可以在http://smtlib.cs.uiowa.edu/中阅读有关 SMTLib 的所有内容
特别是，文档http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf是所有 SMTLib 命令的“官方”文档。
对于逻辑，您要浏览：http://smtlib.cs.uiowa.edu/logics.shtml
现在，本文档不是 Z3 特定的。但在很大程度上，它捕获了 Z3 支持的所有 SMT 命令/逻辑，并且 Z3 是实现规范方面最“合规”的求解器之一。当然有一些区别：例如，规范从不谈论优化，而 Z3 确实支持优化，同样对于集合操作和其他一些“附加功能”。正如 Malte 指出的那样，这些文档是可用的，但可能不容易浏览。我最喜欢的链接是：
https://ericpony.github.io/z3py-tutorial/guide-examples.htm（特定于 Python，但也有大量有关 Z3 功能的信息。）
Z3 编程： https: //theory.stanford.edu/~nikolaj/programmingz3.html这是一份精彩的文档，详细介绍了 z3 的内部工作原理，并演示了其大部分功能。同样，它使用 Python，但大多数情况下您可以或多或少直接在 SMTLib 中找到相应的命令。
各种语言的 API 文档：https://z3prover.github.io/api/html/index.html最终，当您开始对 z3 进行编程时，您将需要这些；但您可以将其保留为“参考”，仅供以后使用。
如果您正在寻找的某条特定信息未在这些文档中涵盖，那么这就是这个论坛的用途！祝你好运..