Loading article…
Z3（Z3定理証明器とも呼ばれる）は、Microsoftが開発した充足可能性法則（SMT）ソルバーである。[ 2 ]
Z3は、マイクロソフトリサーチ・レドモンドのソフトウェアエンジニアリング研究（RiSE）グループで開発され、ソフトウェア検証やプログラム解析で発生する問題を解決することを目的としています。Z3は、算術演算、固定サイズのビットベクトル、拡張配列、データ型、未解釈関数、および量指定子をサポートしています。主な用途は、拡張静的チェック、テストケース生成、および述語抽象化です。
Z3は2015年初頭にオープンソース化されました。[ 3 ]ソースコードはMITライセンスでライセンスされており、 GitHubでホストされています。[ 4 ]ソルバーはVisual Studio、makefile、またはCMakeを使用して ビルドでき、 Windows、FreeBSD、Linux、macOSで動作します。
Z3 のデフォルトの入力フォーマットはSMTLIB2です。また、 C、C++、Python、.NET、Java、OCamlなど、いくつかのプログラミング言語の公式サポートバインディングも備えています。[ 5 ]
この例では、命題 a と b を表す関数を使用して命題論理のアサーションをチェックします。次の Z3 スクリプトは、:
(declare-fun a () Bool) (declare-fun b () Bool) (assert (not (= (not (and ab)) (or (not a)(not b))))) （チェックサット）
結果：
不満
このスクリプトは、対象となる命題の否定を主張していることに注意してください。unsatという結果は、否定された命題が充足不可能であることを意味し、したがって望ましい結果（ド・モルガンの法則）が証明されます。
以下のスクリプトは、与えられた2つの方程式を解き、変数aとbの適切な値を求めます。
（Int型のconst宣言） (declare-const b Int) (assert (= (+ ab) 20)) (assert (= (+ a (* 2 b)) 10)) （チェックサット） (get-model)
結果：
土曜日 （モデル (define-fun b () Int -10) (define-fun a () Int 30) ）
2015年、Z3はACM SIGPLANからプログラミング言語ソフトウェア賞を受賞しました。[ 6 ] [ 7 ] 2018年、Z3はソフトウェアの理論と実践に関する欧州合同会議（ETAPS）からTest of Time賞を受賞しました。 [ 8 ] Microsoftの研究者であるNikolaj BjørnerとLeonardo de Mouraは、Z3を用いた定理証明の進歩に関する功績が認められ、2019年Herbrand賞（自動推論への顕著な貢献）を受賞しました。[ 9 ] [ 10 ]
