自动构建析取

Question

我必须自动构建析取/合取公式，我所知道的是列表的长度，从中我必须获取变量的值，例如：

x=Int('x')    
list= [0,1,2,3]
solver=Solver()

手动执行此操作的一种方法：

solver.add(Or(x==0,x==1,x==2,x==3))

是否可以在循环或任何列表理解方法中自动从列表中加载 x 的值？我只知道 len(list)。

Answer 1

是的，我相信

z3.Or

接受一个元组，所以我们可以使用 python 构造来构建它。

solver.add(Or(tuple([x == obj for obj in list])))