这是我之前关于 Z3 的基于模型的量词实例化 (MBQI) 和分层排序片段的问题的后续内容（再次感谢 Leonardo de Moura 的快速回答）。
在他们关于多排序逻辑的可判定片段的论文 [Abadi 等人，多排序逻辑的可判定片段，LPAR 2007] 中，作者描述了多排序逻辑的片段 St1，该片段可通过有限模型属性判定。
此片段需要对排序进行分层，并且公式 F 必须是（skolemized）prenex 范式，如 Z3 文档中所述，但允许使用额外的原子公式
y in Im[f]
出现在 F 中，这是一个“简写”
存在 x1 : A1, ..., xn : An 。y = f(x1,...,xn)
其中 f 是具有签名 f 的函数：A1 x ... x An -> B，并且 f 必须是范围为 B 的唯一函数。因此，St1 片段允许（以非常有限的方式）违反分层，例如，为了断言 f 是满射的。
我不确定这是否是一个开放的研究问题：有人知道 Z3 的 MBQI 决策程序对于 St1 片段是否完整？Z3 会在有限时间后（理论上）为 F 产生 SAT 或 UNSAT 吗？
首先，澄清一点，原则上，MBQI可以决定分层的多排序片段。理由在http://research.microsoft.com/en-us/um/people/leonardo/ci.pdf (*) 的第 4.1 节中给出。但是，Z3 4.0 不支持实施第 4.1 节中建议的附加规则。因此，Z3 4.0 可能会unknown在此片段中的公式上失败（返回）。我只是想明确区分算法和使用当前 Z3 的实际实现。
关于您的问题，是的 MBQI 框架可以决定包含扩展谓词的分层公式y in Im[f]。我假设这个谓词只是积极地出现。也就是说，我们没有not y in Im[f]which 等价于
forall x1:A1, ...,xn:An. y != f(x1, ... xn)
如果y in Im[f]仅积极地出现，那么它可以被扩展，并且在 skolemization 之后，我们有一个形式为 的基础公式y = f(k1, ..., kn)。MBQI 仍然是一个决策过程，因为F*(*) 中定义的集合仍然是有限的。F*只有当分层在一个通用公式中被打破时，它才会变得无限。