今天在vidar的分享会上
s神跟我们讲了一个python的库叫做z3

可以在python中用这个库解决任何方程（只要有解）
网上找不到任何中文资料=。=看来我只能自己写了

z3库的介绍

Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外，著名的二进制分析框架 angr 也内置了一个修改版的 Z3。

z3的安装过程

我差点就放弃这个库了，就是因为一直安装不上。。
后来询问了s神，s神跟我说要用源码安装
给个地址https://pypi.org/project/z3-solver/4.5.1.0/#files（whl文件下载地址）
只能python2，所以我装在虚拟机上了
千万千万不要使用pip install z3，不知道为什么就是不一样。。

安装好了！

z3如何使用！

惊了这个库可以解决所有的方程，如果有解
首先要给所有的设置一个变量，他有很多种变量
Int型他代表整数所有的解都只能是整数，当然也可以用Ints一次性设置多个变量

还有就是Real型的这个代表的是有理数，可以解出所有的有理数
以及BitVec（常用的）

• Int型解方程

首先是给变量赋值
设置一个解方程的类Solver
然后一个一个添加（这样比较直观）
check一下看看有没有解，最后得出一个解，当然还有另外一种方法

• Real型解方程

直接用solve函数就可以了

• BitVec型解方程

这些都不算什么，平常都可以解出来
现在有平常解不出来的东西！！！就是向量（位与运算）

！！！！惊了这都能解出来以后我再也不用担心计组了

z3 的学习连接

• https://rise4fun.com/z3
• https://github.com/Z3Prover/z3/wiki/Slides
• http://z3prover.github.io/api/html/index.html
• http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.pdf
• Z3 - Guide