Hacker News Digest

Z3 — высокопроизводительный теоретический доказатель, разработанный в Microsoft Research, с API для Python (Z3Py). Он применяется в верификации ПО/железа, решении ограничений, анализе гибридных систем, безопасности и биологии. Базовый синтаксис позволяет создавать переменные через Int('x') или Real('x'), определять ограничения и решать их с помощью solve(). Z3Py поддерживает упрощение выражений simplify(), работу с рациональными и иррациональными числами, а также логические операции And, Or, Not.

Z3 обрабатывает нелинейные полиномиальные ограничения и точно представляет произвольно большие целые числа, рациональные и алгебраические иррациональные числа. Пример решения системы: solve(x > 2, y < 10, x + 2*y == 7). Для вывода результатов можно настроить точность: set_option(precision=30). Важно различать Python-деление 3/2 и рациональные числа Z3, созданные через Q(1,3) или RealVal(1)/3. Система может быть как выполнимой (satisfiable), так и невыполнимой (unsatisfiable).