Z3 - Как установить ограничение байта на BitVec

Question

Я пытаюсь установить список возможных разрешенных байтов в BitVec, но я не уверен, что на самом деле устанавливаю ограничения в правильном порядке.

Например:

Давайте иметь 32 бит BV называется bv и Solver() называется s:

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

Я хочу, чтобы каждый байт может быть либо 0x2 или 0x34 или 0xFF так что я использовал Extract():

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 или 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(...), что дизъюнкция.