【Z3ソルバー】関数の define と declare

z3 プログラム合成

Z3 ソルバーについてのメモ。
主なトピックは SMT-LIB の define と declare について。

Z3 と SMT-LIB

Z3 は言わずと知れた SMT ソルバーである。オープンソースであり、Github のページにインストール手順も載っている。この手順の通りにやれば（少なくとも Ubuntu 上では）簡単にインストールできる。ソルバーに与えられる命令列の形式として SMT-LIB がサポートされているため、ユーザは解きたい論理式を SMT-LIB の形式で Z3 に与えればよい。また、各種プログラミング言語から Z3 ソルバーへアクセスするためのインターフェースも充実しており、アルゴリズムの一部として SMT ソルバーを使用したいときは Z3 は使い勝手がよい。詳しくは Github のページを参照。

SMT-LIB 上での関数定義

define-fun（独自の関数を定義）

SMT-LIB では define-fun 命令を用いて関数を定義できる。
試しに2つの引数のうち最大値を返す max 関数を以下のように定義してみる

(define-fun max ((x Int) (y Int)) Int 
    (ite (>= x y) x y)
)

(assert (= (max 1 3) 3))

(check-sat)

ここで ite は if-then-else であり、assert によって \text{ max }(1, 3) = 3 であることを表明している。そして、(check-sat) によって assert された制約式が真になりうるか検証する。

もちろんこの制約は真なので、これを Z3 に与えたときの結果は以下のように sat（充足可能）と判定される。

$ z3 f1.smt2 
sat

こんな感じで独自の関数を define-fun によって定義できる。
ちなみに ite や >= などの演算子が使用可能なのはこれらが Core theory に含まれるからである。Core Theory は任意の Theory において暗黙的にインポートされる。詳しくは SMT-LIB の言語仕様 の 3.7.1 章を参照。

declare-fun（未知の関数を定義）

declare-fun では未知の関数を定義できる。
つまり、Z3 に「こんな制約を満たす関数は存在するか？」という問い合わせができる。
たとえば、具体的な定義が不明な max 関数を declare-fun を用いて定義してみる。

(declare-fun max (Int Int) Int)

(assert (= (max 0 1) 1))
(assert (= (max 4 2) 4))

(check-sat)
(get-model)

この実行結果は以下のようになる。

$ z3 f2.smt2 
sat
(
  (define-fun max ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 4) (= x!1 2)) 4
      1))
)

充足可能であることが sat として表示された後、具体的に得られた max 関数が (get-model) 命令により define-fun として表示されている。この関数は「第一引数が 4 で第二引数が 2 のときは 4 を返すけど、それ以外のときは 1 を返す」ものである。最大値を一般的に求める関数は得られなかったが、一応 assert を満たす関数は構成できた。

余談。これは一種のプログラム合成、とくに入出力例からプログラムを合成する inductive synthesis の問題を解いたことになる。ただし、その解は「2引数を最大値を返す」ような一般性のあるものではなく、assert によって与えられた入出力例に overfit したものである。こういう解を出すのではプログラム合成としてはつまらない。もっと一般性の高い解を見つけられるソルバーを開発したい。そういうモチベーションを持っているのが SyGuS というコミュニティである。

t-keita.hatenadiary.jp

define-fun と declare-fun の関係

SMT-LIB の言語仕様を見ると以下のような話がある。

(define-fun f ((x1 σ1) · · · (xn σn)) σ t)
with n ≥ 0 and t not containing f is semantically equivalent to the command sequence
(declare-fun f (σ1 · · · σn) σ)
(assert (forall ((x1 σ1) · · · (xn σn)) (= ( f x1 · · · xn) t))

つまり、

  • (define-fun f ((x1 σ1) · · · (xn σn)) σ t)

という命令は、以下の２つの命令列と意味的に等しい。

  • (declare-fun f (σ1 · · · σn) σ)
  • (assert (forall ((x1 σ1) · · · (xn σn)) (= ( f x1 · · · xn) t))

具体的を考えてみる。さきほど挙げた max 関数の例では

(define-fun max ((x Int) (y Int)) Int 
    (ite (>= x y) x y)
)

と

(declare-fun max (Int Int) Int)
(assert (forall ((x Int) (y Int)) (= (max x y) (ite (>= x y) x y))

が意味的に等しいということ。

以上、当たり前みたいな話でした。