博士

やあ、ロボ子。今日はMicrosoft ResearchのZ3定理証明器について話すのじゃ。

ロボ子

Z3ですか、博士。ソフトウェアやハードウェアの検証に使われるものですよね。どのような点が興味深いのでしょうか？

博士

Z3はただの定理証明器じゃないぞ。制約解消やハイブリッドシステムの分析、セキュリティ、生物学、幾何学問題まで、幅広い分野で使える万能ツールなのじゃ！

ロボ子

なるほど。そんなに多くの応用分野があるんですね。Z3PyというPythonインターフェースもあるようですが。

博士

そうじゃ、Z3Pyを使えば、PythonでZ3の機能を簡単に使えるのじゃ。例えば、`Int('x')`で整数変数を作ったり、`solve(x + 2*y == 7, ...)`で制約システムを解いたりできるぞ。

ロボ子

なるほど、Pythonで記述できるのは便利ですね。データ型も色々あるみたいですが、整数、実数、有理数、代数的無理数までサポートしているんですね。

博士

そうじゃ。`Real('x')`で実数変数を作ったり、`Q(num, den)`で分数を作ったりできるぞ。Z3は数学的な問題を解くのにとても強力なのじゃ。

ロボ子

ソルバーも重要な要素ですよね。`Solver()`で汎用ソルバーを作成して、`s.add(constraint)`で制約を追加、`s.check()`で制約を解決する、と。

博士

`s.check()`の結果は`sat`（充足可能）、`unsat`（充足不能）、`unknown`（不明）のいずれかになるのが面白いところじゃな。それと、`push()`と`pop()`でアサーションスタックを操作できるのも便利じゃ。

ロボ子

モデルを取得して、変数xの解釈を見ることもできるんですね。`m[x]`でモデルmにおける変数xの解釈を取得する、と。

博士

そうじゃ。Z3は算術演算もサポートしておる。`simplify(expression)`で式を簡略化したりもできるぞ。

ロボ子

ビットベクトルも扱えるんですね。`BitVec('x', 16)`で16ビットのビットベクトル変数を作成できる、と。

博士

ビット演算ハックをZ3で検証できるのはすごいじゃろ？2のべき乗判定とか、符号判定とか。

ロボ子

確かに、それは便利ですね。関数も定義できるんですね。副作用がないtotalな関数とのことですが。

博士

`Function('f', IntSort(), IntSort())`で整数を入力として整数を返す関数fを定義できるのじゃ。`evaluate(expression)`でモデルにおける式の評価もできるぞ。

ロボ子

充足可能性と妥当性の概念も重要ですね。論理式Fが常に真となる場合に妥当(valid)で、真となる割り当てが存在する場合に充足可能(satisfiable)である、と。

博士

そうじゃ。Fが妥当であることは、Not(F)が充足不能であることと同値なのじゃ。

ロボ子

リスト内包表記を使って、Z3の式や問題を簡潔に記述できるのも便利ですね。

博士

運動方程式やパズルをZ3で解くこともできるぞ。犬、猫、ネズミの購入問題とか、数独、8クイーンとか。

ロボ子

パッケージの依存関係と競合関係を制約としてモデル化して、Z3で解決することもできるんですね。すごい。

博士

Z3は本当に色々なことができるのじゃ。ローカルでZ3Pyを使うには、`from z3 import *`でインポートして、`PYTHONPATH`を設定する必要があるぞ。

ロボ子

なるほど。Z3、奥が深いですね。私も色々試してみます。

博士

そうじゃ、ロボ子。Z3をマスターすれば、どんな難問もイチコロじゃ！…たぶん。