Описание тега z3
Z3 - это высокопроизводительное средство доказательства теорем, разрабатываемое Microsoft Research.
Z3 - это высокопроизводительное средство доказательства теорем, разрабатываемое Microsoft Research. Z3 поддерживает линейную действительную и целочисленную арифметику, битовые векторы фиксированного размера, объемные массивы, неинтерпретируемые функции и кванторы.
Некоторые ключевые особенности Z3:
- Высокопроизводительный инструмент доказательства теорем
- Интеграция эффективных технологий решения ограничений
- Проверка выполнимости логических формул с помощью кванторов
- Широкие возможности настройки с помощью обширного API
- Включая поддержку пользовательских теорий
Для получения дополнительных сведений о Z3 посетите домашнюю страницу Z3 или попробуйте Z3 в своем браузере.
См. Также руководство по Z3 для более подробного ознакомления с Z3.