Z3 Theorem Prover

Z3 Theorem Prover

Тип	SMT solverd
Автор	Microsoft Research
Розробник	Microsoft
Перший випуск	2012; 12 років тому (2012)
Платформа	IA-32, x86-64, WebAssembly, arm64
Операційна система	Windows[1], macOS[1], Linux[1] і FreeBSD[1]
Мова програмування	C++
Ліцензія	MIT[2]
Репозиторій	github.com/Z3Prover/z3

Z3, також відомий як Z3 Theorem Prover — це розв'язувач (SMT), розроблений Microsoft.^[3]

Z3 був розроблений дослідницькою групою в Research in Software Engineering (RiSE), під крилом Microsoft Research та спрямований на розв'язання проблем, що виникають при верифікації програмного забезпечення та при аналізі програм. Z3 підтримує арифметичні операції, бітові вектори фіксованого розміру, екстенсіональні масиви, типи даних, не інтерпретовані функції та квантори. Його основними застосуваннями є розширена статична перевірка^[en], генерація тестових випадків та абстракція предикатів^{[джерело?]}.

Код Z3 став відкритим на початку 2015 року.^[4] Вихідний код ліцензовано згідно з ліцензією MIT і розміщено на GitHub.^[5] Програму можна скомпілювати за допомогою Visual Studio, використовуючи Makefile або за допомогою CMake і запустити на Windows, FreeBSD, Linux та macOS.

Формат вхідних даних для Z3 за замовчуванням — SMTLIB. Цей формат використовується кількома розв'язувачами SMT. Він також має офіційну підтримку для деяких мов програмування, включаючи C, C++, Python, .NET, Java, і OCaml, а також мовне зв'язування.^[6] SMTLIB використовує синтаксис, подібний до LISP, щоб полегшити серіалізацію та десеріалізацію моделей, але він не оптимізований для читання людиною. SMTLIB визначає декілька теорій.

У цьому прикладі перевіряються твердження пропозиційної логіки з використанням функцій для представлення висловлень a та b. Наступний скрипт Z3 перевіряє, чи ${\displaystyle {\overline {a\land b}}\equiv {\overline {a}}\lor {\overline {b}}}$:

(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (not (= (not (and a b)) (or (not a)(not b)))))
(check-sat)

Результат:

unsat

Зверніть увагу, що скрипт стверджує заперечення висловлення, яке нас цікавить. Результат «незадоволено» (unsatisfied) означає, що заперечена пропозиція не є задовільною, таким чином доводячи бажаний результат (Правила де Моргана).

Наступний скрипт розв'язує два рівняння, знаходячи відповідні значення для змінних a та b:

(declare-const a Int)
(declare-const b Int)
(assert (= (+ a b) 20))
(assert (= (+ a (* 2 b)) 10))
(check-sat)
(get-model)

Результат:

sat
(model
  (define-fun b () Int
    -10)
  (define-fun a () Int
    30)
)

В 2015, Z3 отримав нагороду За програмне забезпечення на мовах програмування (Programming Languages Software Award) від ACM.^[7][8]

В 2018, Z3 отримав нагороду Випробування часом (Test of Time Award) від Європейські спільні конференції з теорії та практики програмного забезпечення (ETAPS).^[9]

Дослідники Microsoft Nikolaj Bjørner та Leonardo de Moura у 2019 році отримали нагороду Herbrand — за видатний внесок в автоматизоване міркування (Herbrand Award for Distinguished Contributions to Automated Reasoning) на знак визнання їхньої роботи в просуванні доведення теорем за допомогою Z3.^[10][11]

• Leonardo De Moura, Nikolaj Bjørner (2008). Z3: an efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems. 4963: 337—340.
• Dennis Yurichev — SAT/SMT by Example
• The inner magic behind the Z3 theorem prover

• Офіційний сайт
• Z3 online playground
• Z3 Guide