z3python：文字列を式に変換する

x,y,z = Ints('x y z')とs='x + y + 2*z = 5'のような文字列を指定すると、sをz3式に簡単に変換できますか？可能であれば、変換を行うためにたくさんの文字列操作を行う必要があるようです。z3python：文字列を式に変換する

2012-09-22 Vu Nguyen

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スクリプトを拒否します。

2012-09-22 03:31:37

geat - すばやい返信ありがとうございましたLeonardo –

「x、y、z」を事前に宣言していないと、この一歩前進して、自動的に 'x、y、z'をどのように宣言しますか？ '' x + y + 2 * z == 5 'のすべての変数が 'Int'型であることを知っていると仮定します。 –

'exec（" x、y、z = Ints（ 'x y z'） "）'などの変数宣言を達成することができました。そうするより良い方法があるのだろうかと思います。 'exec/eval'はPythonの危険な操作です –

答えて