Я знаю, что теория целых чисел с умножением в общем неразрешима. Тем не менее, в некоторых случаях Z3 возвращает модель. Мне любопытно узнать, как это делается. Имеет ли это какое-то отношение к новой процедуре принятия решений по нелинейной арифметике над вещественными числами? Какие конкретные случаи (например, целые числа с конечным модулем и т. Д.) Были распознаны, для которых Z3 возвращает модель для запроса умножения? Буду признателен за любую оказанную помощь.