Z3求解器基本指南

這是部落客 alu_xd 翻譯的官網上的z3手冊，但是不全面，想看全面的手冊見官網手冊：z3手冊

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

使用方式

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

基本指令

Z3的輸入格式是SMT-LIB2.0标準（想進一步了解smt-lib标準，可以參考這個網站）的一個拓展，一個Z3腳本就是一個指令序列。你可以使用help指令去檢視一系列可用的指令。echo指令用于顯示一個資訊。Z3的内部維持着一個棧，這個棧裡面儲存着使用者輸入的公式和申明（常量的和函數的）。declare-const指令用于申明一個給定類型的常量，declare-fun指令則用于申明一個函數。

(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指令去擷取一個使z3棧中所有公式內建立解釋。

(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
           

配置

set-option指令用來配置z3，該指令有幾個選項去控制z3的行為。這些選項中的一部分隻能夠在斷言和申明指令之前設定。使用reset指令可以擦出所有的斷言和申明，在使用reset指令後，所有的配置選項都可以設定了。

(set-option :print-success true) 
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(set-option :produce-proofs true) ; enable proof generation
(declare-const x Int)
(set-option :produce-proofs false) ; error, cannot change this option after a declaration or assertion
(echo "before reset")
(reset)
(set-option :produce-proofs false) ; ok
           

其中配置選項print-success true是相當有用的，這個選項可以用來判斷你的輸入檔案中的指令是否有錯誤，如果指令沒有錯誤，會輸出success，有錯的話則會報出具體的出錯位置。

命題邏輯

z3中預定義的類型Bool是所有的Boolean命題表達式的類型。Z3支援常用的Boolean運算符and，or，xor，not，=>(蘊含)，ite（if-than-else）。蘊含式通常用=表示。下面的例子中我們展示了如何證明這個命題：如果p蘊含q并且q蘊含r，那麼p蘊含r。我們通過證明該命題的否命題是不滿足的方式來證明該命題。注意該例子中我們給定了函數conjecture一個具體的定義。

(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(define-fun conjecture () Bool
    (=> (and (=> p q) (=> q r))
        (=> p r)))
(assert (not conjecture))
(check-sat)
           

無解釋的函數與常量

SMT公式的基本建構單元就是常量和函數，常量說白了就是沒有參數的函數，是以，基本的建構單元事實上都是函數。

(declare-fun f (Int) Int)
(declare-fun a () Int) ; a is a constant
(declare-const b Int) ; syntax sugar for (declare-fun b () Int)
(assert (> a 20))
(assert (> b a))
(assert (= (f 10) 1))
(check-sat)
(get-model)
           

不像程式語言，函數有邊際效應，能夠抛異常或者沒有傳回值，傳統的一階邏輯表達式函數沒有邊際效應，它是完整的。

純的一階邏輯函數和常量是無解釋的，或者說是自由的，這意味着沒有一個先天的解釋是附加在改表達式上的。這和那些有理論簽名的函數形成對比，比如數學上函數+有一個固定的标準的解釋（對兩個數進行加操作）。無解釋的函數和常量是最大限度自由的，它們允許任何和限制一緻的解釋。

為了說明無解釋的類型，在下面的例子中，我們定義了一個無解釋的類型A，并且定義了兩個類型為A的常量x和y。

(declare-sort A)
(declare-const x A)
(declare-const y A)
(declare-fun f (A) A)
(assert (= (f (f x)) x))
(assert (= (f x) y))
(assert (not (= x y)))
(check-sat)
(get-model)
           

求解該限制集得到的結果如下：

sat
(model 
  ;; universe for A:
  ;;   A!val!0 A!val!1 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun A!val!0 () A)
  (declare-fun A!val!1 () A)
  ;; cardinality constraint:
  (forall ((x A)) (or (= x A!val!0) (= x A!val!1)))
  ;; -----------
  (define-fun y () A
    A!val!1)
  (define-fun x () A
    A!val!0)
  (define-fun f ((x!1 A)) A
    (ite (= x!1 A!val!0) A!val!1
    (ite (= x!1 A!val!1) A!val!0
      A!val!1)))
)
           

結果模型中為A給定了一個抽象的值，因為A是無解釋的。