z3(Python)简单大小比较的求解和化简

1、首先，对于简单的不等式可以用z3.SimpleSolver创建solver，然后用add函数添加约束并求解。返回结果和z3.sat/z3.unsat做比较，如图。

3、但是SimpleSolver在表达式不做特定化简的情况下，不能够处理如次方这样的情形，得到的结果是unknown，如图所示。此时将SimpleSolver换成Solver即可求解，代码类似。

5、如果要查看所有可用的tactic，使用z3.describe_tactics()查看。

7、如果要详细了解z3(Python)的API，可以查看z3prover官方文档。

9、如果约束如图所示，有一个比较复杂的2*x<y，则使用ctx-solver-simplify可以得到最简结果。