我尝试使用 Z3Py 从布尔公式开始，然后对其进行抽象，以便布尔函数未知，然后将其转换为 smt 约束，以便这些约束的每个模型对应于与我的原始公式类似的不同公式。我想枚举所有模型。我想知道使用 z3 是否可以？
您似乎正在寻找未解释的函数。您可以定义函数而不需要任何定义（只是它们的类型签名），并且 SMT 求解器可以非常有效地对它们进行推理。如果您需要使用量词来限制这些函数的行为，事情就会变得棘手，但如果它们超过布尔域（并且假设您没有大量输入），则可能有有效的方法来对这些函数进行建模，而无需任何打击 -问题。
请参阅此处，了解 z3py 中未解释函数的描述：未解释排序（在该页面中搜索名为“未解释排序”的部分）。