9

x,y,z = Ints('x y z') それとのような文字列を考えると、 s='x + y + 2*z = 5's を z3 式に変換する簡単な方法はありますか? それが不可能な場合は、変換を行うために多くの文字列操作を行う必要があるようです。

4

1 に答える 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 に答える