本经验介绍在z3(Python)中，简单大小比较的求解和化简怎么做。求解可以根据需要用合适的solver，大小比较的化简同样需要合适的Tactic。但是如果是要求解符号不等式，则z3可能不适合，应当使用其它的符号求解系统。
工具/原料
vscode 1.37.1
方法/步骤
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
注意事项
propagate-ineqs的另一个作用是防止1=x)，而是将1