Как создается модель с Z3?

Question

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

Спасибо, Yannic

Answer 1

Исходный код Z3 на https://github.com/z3prover/z3.git. Есть несколько арифметических решателей. Z3 обычно использует двойной симплекс.