в документации Z3 говорится о экземпляре квантификатора на основе модели (MBQI):
Фрагмент стратифицированных сортов
Фрагмент статифицированных сортировок - еще один разрешимый фрагмент многих формул сортированной логики первого порядка. Это соответствует формулам, которые при записи в пренексной нормальной форме имеют функциональный уровень от сортовых до натуральных, и для каждой функции
(объявить-веселье f(S_1...S_n)R)
уровень(R) ‹ уровень(S_i).
Поддерживает ли Z3 любую формулу в пренексной нормальной форме или только универсальные, в которых все кванторы существования удалены сколемизацией?
Это сделало бы фрагмент более ограничительным, не так ли (поскольку функции skolem могут нарушить стратификацию)?
(По крайней мере, в статье о MBQI [Полное описание количественных формул SMT, Yeting Ge and Leonardo de Moura, CAV 2009] мне кажется, что были рассмотрены только универсальные формулы.)
