z3python:将字符串转换为表达式 [英] z3python: converting string to expression

问题描述

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

Given that x,y,z = Ints('x y z') and a string like s='x + y + 2*z = 5', is there a quick way to convert s into a z3 expression ? If it's not possible then it seems I have to do lots of string operations to do the conversion.

推荐答案

您可以使用 Python eval 函数.下面是一个例子:

You can use the Python eval function. Here is an example:

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].

This script displays [y = 0, z = 0, x = 5] on my machine.

很遗憾，我们无法在 http://rise4fun.com/z3py 执行此脚本.rise4fun 网站拒绝包含 eval 的 Python 脚本(出于安全原因).

Unfortunately, we can't execute this script at http://rise4fun.com/z3py. The rise4fun website rejects Python scripts containing eval (for security reasons).

这篇关于z3python:将字符串转换为表达式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！