前言
最近，我发现了一个神器，它能够解决很多的数学问题，简直是数学学生的福音，当然了，它的功能也十分强大，它可以解很多具有约束条件的方程，不仅支持简单的四则混合，同时也支持位域的运算求解方程。下面就讲讲其在Android上的安装方式。
误区
首先，在Android上，要想使用Z3，还真是不简单，肯定需要准备工具，termux,一般认为就是简单的
1 | pip install z3-solver |
可能也可以，不过失败率高。
正解
首先用
1 | git clone https://github.com/angr/z3.git |
下载到本地，手动下载也可以。
然后，cd进入z3目录
1 | cd z3 |
接下来执行
1 | python scripts/mk_make.py |
然后，经过漫长的等待
1 | cd build; make |
又是等待，接下来
1 | sudo make install |
手机没有root,就用
1 | proot make install |
没root，需要下载 proot
1 | pkg install proot |
安装完成后，就可以输入
1 | python |
然后输入
1 | from z3 import * |
如果不报错，你就成功了
本教程Linux也适用。
