z3(Python)实数Real类型的简单使用

1、首先，假设已经安装z3并且import z3。使用如图代码可以快速求解关于实数x的不等式。

3、如果表达式不能满足，则求解的结果是z3.unsat，化简的结果是False。

5、使用z3.Reals可以一次声明多个常量，如图所示。如图是求解一个二元方程组，可以得到解。