z3sml リリース！
この記事は MLアドベントカレンダー 12日目の記事です。
SML# 向けに Z3 というライブラリのバインディングライブラリ z3sml をリリースしました。
Z3 は SMT*1ソルバ(もしくは単にSMT) と呼ばれる種類のソフトウェアで、ある種類の制約充足問題を自動で解くことが出来ます。
z3sml を使うと、SML#からZ3のC言語インターフェースにアクセスすることが出来るようになります。
SMTとは
SMTソルバは(原則)一階述語論理の制約充足問題を扱う様々な理論ソルバの寄せ集めです。
同じく制約充足問題を扱うSATソルバが命題論理(bool式)しか扱えないのと比べて、様々な理論が使えるため問題のエンコードが簡潔かつ直接的に行えます。
参考 SATソルバーの基礎
ユースケース
- パズル
- SMTのデモとしてよく引き合いに出されるのは数独やピクロスと始めとするパズルソルバの実装です。これらのパズルはルールが単純でSMTソルバの入力としてエンコードしやすく、また解が列挙出来るためSMTで扱えることも明らか[要出典]です。何かを線で繋いだり囲んだりする類のパズルでも制約の記述を工夫すると解けるようです。
- 自動定理証明
- SMTソルバは自動定理証明器としても扱えます。そもそも最初から定理証明器として作られるSMTソルバもあります。どのように定理証明が出来るかというと、まず対象の命題(P)の否定(¬P)をSMTソルバに与えます。 するとSMTソルバは命題(P)の反例を探索することになります。ここで解が見つからない場合は命題(P)の反例が無いことになり、その命題(P)が常に成り立つ事が分かり、証明終了。…となります。
- 型推論器
- 我々(誰？)にとって重要なのはこれですよね。SMTソルバは型推論にも使うことが出来る…見込みです*2。型推論というのは、与えられたターム(型の付いてないプログラム)から得られた型についての方程式を解くことで型を決定する仕組みです。よく知られたMLやHaskell系の型推論では、高速に解ける範囲の問題に収まるように型の表現力を制限していますが、この制限を緩めて(一部を)SMTソルバに力業で解かせることでより詳細な(?)型を扱うことが出来るようになります。
- その他
- 最近では最強のボジョレーを求めることも出来るようです :)
Z3とは
Z3はマイクロソフトの研究所(MSR)が作成している高速なSMTソルバです。
いきなりトップに
Z3 is a theorem prover from Microsoft Research.
と書いてあるので実際定理証明器ですね。
でもz3のスライドを見るとテストケースの生成に使ってるとか書いてあるし、F*にも使ってるし、いろいろ使える普通のSMTソルバです。
公式に C, C++, OCaml(!!), Pythonインターフェースが提供されています。が、公式的にはpython推しっぽい気がします。
z3smlとは
今回リリースした z3sml はSMLから z3 の機能を使用できるようにしたバインディングライブラリです。
このライブラリでは SML# から z3 の全機能(v4.3.2時点^^;;)を使用できるようにバインディングが提供されています。
エラー通知やプラグイン周りのAPIが関数ポインタを要求しますが、SML# のFFIでは任意の(型の合う)クロージャを関数ポインタに変換してC側に渡せるため、これらも含めてSMLのコードだけで Z3 の機能を使うことが出来ます。*3
ビルドして動かす
ビルドするには SML# と Z3 をインストールした上で z3sml のディレクトリで make するだけです。
sample ターゲットを指定するとサンプルが実行されます。
これは公式で提供されているC APIのサンプルをほとんどそのまま含んでいるので参考にしてください。
$ make (* ビルド *) $ make sample (* サンプルを動かす *)
使い方
自分のコードから使うにはトップ階層の z3.smi を _require するだけです。
実行する際には libz3.so が動的にリンクできる必要があります。
(* sample.smi *) _require "z3.smi" (* sample.sml *) open Z3 fun main () = ...
$ smlsharp -Iz3sml/src -o sample sample.smi
コード例(数独ソルバ)
id:suer さんのSMT solver 入門の例をパク^H^H参考にした数独ソルバをz3smlで書いた例を以下に示します。
(コード全体はもう少し長いので省略…。全体は example/example3.sml としてリポジトリに入ってるのでそちらを参照。)
open Z3 (* いろいろ準備を省略 *) fun solve () = with_context (fn ctx => let fun Var id = int_var ctx id fun Int v = Z3_mk_int (ctx, v, Z3_mk_int_sort ctx) infix 4 == <> >= <= fun p == q = Z3_mk_eq (ctx, p, q) fun p <> q = Z3_mk_not (ctx, p == q) fun p <= q = Z3_mk_le (ctx, p, q) fun p >= q = Z3_mk_ge (ctx, p, q) fun && xs = Z3_mk_and (ctx, Vector.fromList xs) fun assert p = D.Z3_assert_cnstr (ctx, p) val x11 = Var "v11" val x12 = Var "v12" val x13 = Var "v13" val x14 = Var "v14" val x21 = Var "v21" val x22 = Var "v22" val x23 = Var "v23" val x24 = Var "v24" val x31 = Var "v31" val x32 = Var "v32" val x33 = Var "v33" val x34 = Var "v34" val x41 = Var "v41" val x42 = Var "v42" val x43 = Var "v43" val x44 = Var "v44" in (* domain *) assert (&& [(Int 1 <= x11), (x11 <= Int 4)]); assert (&& [(Int 1 <= x12), (x12 <= Int 4)]); assert (&& [(Int 1 <= x13), (x13 <= Int 4)]); assert (&& [(Int 1 <= x14), (x14 <= Int 4)]); assert (&& [(Int 1 <= x21), (x21 <= Int 4)]); assert (&& [(Int 1 <= x22), (x22 <= Int 4)]); assert (&& [(Int 1 <= x23), (x23 <= Int 4)]); assert (&& [(Int 1 <= x24), (x24 <= Int 4)]); assert (&& [(Int 1 <= x31), (x31 <= Int 4)]); assert (&& [(Int 1 <= x32), (x32 <= Int 4)]); assert (&& [(Int 1 <= x33), (x33 <= Int 4)]); assert (&& [(Int 1 <= x34), (x34 <= Int 4)]); assert (&& [(Int 1 <= x41), (x41 <= Int 4)]); assert (&& [(Int 1 <= x42), (x42 <= Int 4)]); assert (&& [(Int 1 <= x43), (x43 <= Int 4)]); assert (&& [(Int 1 <= x44), (x44 <= Int 4)]); (* distinct row *) assert (&& [(x11 <> x21), (x11 <> x31), (x11 <> x41), (x21 <> x31), (x21 <> x41), (x31 <> x41)]); assert (&& [(x12 <> x22), (x12 <> x32), (x12 <> x42), (x22 <> x32), (x22 <> x42), (x32 <> x42)]); assert (&& [(x13 <> x23), (x13 <> x33), (x13 <> x43), (x23 <> x33), (x23 <> x43), (x33 <> x43)]); assert (&& [(x14 <> x24), (x14 <> x34), (x14 <> x44), (x24 <> x34), (x24 <> x44), (x34 <> x44)]); (* distinct column *) assert (&& [(x11 <> x12), (x11 <> x13), (x11 <> x14), (x12 <> x13), (x12 <> x14), (x13 <> x14)]); assert (&& [(x21 <> x22), (x21 <> x23), (x21 <> x24), (x22 <> x23), (x22 <> x24), (x23 <> x24)]); assert (&& [(x31 <> x32), (x31 <> x33), (x31 <> x34), (x32 <> x33), (x32 <> x34), (x33 <> x34)]); assert (&& [(x41 <> x42), (x41 <> x43), (x41 <> x44), (x42 <> x43), (x42 <> x44), (x43 <> x44)]); (* distinct 2x2 block *) assert (&& [(x11 <> x12), (x11 <> x21), (x11 <> x22), (x12 <> x21), (x12 <> x22), (x21 <> x22)]); assert (&& [(x13 <> x14), (x13 <> x23), (x13 <> x24), (x14 <> x23), (x14 <> x24), (x23 <> x24)]); assert (&& [(x31 <> x32), (x31 <> x41), (x31 <> x42), (x32 <> x41), (x32 <> x42), (x41 <> x42)]); assert (&& [(x33 <> x34), (x33 <> x43), (x33 <> x44), (x34 <> x43), (x34 <> x44), (x43 <> x44)]); (* pre assinged values *) (** * 1 2 3 4 * +---+---+---+---+ * 1 | | | | 4 | * +---+---+---+---+ * 2 | | | 1 | 2 | * +---+---+---+---+ * 3 | | 1 | 4 | 3 | * +---+---+---+---+ * 4 | 4 | 3 | 2 | 1 | * +---+---+---+---+ *) assert (x14 == Int 4); assert (x23 == Int 1); assert (x24 == Int 2); assert (x32 == Int 1); assert (x33 == Int 4); assert (x34 == Int 3); assert (x41 == Int 4); assert (x42 == Int 3); assert (x43 == Int 2); assert (x44 == Int 1); check ctx Z3.Z3_lbool.Z3_L_TRUE end)
これを実行してみると、以下のように制約を満たすモデルを出力します。
z3sml.git$ make sample3 SML# [sample/sample3.o] ./sample/sample3 sat v43 -> 2 v24 -> 2 v34 -> 3 v12 -> 2 v14 -> 4 v21 -> 3 v41 -> 4 v33 -> 4 v42 -> 3 v23 -> 1 v32 -> 1 v31 -> 2 v22 -> 4 v11 -> 1 v44 -> 1 v13 -> 3
これを並べてみると以下のようになり、確かに解けていることが分かります。
1 2 3 4 +---+---+---+---+ 1 | 1 | 2 | 3 | 4 | +---+---+---+---+ 2 | 3 | 4 | 1 | 2 | +---+---+---+---+ 3 | 2 | 1 | 4 | 3 | +---+---+---+---+ 4 | 4 | 3 | 2 | 1 | +---+---+---+---+
コード例(定理証明)
次は定理証明の例です。サンプルコード(sample/sample2.sml)に全体があります。
(* 命題 f が成り立つことを証明する補助関数 *) fun prove ctx f is_valid = local_ctx ctx (fn ctx => let val not_f = Z3_mk_not (ctx, f) val () = D.Z3_assert_cnstr (ctx, not_f) val m : Z3_model ref = ref (Ptr.NULL()) val ret = D.Z3_check_and_get_model (ctx, m) val ref m = m in case ret of Z3_lbool.Z3_L_FALSE => ... | Z3_lbool.Z3_L_UNDEF => ... | Z3_lbool.Z3_L_TRUE => ... end) fun main () = with_context (fn ctx => let infix 4 == fun p == q = Z3_mk_eq (ctx, p, q) infix 8 $ fun f $ x = Z3_mk_app (ctx, f, Vector.fromList [x]) (* create uninterpreted type *) val U = Z3_mk_uninterpreted_sort (ctx, Z3_mk_string_symbol (ctx, "U")) (* g : U -> U *) val g = Z3_mk_func_decl (ctx, Z3_mk_string_symbol (ctx, "g"), Vector.fromList[U], U) (* create x and y *) val x = Z3_mk_const (ctx, Z3_mk_string_symbol(ctx, "x"), U) val y = Z3_mk_const (ctx, Z3_mk_string_symbol(ctx, "y"), U) in D.Z3_assert_cnstr (ctx, x == y); (* x == y と仮定 *) (* g x == g y となることを証明 *) print "prove: x = y ==> g(x) = g(y)\n"; prove ctx (g $ x == g $ y) Z3_TRUE; (* g (g x) == g y とは(一般には)ならないことを証明 *) print "disprove: x = y implies g(g(x)) = g(y)\n"; prove ctx (g $ (g $ x) == g $ y) Z3_FALSE end)
内容はコメントから察してもらうとして重要なのは prove です。
prove 関数の冒頭部分に注目してみると、上で説明した定理証明の形がそのまま現れていることが分かります。
fun prove ... = ... val not_f = Z3_mk_not (ctx, f) (* 命題 f の否定を作る *) val () = D.Z3_assert_cnstr (ctx, not_f) (* (not f) が成り立つよ と仮定してみる *) val m : Z3_model ref = ref (Ptr.NULL()) val ret = D.Z3_check_and_get_model (ctx, m) (* 否定した命題を満たすモデルがあるか検証 *) ...
その他の例
さらなる例としては冒頭紹介した、 sample ターゲットで使用する
sample/example.sml が z3/path/to/example.c(公式のC APIのサンプル) をSMLに移植したものとなっているので見てみるとよいでしょう。
広範囲のAPIを使用するサンプルコードが多く含まれて居ます*4。
binding/naming規則
以下でbindingと命名の規則を示します。
各APIの説明は公式のC APIドキュメントで確認してください。
関数
C APIと同名の関数が structure Z3 から提供される。
ただしdeprecatedなやつはstructure Z3.Deprecated の中にある。
例えばC言語で Z3_xxx という名前の関数はSMLでは Z3.Z3_xxx という名前になる。
Z3の型
ほぼ全てのopaqueポインタはstructure Z3から提供される。これらはSMLでもopaqueポインタ型になっている。
例えば Z3_ast 型は Z3.Z3_ast (= Z3.Tag.Z3_ast ptr) として表現される。
Z3.Tag.Z3_ast 型はopaqueなのでデリファレンスは出来ないが nullable になっている。(引数経由で受け取るAPIあるから仕方ないんや…)
Enum
全てのenum型はC APIと同名のstructureとして、バリアントは(当然)コンストラクタとして提供される。
またそれぞれのstructureには val fromInt : int -> t と val toInt : t -> int が提供され、int型の値と相互に変換できる。
例えば Z3_symbol_kind は以下のようなシグネチャを持つ。
structure Z3_symbol_kind = struct datatype t = Z3_INT_SYMBOL | Z3_STRING_SYMBOL val fromInt : int -> t val toInt : t -> int end
以上！
SML#用の z3 バインディングを紹介しました！
現状ではCと同じインターフェースしか含んでいないのでSML的な便利インターフェースを提供していきたいです。
次は古参SML#er よんた(@keita44_f4) さんの番です期待しませう +(0ﾟ・∀・) +
