Z3是微软研发的高性能定理证明器，支持Python等API，用于软件验证、约束求解等领域。本教程介绍Z3Py的基本用法，无需Python基础，也提供C、.Net等接口。示例展示了如何用Z3Py求解简单约束问题。

Z3Py使用指南

Z3是由微软研究院开发的高性能定理证明器，广泛应用于软件/硬件验证、约束求解、混合系统分析、安全、生物信息学和几何问题等领域。本指南介绍Z3的Python接口Z3Py的主要功能。

1. 基本使用

• 创建变量：x = Int('x')
• 求解约束：solve(x > 2, y < 10, x + 2*y == 7)
• 表达式简化：simplify(x + y + 2*x + 3)

2. 数学运算

• 支持整数和实数运算
• 非线性多项式约束求解：solve(x2 + y2 > 3, x**3 + y < 5)
• 大数支持：solve(x + 10000000000000000000000 == y)

3. 布尔逻辑

• 支持与(And)、或(Or)、非(Not)、蕴含(Implies)等操作
• 布尔约束示例：solve(Implies(p, q), r == Not(q))

4. 求解器API

• 创建求解器：s = Solver()
• 添加约束：s.add(x > 10)
• 检查可满足性：s.check()
• 支持push/pop操作管理约束栈

5. 位向量运算

• 创建位向量：x = BitVec('x', 32)
• 支持位操作：&(与)、|(或)、~(非)
• 移位操作：>>(算术右移)、<<(左移)、LShR(逻辑右移)

6. 函数与模型

• 定义未解释函数：f = Function('f', IntSort(), IntSort())
• 模型求值：m.evaluate(f(f(x)))

7. 应用示例

• 运动学方程求解
• 位操作技巧验证
• 数独求解
• 八皇后问题
• 软件包安装问题

8. 本地安装

• 从Z3的python目录导入：from Z3 import *
• 需设置PYTHONPATH环境变量
• 可手动初始化：init("z3.dll")

Z3Py提供了丰富的功能来解决各种约束问题，从简单的数学约束到复杂的逻辑难题。通过Python接口，用户可以方便地利用Z3的强大求解能力。

这篇评论总结如下：

1. 正面评价：

• 认为内容简洁全面（"Very good to see all this in one short page!"）

2. 内容过时问题：

• 指出文档已有11年历史，举例说明Python 2和3的整数除法差异（"in Python 3/2 is an integer, which is indeed true in Python 2 but not in Py3"）
• 建议现代用户使用新安装方式（"you'd want to do pip install z3-solver rather than use Z3Py"）

3. 补充资源：

• 提供了额外的Z3学习资源链接（"https://www.hakank.org/z3/"）