MacにZ3をインストールした。

新しいMacを手に入れたので環境構築を行っている。
その過程で、Z3のインストールにハマったので忘備録を書いておく。

目標

Z3はMicrosoftが開発しているSMTソルバで、様々な言語のバインディングがある。
公式でサポートしているのはC/C++, Java, Python, OCaml等でHaskellでは非公式のラッパーライブラリを用いる。
github.com
z3: Bindings for the Z3 Theorem Prover

今回はOCamlとHaskell両方のバインディングをインストールしたい。

トラブル

まず、z3をmlバインディングつきでインストールする。

$ git clone https://github.com/Z3Prover/z3.git
$ cd z3
$ scripts/mk_make.py --ml # --mlはmlバインディングをインストールするフラグ
$ make -C build
$ make -C build install

これでlibz3.dylibが/usr/local/lib以下にインストールされ、mlバインディングのライブラリは~/.opam/`opam switch show`/lib/Z3以下にインストールされる。

次にZ3のHaskellバインディングライブラリをインストールしようとして失敗した。

$ cabal install z3 -f examples
=> ERROR!

これをデバッグしていくと、libz3.dylibに_Z3_get_error_msg_exという関数がないことが原因だとわかった。

$ gobjdump -T /usr/local/lib/libz3.dylib | grep _get_error
0000000000028af0 g       1e SECT   01 0000 [.text] __Z22exec_Z3_get_error_codeR11z3_replayer
0000000000028b40 g       1e SECT   01 0000 [.text] __Z21exec_Z3_get_error_msgR11z3_replayer
0000000000069880 g       1e SECT   01 0000 [.text] __Z21log_Z3_get_error_codeP11_Z3_context
0000000000069a10 g       1e SECT   01 0000 [.text] __Z20log_Z3_get_error_msgP11_Z3_context13Z3_error_code
0000000000034060 g       0f SECT   01 0000 [.text] _Z3_get_error_code
00000000000340f0 g       0f SECT   01 0000 [.text] _Z3_get_error_msg
$

原因究明

Z3のレポジトリを読んでいつこの関数が消えたのかということを調べたら、去年の11月ごろに以下のコミット周辺で消されていることが判明した。
github.com
このコミット以前では次のようなAPIになっていた。

Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err);
Z3_API char const * Z3_get_error_msg(Z3_error_code err);

実装を読むとZ3_get_error_msgはZ3_get_error_msg_ex(0, err)と同じ振る舞いをするようだ。
ずいぶん前からZ3_get_error_msg自体はdeprecatedになっており、代わりにZ3_get_error_msg_exを使えということになっていた。

コミットの以後はつぎのようなAPIになっている。

Z3_API char const * Z3_get_error_msg(Z3_context c, Z3_error_code err);

つまり、長らく負の遺産となっていたZ3_get_error_msgをまともなAPIに直したということだろう。
しかし、このとき同時にZ3_get_error_msg_exも消し去ってしまうのは後方互換性の考え方からしてちょっと配慮が足りないのではないだろうか。当分の間はZ3_get_error_msg_exはdeprecatedのまま残しておいてwrapperライブラリ開発者が対応する時間を与えるべきだったと思う。

解決策

z3-haskellの開発者にプルリクを送ろうかとも考えたが、z3-haskellがmercurialで管理されていたのでしばらくプルリクの送り方を勉強してからにする予定である。
当分は問題の少なそうなコミットを適当に探した結果、c2108f74f1e5c5ab96c6e4cc189ccbc55dca339aをチェックアウトしてからビルドすれば問題なさそうである。
そもそもz3のバージョンが変わらないのにAPIの仕様が変わっているのがすごくよくないと思うので、z3にはstableなブランチを是非とも作って欲しいものだ。

5/30 21:30 追記

そもそも、masterブランチで開発されているのはz3-4.4.2でありRelease前のバージョンだと気付いた。stableなバージョンも普通にgithubのreleasesにあった。
Releases · Z3Prover/z3 · GitHub
master HEADは極めてunstableでないとわかったので大人しく最新releaseであるz3-4.4.1をインストールするのが無難だろう。

$ git clone https://github.com/Z3Prover/z3.git
$ cd z3
$ git checkout refs/tags/z3-4.4.1
$ python scripts/make_mk.py --ml --prefix=/usr/local
$ make -C build
$ make -C build install