z3 - 基于模型的量词实例化和分层排序片段

Question

Z3 的文档说基于模型的量词实例化（MBQI）：

分层排序片段

统计排序片段是许多排序的一阶逻辑公式的另一个可判定片段。它对应于公式，当以 prenex 范式编写时，有一个从排序到自然的函数级别，并且对于每个函数

(declare-fun f (S_1 ... S_n) R)

级别（R）<级别（S_i）。

Z3 是否支持 prenex 范式的任何公式，或者仅支持所有存在量词已被 skolemization 删除的通用公式？

这会使片段更具限制性，不是吗（因为 skolem 函数可能会破坏分层）？

（至少在关于 MBQI 的论文 [Complete instantiation for quantified SMT formulas, Yeting Ge 和 Leonardo de Moura, CAV 2009] 在我看来，似乎只涵盖了通用公式。）

Answer 1

你是对的。level(R) < level(S_i)在所有存在量词都被 skolemization 删除之后，必须满足条件。Skolemization 可能会引入新的未解释的函数符号，它们也需要满足上述条件。