z3py：将解限制为一组值

Question

我是Z3-solver 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):
    inside = False
    for i in lst:
        inside = Or(inside, x == i)
    return inside


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]

我相信这是您的追求。