python - z3python : converting string to expression

Question

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

Answer 1

您可以使用 Python eval 函数。这是一个例子:

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 脚本(出于安全原因)。