1、在import z3之后，就可以使用z3.substitude函数进行表达式内的替换，其简单说明如图。
2、以如图为例，有一个表达式x or (y and z)，使用如图substitude函数将y替换为BoolVal(True)，化简得到x or z。如果我们将整个式子And上y==True，可以化简得到(x or z) and y，仍然有and y一项。
3、substitude也可以将一个符号替换成另一个。如图分别将z替换为x，或者y替换为z。
4、不过，如果尝试将符号替换成python中的值是会报错的，必须转化成z3能接受的形式。
5、如图的BoolVal和IntVal就分别将python中的值，转化为z3接受的值。
6、另外，对于Real实数，和EnumSort自定义枚举，替换方式如图所示（枚举使用的python对象on，是从z3.EnumSort返回得到的z3可接受的值）。
