左または右に任意の量だけビット単位のロールを行う推奨される方法はありますか?
たとえば、バイトで - 0x57 rolr 3 = 0xEA.
Z3py ドキュメントで「ロール」操作を見つけられませんでした。各ビットに s を使用することを考えてBitVecいましたが、それは効率的ではないようです/おそらく機能しません。アドバイスをいただければ幸いです。
編集：これまでの回答に感謝します。私は今それを吸うので、これはよりAPIの質問です。ここに私が出発点として持っているものがあります。
def roll(bt):
count = BitVecVal(int('0x03', 16), 8)
s.add(bt == (bt << count | bt >> (8 - count)) & 0xFF)
a = BitVec('a', 8)
s = Solver()
roll(a)
s.add(a == BitVecVal(int('0xEA', 16), 8))
s.check()
これは何も出力せず、モデルは利用できません。