1、首先，假设已经安装z3并且import z3。使用如图代码可以快速求解关于实数x的不等式。
2、如果需要对表达式化简，或者对结果有更多皮薹匆热控制，则需要使用如图的代码，第一部分是使用Solver进行求解，第二部分是使用ctx-solver-simplify进行化简。可以看到求得了一个分数。
3、如果表达式不能满足，则求解的结果是z3.unsat，化简的结果是False。
4、另外，有些在实数范围内成立的结果，如果换成Int整数，也同样unsat。
5、使用z3.Reals可以一次声明多个常量，如图所示。如图是求解一个二元方程组，可以得到解。
6、如果是实数和整数混合的方程，则默认Solver下可能不容易求解。如图是一个特殊情况，z3求出了一个简单的解。
