Войти
 | |
| Автор (ы) | Microsoft Research |
|---|---|
| Разработчик (и) | Microsoft |
| Первоначальный выпуск | 2012; 8 лет назад (2012 г.) |
| Стабильный выпуск | z3-4.8.9 / 10 сентября 2020 г.; 44 дня назад (2020-09-10) |
| Репозиторий | github.com / Z3Prover / z3 |
| Написано на | C ++ |
| Операционная система | Windows, FreeBSD, Linux (Debian, Ubuntu ), macOS |
| Platform | IA -32, x86-64 |
| Тип | Программа доказательства теорем |
| Лицензия | Лицензия MIT |
| Веб-сайт | github.com / Z3Prover |
Z3 Theorem Prover - это кроссплатформенная программа выполнимости теорий по модулю (SMT) от Microsoft.
Z3 был разработан в рамках исследований в области разработки программного обеспечения (RiSE) в Microsoft Research и нацелена на решение проблем, возникающих при проверке программного обеспечения и. Z3 поддерживает арифметику, битовые векторы фиксированного размера, расширенные массивы, типы данных, неинтерпретируемые функции и квантификаторы. Его основные приложения - это расширенная статическая проверка, генерация тестовых примеров и абстракция предикатов.
В 2015 году он получил награду Programming Languages Software Award от ACM SIGPLAN. В 2018 году Z3 получил награду Test of Time Award от Европейской совместной конференции по теории и практике программного обеспечения (ETAPS). Исследователи Microsoft Николай Бьёрнер и Леонардо де Моура получили награду Herbrand Award 2019 за выдающийся вклад в автоматизированное рассуждение в знак признания их работы по продвижению доказательства теорем с помощью Z3.
Исходный код Z3 изначально был открытым. 2015 г. Исходный код находится под лицензией MIT License и размещен на GitHub. Решатель может быть построен с использованием Visual Studio, Makefile или с помощью CMake и работает в Windows, FreeBSD, Linux и macOS.
Он имеет привязки для различных языков программирования, включая C, C ++, Java, Haskell, OCaml, Python, WebAssembly и .NET / Mono. Формат ввода по умолчанию - SMTLIB2.
В этом примере утверждения логики высказываний проверяются с использованием функций, представляющих предложения a и b. Следующий сценарий Z3 проверяет, ¬ (a ∧ b) ≡ (¬ a ∨ ¬ b):
(declare-fun a () Bool) (declare-fun b () Bool) (assert ( not (= (not (and ab)) (or (not a) (not b))))) (check-sat)
Результат:
unsat
Обратите внимание, что сценарий утверждает отрицание интересующего предложения. Неудовлетворительный результат означает, что отрицаемое предложение невыполнимо, что доказывает желаемый результат (законы Де Моргана ).
Следующий скрипт решает два заданных уравнения, находя подходящие значения для переменных a и b:
(declare-const a Int) (declare-const b Int) (assert (= (+ ab) 20)) (assert (= (+ a (* 2 b)) 10)) (check-sat) (get-model)
Результат:
sat (model (define-fun b () Int -10) (define-fun a () Int 30))
Портал бесплатного программного обеспечения с открытым исходным кодом 