Z3 Theorem Prover

Z3 Theorem Prover
Тип	SMT solverd
Автор	Microsoft Research
Розробники	Microsoft
Перший випуск	2012; 13 років тому
Платформа	IA-32, x86-64, WebAssembly, arm64
Операційна система	Windows, macOS, Linux і FreeBSD
Мова програмування	C++
Ліцензія	MIT
Репозиторій	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 перевіряє, чи ${\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]

Посилання

↑ ^а ^б ^в ^г https://github.com/Z3Prover/z3/wiki#platforms
↑ https://github.com/Z3Prover/z3/blob/master/LICENSE.txt
↑ https://microsoft.github.io/z3guide/docs/logic/intro/
↑ Microsoft's Visual Studio timeline and Z3 Theorem Prover, Google Cloud Launcher, Facebook's Fresco—SD Times news digest: March 27, 2015. 27 березня 2015.
↑ GitHub - Z3Prover/z3: The Z3 Theorem Prover. 1 грудня 2019 — через GitHub.
↑ Bjørner, Nikolaj; de Moura, Leonardo; Nachmanson, Lev; Wintersteiger, Christoph (2019). Programming Z3. Programming Z3. Архів оригіналу за 9 лютого 2023. Процитовано 21 травня 2023.
↑ Programming Languages Software Award. www.sigplan.org.
↑ Microsoft Z3 Theorem Prover Wins Award
↑ ETAPS 2018 Test of Time Award. Архів оригіналу за 8 серпня 2020. Процитовано 23 травня 2023. [Архівовано 2020-08-08 у Wayback Machine.]
↑ The inner magic behind the Z3 theorem prover — Microsoft Research
↑ Herbrand Award

Додаткові ресурси

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

Посилання

[[https://github.com/Z3Prover/z3/wiki#platforms_https://github.com/Z3Prover/z3/wiki#platforms]<span_class="wef_low_priority_links"></span><div_style="display:none"></div>-1] а ^б ^в ^г https://github.com/Z3Prover/z3/wiki#platforms

[[https://github.com/Z3Prover/z3/blob/master/LICENSE.txt_https://github.com/Z3Prover/z3/blob/master/LICENSE.txt]<span_class="wef_low_priority_links"></span><div_style="display:none"></div>-2] ttps://github.com/Z3Prover/z3/blob/master/LICENSE.txt

[3] ttps://microsoft.github.io/z3guide/docs/logic/intro/

[4] Microsoft's Visual Studio timeline and Z3 Theorem Prover, Google Cloud Launcher, Facebook's Fresco—SD Times news digest: March 27, 2015. 27 березня 2015.

[5] GitHub - Z3Prover/z3: The Z3 Theorem Prover. 1 грудня 2019 — через GitHub.

[6] Bjørner, Nikolaj; de Moura, Leonardo; Nachmanson, Lev; Wintersteiger, Christoph (2019). Programming Z3. Programming Z3. Архів оригіналу за 9 лютого 2023. Процитовано 21 травня 2023.

[7] Programming Languages Software Award. www.sigplan.org.

[8] Microsoft Z3 Theorem Prover Wins Award

[9] ETAPS 2018 Test of Time Award. Архів оригіналу за 8 серпня 2020. Процитовано 23 травня 2023. [Архівовано 2020-08-08 у Wayback Machine.]

[10] The inner magic behind the Z3 theorem prover — Microsoft Research

[11] Herbrand Award

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]