申明：本文翻譯自rise4fun，翻譯與原文存在一些差異。

z3是由微軟公司開發的一個優秀的SMT求解器（也就定理證明器），它能夠檢查邏輯表示式的可滿足性。

使用方式

z3是一個底層的工具，它最好是作為一個元件應用到其它需要求解邏輯公式的工具中。為了方便使用，z3提供了很多的API，這些api支援的語言有C, .NET, and OCaml。當然，z3也可以通過命令列的方式來執行。（最新版本的z3可以到這裡下載，微軟官網上只更新到4.1）

基本命令

Z3的輸入格式是SMT-LIB2.0標準（想進一步瞭解smt-lib標準，可以參考這個網站）的一個拓展，一個Z3指令碼就是一個命令序列。你可以使用help

(echo "starting Z3...")
(declare-const a Int)
(declare-fun f (Int Bool) Int)

這個例子中申明瞭一個函式，有兩個引數，分別為Int型和Bool型，返回一個Int型的值

命令assert用於新增一個公式到z3的棧中，如果對於輸入的所有公式，z3能夠給出一種解釋（對於使用者定義的常量和函式），使得所有的公式都成立，那麼我麼說這個公式集是可滿足的。看下面這個例子：

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

這個例子中第一個斷言表示常量a必須大於10，第二個斷言表示引數為a和true的函式f必須返回一個小於100的值。check-sat命令告訴求解器去求解當前z3棧中公式的可滿足性。如果棧中的公式是可滿足的，z3返回sat；如果不滿足，z3返回unsat；當求解器無法判斷當前公式是不是可滿足的就返回unknown。

如果命令集是可滿足的，我們可以使用get-model

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

我們用z3去求解這個公式集，得到的結果如下：

sat
(model 
  (define-fun a () Int
    11)
  (define-fun f ((x!1 Int) (x!2 Bool)) Int
    (ite (and (= x!1 11) (= x!2 true)) 0
      0))
)

結果中sat指的是該公式集是可滿足的，而model中的內容則是對公式集的一個解釋，看起來不太好理解，我們下面對model中的解釋方式進行說明。

model中的解釋是通過定義的方式給定的，例如

(define-fun a () Int [val])

這個定義申明函式a的返回值為[val]

(define-fun f ((x!1 Int) (x!2 Bool)) Int
   ...
)

這個定義跟程式語言中的函式申明類似。其中x1和x2是z3給出的函式f的引數解釋。在上面的例子中，對f的定義使用了ite（if-than-else）的方式。

(ite (and (= x!1 11) (= x!2 false)) 21 0)

這個表示式是說當x1=11並且x2=false的時候函式返回21，否則返回0。這樣就給出了一個使得公式集滿足的解。

使用範圍

有時候在解決一些相似的問題的時候，我們希望去複用一些定義和斷言，z3提供了push和pop命令去實現這個功能。上面也提到了，z3會維持一個全域性的棧，定義和斷言就儲存在棧中。Push命令通過儲存當前棧大小的方式建立一個範圍。Pop命令則是移除與之相匹配的push之間的所有斷言和申明。

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(push)
(assert (= (+ x y) 10))
(assert (= (+ x (* 2 y)) 20))
(check-sat)
(pop) ; remove the two assertions
(push) 
(assert (= (+ (* 3 x) y) 10))
(assert (= (+ (* 2 x) (* 2 y)) 21))
(check-sat)
(declare-const p Bool)
(pop)
(assert p) ; error, since declaration of p was removed from the stack

未完待續。。。。。。