x,y,z = Ints('x y z')
それとのような文字列を考えると、 s='x + y + 2*z = 5'
s を z3 式に変換する簡単な方法はありますか? それが不可能な場合は、変換を行うために多くの文字列操作を行う必要があるようです。
12784 次
1 に答える
10
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 Web サイトは、eval
(セキュリティ上の理由から) を含む Python スクリプトを拒否します。
于 2012-09-22T03:31:37.360 に答える