Z3 是一个微软出品的开源约束求解器，能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题（可以简单理解为解方程的感觉，虽然这么比喻其实还差距甚远，请勿吐槽），功能强大且易于使用。
Z3 约束求解器是针对 Satisfiability modulo theories Problem 的一种通用求解器。所谓 SMT 问题，在 Z3 环境下是指关于算术、位运算、数组等背景理论的一阶逻辑组合决定性问题。虽然 Z3 功能强大，但是从理论上来说，大部分 SMT 问题的时间复杂度都过高，根本不可能在有限时间内解决。所以千万不要把 Z3 想象得过于万能。
Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。就 CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。
Z3 本身提供一个类似于 Lisp 的内置语言，但是实际使用中，一般使用 Python Binding 操作会比较方便。
本文记录了如何在Windows(10 x64)环境下安装Z3并配置使用 Python Binding 。
0x00 安装前准备
由于在 Windows 环境下需要用到 Visual Studio Command Prompt 来 build Z3 ，所以需要安装 Visual Studio（或者直接安装 nmake ），我使用的是 Visual Studio 2017 ，直接在开始菜单中找到 VS2017 的文件夹，下拉可以找到 x64 Native Tools Command Prompt for VS 2017
0x01 安装Z3
从 github 上 clone Z3
git clone https://github.com/Z3Prover/z3.git
打开 x64 Native Tools Command Prompt for VS 2017 ，命令行中进入 Z3 文件夹，执行命令：
python scripts/mk_make.py -x --python
cd build
nmake
经过漫长的等待，当看到
Z3 was successfully built.
"Z3Py scripts can already be executed in the 'build\python' directory."
"Z3Py scripts stored in arbitrary directories can be executed if the 'build\python' directory is added to the PYTHONPATH environment variable and the 'build' directory is added to the PATH environment variable.
就说明安装成功了。
0x02 将 Z3 路径加入 PYTHONPATH
我的电脑->右键->属性->高级系统设置->环境变量，如果没有 PYTHONPATH 需要自行创建，在 python 命令行界面输入：
import os
print(os.sys.path)
可以看到当前的 PYTHONPATH ，将其加入环境变量，并把Z3文件夹下的 build\python 文件夹也加入 PYTHONPATH 。
测试一下，在 python 命令行下：
from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)
一般会看到结果：
[y = 0, x = 7]
说明配置成功。
参考资料
https://zhuanlan.zhihu.com/p/30548907
https://github.com/Z3Prover/z3