Перегляд вихідного коду сторінки Z3 Theorem Prover

{{картка програми
| author = [[Microsoft Research]]
| developer = [[Microsoft]]
| released = {{Start date and age|2012}}
| platform = [[IA-32]], [[x86-64]], [[WebAssembly]], [[arm64]]
}}
'''Z3''', також відомий як '''Z3 Theorem Prover'''&nbsp;— це [[Satisfiability Modulo Theories|розв'язувач (SMT)]], розроблений [[Microsoft]].<ref>https://microsoft.github.io/z3guide/docs/logic/intro/</ref>

== Огляд програми ==
'''Z3''' був розроблений дослідницькою групою в ''Research in Software Engineering'' (RiSE), під крилом [[Microsoft Research]] та спрямований на розв'язання проблем, що виникають при [[Верифікація програмного забезпечення|верифікації програмного забезпечення]] та при [[Аналіз програм|аналізі програм]]. Z3 підтримує арифметичні операції, бітові вектори фіксованого розміру, екстенсіональні масиви, типи даних, не інтерпретовані функції та квантори. Його основними застосуваннями є {{Нп|Розширена статична перевірка|розширена статична перевірка|en|Extended static checking}}, генерація тестових випадків та абстракція предикатів{{Citation needed}}.

Код Z3 став відкритим на початку 2015 року.<ref>{{Cite web|url=https://sdtimes.com/android/microsofts-visual-studio-timeline-and-z3-theorem-prover-google-cloud-launcher-facebooks-fresco-sd-times-news-digest-march-27-2015/|title=Microsoft's Visual Studio timeline and Z3 Theorem Prover, Google Cloud Launcher, Facebook's Fresco—SD Times news digest: March 27, 2015|date=27 березня 2015}}</ref> Вихідний код ліцензовано згідно з [[Ліцензія MIT|ліцензією MIT]] і розміщено на [[GitHub]].<ref>{{Cite web|url=https://github.com/Z3Prover/z3|title=GitHub - Z3Prover/z3: The Z3 Theorem Prover|date=1 грудня 2019|via=GitHub}}</ref> Програму можна скомпілювати за допомогою [[Visual Studio]], використовуючи [[Makefile]] або за допомогою [[CMake]] і запустити на [[Microsoft Windows|Windows]], [[FreeBSD]], [[Linux]] та [[macOS]].

Формат вхідних даних для Z3 за замовчуванням&nbsp;— SMTLIB. Цей формат використовується кількома розв'язувачами SMT. Він також має офіційну підтримку для деяких мов програмування, включаючи [[C (мова програмування)|C]], [[C++]], [[Python (мова програмування)|Python]], [[.NET Framework|.NET]], [[Java (мова програмування)|Java]], і [[OCaml]], а також [[мовне зв'язування]].<ref>{{Cite web |last=Bjørner |first=Nikolaj |last2=de Moura |first2=Leonardo |last3=Nachmanson |first3=Lev |last4=Wintersteiger |first4=Christoph |date=2019 |title=Programming Z3 |url=https://z3prover.github.io/papers/programmingz3.html |url-status=live |archive-url=https://web.archive.org/web/20230209065233/https://z3prover.github.io/papers/programmingz3.html |archive-date=9 лютого 2023 |access-date=21 травня 2023 |website=Programming Z3}}</ref>
SMTLIB використовує синтаксис, подібний до LISP, щоб полегшити серіалізацію та десеріалізацію моделей, але він не оптимізований для читання людиною. SMTLIB визначає декілька теорій.

== Приклади використання ==

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

 (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'') від [[Association for Computing Machinery|ACM]].<ref>{{Cite web|url=http://www.sigplan.org/Awards/Software/|title=Programming Languages Software Award|website=www.sigplan.org}}</ref><ref>[https://www.i-programmer.info/news/112-theory/8722-microsoft-z3-theorem-prover-wins-award-.html Microsoft Z3 Theorem Prover Wins Award]</ref>

В 2018, Z3 отримав нагороду ''Випробування часом'' (''Test of Time Award'') від [[Європейські спільні конференції з теорії та практики програмного забезпечення]] (ETAPS).<ref>{{Cite web |url=https://www.etaps.org/about/test-of-time-award/test-of-time-award-2018 |title=ETAPS 2018 Test of Time Award |accessdate=2023-05-23 |archive-date=2020-08-08 |archive-url=https://web.archive.org/web/20200808175010/https://etaps.org/about/test-of-time-award/test-of-time-award-2018 }} {{Webarchive|url=https://web.archive.org/web/20200808175010/https://etaps.org/about/test-of-time-award/test-of-time-award-2018 |date=2020-08-08 }}</ref>

Дослідники Microsoft Nikolaj Bjørner та Leonardo de Moura у 2019 році отримали нагороду ''Herbrand&nbsp;— за видатний внесок в автоматизоване міркування'' (''Herbrand Award for Distinguished Contributions to Automated Reasoning'') на знак визнання їхньої роботи в просуванні доведення теорем за допомогою Z3.<ref>[https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/ The inner magic behind the Z3 theorem prover&nbsp;— Microsoft Research]</ref><ref>[http://www.cadeinc.org/Herbrand-Award Herbrand Award]</ref>

== Посилання ==
{{Reflist}}

== Додаткові ресурси ==
* {{Cite journal|authors=Leonardo De Moura, Nikolaj Bjørner|title=Z3: an efficient SMT solver|year=2008|journal=Tools and Algorithms for the Construction and Analysis of Systems|volume=4963|pages=337–340}}
* [https://yurichev.com/writings/SAT_SMT_by_example.pdf Dennis Yurichev&nbsp;— SAT/SMT by Example]
* [https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/ The inner magic behind the Z3 theorem prover]

== Посилання ==
* {{Official website|https://github.com/Z3Prover}}
* [https://jfmc.github.io/z3-play/ Z3 online playground]
* [https://microsoft.github.io/z3guide/docs/logic/intro/ Z3 Guide]

[[Категорія:NP-повні задачі]]
[[Категорія:Формальні методи]]