Z3 - BitVecでバイト制約を設定する方法

Question

BitVecで使用可能なバイトのリストを設定しようとしていますが、実際に正しい方法で制約を設定しているかどうかはわかりません。

例：

は私たちが持ってみましょう32ビットBV bvと呼ばれ、s呼ばSolver()：私は各バイトができることをしたい

s = Solver() 
bv = BitVec(8 * 4) 

ので、私はExtract()を使用0x2か0x34または0xFFのいずれか：

i = 0 
while (i < 8 * 4): 
    s.add(Extract(i + 7, i, bv) == 0x2) 
    s.add(Extract(i + 7, i, bv) == 0x34) 
    s.add(Extract(i + 7, i, bv) == 0xFF) 
    i += 8 

悲しいことに、s.check()はunsatを返します。

私は、これは、それらのバイトがを0x2または0x34のOR 0xFFであり得ることを表現するための正しい方法ではないと思います。 私は正しい方法で制約を書いていたのですか、あるいは私の思考プロセスは間違っていますか？

Answer 1

i = 0 
while (i < 8 * 4): 
    s.add(Or(Extract(i + 7, i, bv) == 0x2), 
      Extract(i + 7, i, bv) == 0x34), 
      Extract(i + 7, i, bv) == 0xFF)) 
i += 8 

Answer 2

ソルバの制約は暗黙的に共役です。つまり、まずは論理和を構築してから、その論理和をs.add(...)にする必要があります。