z3py: ограничение решения набором значений

Question

Я новичок в Z3-решателе python. Я пытаюсь определить список и ограничить все свои выводы этим списком для такой простой операции, как xor.

Мой код:

b=Solver()   
ls=[1,2,3,4,5] #my list    
s1=BitVec('s1',32)    
s2=BitVec('s2',32)    
x=b.check(s1^s2==1,  s1 in ls,  s2 in ls)  #s1 and s2 belongs to the list, however, this is not the correct way

if x==sat: print(b.model().eval)

Функция проверки не работает таким образом. Может кто-нибудь помочь мне разобраться, как это сделать по-другому?

Ответ: s1=2,s2=3; так как 2xor3 = 1 и s2, s3 принадлежит ls = [1,2,3,4,5]

Answer 1

Самый простой способ сделать это - определить функцию, которая проверяет наличие заданного аргумента в списке. Что-то вроде:

from z3 import *

def oneOf(x, lst):
    return Or([x == i for i in lst])

s1 = BitVec('s1', 32)
s2 = BitVec('s2', 32)

s = Solver()
ls = [1, 2, 3, 4, 5]

s.add(oneOf(s1, ls))
s.add(oneOf(s2, ls))
s.add(s1 ^ s2 == 1)

print (s.check())
print (s.model())

Когда я запускаю это, я получаю:

sat
[s2 = 2, s1 = 3]

, что, я считаю, то, что вы ищете.