Z3的文档说基于模型的量词实例化（MBQI）：
分层排序片段
统计排序片段是许多可判定片段的另一个可判定片段 排序的一阶逻辑公式。它对应于以下公式： 当以Prenex范式编写时，有一个功能级别从 排序为自然，并针对每个函数
（声明-乐趣 f （S_1 ...S_n） R）
级别（R） <级别（S_i）。>
Z3 是否支持任何 prenex 范式的公式，或者仅支持所有存在量词都被 skolemization 删除的通用公式？
这将使片段更具限制性，不是吗（因为 skolem 函数可能会破坏分层）？
（至少在关于MBQI的论文[量化SMT公式的完整实例化，Yeting Ge和Leonardo de Moura，CAV 2009]在我看来，只涵盖了通用公式。
你是对的。在通过 skolemization 删除所有存在量词之后，必须满足条件level(R) < level(S_i)。Skolemization可能会引入新的未解释函数符号，并且它们还需要满足上述条件。