大多数代码示例中，z3py的 公式或表达式 都是直接作为参数传入solve或s.add等函数中，例如：
from z3 import * x = Int('x') y = Int('y') solve(x > 2, y < 10, x + 2*y == 7)然而，有时候 公式/表达式 是从其它程序或文件中读取的字符串，不能把字符串作为solve的参数，例如：
from z3 import * x = Int('x') y = Int('y') # str_expression为字符串 str_expression = "x > 2, y < 10, x + 2*y == 7" solve(str_expression) # 错误使用此时，正确的用法，是将字符串用eval()函数转化成表达式再使用，例如：
from z3 import * x = Int('x') y = Int('y') # expression为表达式 expression = eval("x > 2, y < 10, x + 2*y == 7") solve(expression) # 正确使用
