z3 (smtソルバ) で遊ぶ

  • 0
    いいね
  • 0
    コメント

    z3とは?

    z3はMicrosoft Researchによって開発されたSMTソルバ (smt solver) です。IntやBoolだけでなく、Listや二分木を用いて書いた論理式の充足可能性をチェックすることができます。Python、Java、C、OCamlなどから使うこともできます。

    http://rise4fun.com/z3/tutorial/guide
    公式のチュートリアルページです。z3をインストールせずに遊ぶことができます。

    z3によって示せる例、および本記事の目標

    Int を使った論理式

    x <- 1
    y <- 2
    forall a ∈ Int . a + x < a + y
    

    ListとIntを使った論理式

    sum :: List Int -> Int
    sum = List Int の要素和を求める関数
    
    forall xs ∈ List Int .
     forall ys ∈ List Int .
      forall a ∈ Int .
       sum xs > sum ys => sum (a:xs) > sum (a:ys)
    

    Pairとか二分木を定義して使ったり再帰関数を定義して使ったりできます。
    ただ、なんでも示せるわけではなく、複雑(?)になるに従ってtimeoutとかunknownが返って来ます。

    準備

    関数や定数、forall、再帰関数の書き方を紹介します。Lispみたいなシンタックスです。

    assert / declare-const / declare-fun / check-sat

    z3は、assertコマンドによって内部スタックに加えられた論理式らが充足可能であるかを判定します。

    (declare-const a Int)
    (declare-fun f (Int Bool) Int)
    (assert (> a 10))
    (assert (< (f a true) 100))
    (check-sat)
    

    これは、assertされている論理式を満たすような
    ・ Int型定数a
    ・ Int->Bool->Int型関数f
    が存在するかを判定しています。

    定数

    define-constコマンドを使います。

    ; n <- 55
    (define-const n Int
     55 )
    
    ; x <- []
    (define-const x (List Int)
     nil )
    

    関数

    define-funコマンドを使います。

    ; plus x y = x + y
    (define-fun plus ((x  Int )(y  Int )) Int 
    (+ x y) )
    
    ; add1 x = x + 1
    (define-fun add1 ((x  Int )) Int 
    (+ x 1) )
    

    forall

    forallコマンドを使います。

    ; forall x ∈ Int . x > 1 => x > 0
    (forall ((x Int))
     (=>
      (> x 1) 
      (> x 0)
     )
    )
    

    if-then-else

    iteコマンドが準備されています。

    ; if b then a1 else a2
    (ite b a1 a2)
    

    List

    declare-datatypesによってデータ型をユーザが定義できます。

    ; List T = nil | cons T (List T)
    (declare-datatypes (T) ((List nil (cons (head T) (tail List)))))
    

    head,tail関数も同時に定義しちゃえます。

    再帰関数

    define-funコマンドでは再帰関数を定義できず、少し変な書き方をします。

    ; sum = List Int の要素和を求める関数
    (declare-fun sum ((List Int)) Int)
    (assert (forall ((xs (List Int)))
              (ite (= nil xs)
                   (= 0           (sum xs))
                   (= (+ (head xs) (sum (tail xs))) (sum xs)))))
    

    まず、declare-funコマンドによってsumという関数を宣言します。
    次に、forallコマンドによってsumの性質を記述します。
    そして、その性質をassertコマンドによってz3内部スタックに加えます。

    z3を書いてみる

    これで、準備はできました。目標にした式らをz3で書いてみます。

    Intを使った論理式をz3で書く

    x <- 1
    y <- 2
    forall a ∈ Int . a + x < a + y
    

    は、

    (define-const x Int 1)
    (define-const y Int 2)
    (assert 
     (forall ((a Int))
      (< (+ a x) (+ a y))
     )
    )
    (check-sat)
    

    となる。

    List Intを使った論理式をz3で書く

    sum :: List Int -> Int
    sum = List Int の要素和を求める関数
    
    forall xs ∈ List Int .
     forall ys ∈ List Int .
      forall a ∈ Int .
       sum xs > sum ys => sum (a:xs) > sum (a:ys)
    

    (declare-fun sum ((List Int)) Int)
    (assert (forall ((xs (List Int)))
              (ite (= nil xs)
                   (= 0                 (sum xs))
                   (= (+ (head xs) (sum (tail xs))) (sum xs)))))
    (assert (not
     (forall ((xs (List Int)) (ys (List Int)) (a Int))
      (=>
       (> (sum xs) (sum ys))
       (> (sum (cons a xs)) (sum (cons a ys)))
      )
     )
    ))
    

    となる。

    assertのところで、forall文にnotを付け、unsatが返ってくることを期待しています。
    つまり、

    exists xs ∈ List Int .
     exists ys ∈ List Int .
      exists a ∈ Int .
       not (sum xs > sum ys => sum (a:xs) > sum (a:ys))
    

    が成立しないことを期待しています。

    おわりに

    z3を使う機会があったので、少しまとめたものを書いてみました。
    使い方におかしい点がありましたら、指摘していただきたいです。