非常基本地，这个工具将帮助我们找到需要满足一些条件的变量的值，手动计算将会很烦人。因此，您可以告诉Z3变量需要满足的条件，它将找到一些值（如果可能的话）。

一些文本和示例摘自

基本操作

布尔值/与/或/非

整数/简化/实数

打印模型

机器算术

现代 CPU 和主流编程语言使用固定大小比特向量进行算术运算。在 Z3Py 中，可以使用比特向量来进行机器算术。

有符号/无符号数字

Z3提供了特殊的有符号版本的算术操作，在这些操作中，位向量被视为有符号或无符号会产生不同的结果。在Z3Py中，操作符**<, <=, >, >=, /, % 和 >>对应于有符号版本。相应的无符号操作符是ULT, ULE, UGT, UGE, UDiv, URem 和 LShR**。

函数

解释函数，如算术，其中函数 +具有固定的标准解释（它将两个数字相加）。未解释函数和常量具有最大的灵活性；它们允许与函数或常量上的约束一致的任何解释。

示例：f两次应用于x会再次得到x，但f应用一次于x与x不同。

例子

数独求解器

参考资料