Z3 Theorem Prover

Шаблон:Картка програми Z3, також відомий як Z3 Theorem Prover — це розв'язувач (SMT), розроблений Microsoft.

Огляд програми

Z3 був розроблений дослідницькою групою в Research in Software Engineering (RiSE), під крилом Microsoft Research та спрямований на розв'язання проблем, що виникають при верифікації програмного забезпечення та при аналізі програм. Z3 підтримує арифметичні операції, бітові вектори фіксованого розміру, екстенсіональні масиви, типи даних, не інтерпретовані функції та квантори. Його основними застосуваннями є Шаблон:Нп, генерація тестових випадків та абстракція предикатівШаблон:Citation needed.

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

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

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

Логіка висловлень та логіка предикатів

У цьому прикладі перевіряються твердження пропозиційної логіки з використанням функцій для представлення висловлень a та b. Наступний скрипт Z3 перевіряє, чи $\overline{a\wedge b}\equiv \bar{a}\vee \bar{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.

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

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

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

• Шаблон:Cite journal
• Dennis Yurichev — SAT/SMT by Example
• The inner magic behind the Z3 theorem prover

Посилання

• Шаблон:Official website
• Z3 online playground
• Z3 Guide