В настоящее время я работаю над подходом к подсчету моделей с помощью решателя SMT Z3. Кто-нибудь знает, как Z3 генерирует модели, например. что-то вроде линейной арифметики (ЛИА)? Какой алгоритм используется и где я могу найти исходный код этого алгоритма?
Спасибо, Янник
