z3python:将字符串转换为表达式

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脚本.