z3(python)如何替换表达式中的符号为指定值

1、在import z3之后，就可以使用z3.substitude函数进行表达式内的替换，其简单说明如图。

3、substitude也可以将一个符号替换成另一个。如图分别将z替换为x，或者y替换为z。

5、如图的BoolVal和IntVal就分别将python中的值，转化为z3接受的值。