Z3中限制BitVec变量取列表值时in关键字失效问题及解决方法

为什么in关键字无法实现预期约束 #

Python原生的in语法执行的是运行时的成员检查逻辑，依赖__contains__魔法方法实现：遍历列表中的每一个元素，和左侧对象做相等性判断，只要有一个匹配就返回True，否则返回False。
Z3的BitVec是符号变量对象，属于约束求解的AST节点，不是实际运行时的数值，且Z3没有为表达式类型重载__contains__方法生成符号约束。所以执行bv in lst时，Python会直接把BitVec对象和列表中的int值做字面量比较，永远都会返回Python布尔值False，不会生成你预期的Or约束表达式。
你第一段代码中相当于给求解器添加了一堆False约束，自然会得到unsat的结果。

更简洁的取值域限制实现 #

Z3没有支持直接用in关键字构造约束，你可以通过封装自定义辅助函数简化写法：

# 通用的符号变量成员判断辅助函数
def z3_member(sym_var, allowed_values):
    return Or([sym_var == val for val in allowed_values])

之后使用时直接调用即可，代码复杂度和直接用in基本一致：

from z3 import *

s = Solver()
lst = [7, 11, 13, 14, 19, 21, 22, 25, 26, 28, 35, 37, 38, 41, 42, 44, 49, 50]
BV  = [BitVec(f"bv{j + 1}", 8) for j in range(11)]

lst_as_domain = [z3_member(bv, lst) for bv in BV]
s.add(lst_as_domain)

print(s.check()) # 输出 sat
print(s.model())

如果需要处理的允许值列表非常大，也可以使用Z3的查表（Table Lookup）优化接口，不过对于百级以内的允许值，上述写法的性能完全足够。

内容的提问来源于stack exchange，提问作者user1832524