1、首先，对于简单的不等式可以用z3.SimpleSolver创建solver，然后用add函数添加约束并求解。返回结果和z3.sat/z3.unsat做比较，如图。
2、如果是可满足的约束，可以调用solver.model()相关函数获取一个解。
3、但是SimpleSolver在表达式不做特定化简的情况下，不能够处理如次方这样的情形，得到的结果是unknown，如图所示。此时将SimpleSolver换成Solver即可求解，代码类似。
4、如果不是要求得一个解，而是想对约束进行化简，则使用化简相关函数。但是z3.simplify默认无法将多个不等式胎炎谈巴联系起来，而创建tactic并使用ctx-solver-simplify则可以结合多个不等式，达到化简目的。
5、如果要查看所有可用的tactic，使用z3.describe_tactics()查看。
6、如果要查看所有z3.simplify函数的参数，使用z3.help_simplify()查看。
7、如果要详细了解z3(Python)的API，可以查看z3prover官方文档。
8、另外补充说明simplify和ctx-solver-simplify。对于如图所示的简单不等式约束，使用propagate-ineqs即可达到化简目的，不需要ctx-solver-simplify。
9、如果约束如图所示，有一个比较复杂的2*x<y，则使用ctx-solver-simplify可以得到最简结果。
