python - z3python：将字符串转换为表达式

Question

鉴于此x,y,z = Ints('x y z') 和类似的字符串s='x + y + 2*z = 5'，是否有一种将 s 转换为 z3 表达式的快速方法？如果不可能，那么似乎我必须做很多字符串操作才能进行转换。

Answer 1

您可以使用 Pythoneval函数。这是一个例子：

from z3 import *
x,y,z = Ints('x y z') 
s = 'x + y + 2*z == 5'
F = eval(s)
solve(F)

该脚本显示[y = 0, z = 0, x = 5]在我的机器上。

不幸的是，我们无法在http://rise4fun.com/z3py执行此脚本。rise4fun 网站拒绝包含eval（出于安全原因）的 Python 脚本。