从带有 forall 量词 Z3 的布尔值列表中选择一个

Question

我有一个变量列表 a_0, a_1, ..., a_n 我想用 forall 循环遍历每一个变量。就像 {a_0, a_1, ..., a_n} 中的∀a。现在我是这样做的，其中 A 是变量列表

ForAll(A, Implies(PbEq([(a, 1) for a in A], 1), ...))

PbEq

只强制一个布尔值为真。但这真的很慢，我猜是因为量词中有很多变量。

有没有办法在列表上应用 ForAll，强制它选择 1？