SMT-LIB語言簡介
smt-lib是smt solver的輸入語言
用來定義"決策問題實例"(decision procedure problem instance)
SMT-LIB支持的theory
- QF: for the restriction to quantifier-free formulas
- A or AX: for arrays without or with extensionality
- BV: for fixed-size bit-vectors
- FP: for Floating-Point
- IA: for integer arithmetic
- RA: for real arithmetic
- IRA: for mixed integer arithmetic
- IDL: for integer difference logic
- RDL: for rational difference logic
- L before IA, RA, or IRA: for the linear fragment of those arithmetics
- N before IA, RA, or IRA: for the nonlinear fragment of those arithmetics
- UF: for the extension allowing free sort and function symbols
舉例：命題邏輯(Boolean)
用SMT-LIB語言表達如下問題：
驗證表達式 \((a\lor b)\land\neg a\) 是否可滿足
SMT-LIB語言中定義函數(從定義域到值域的映射)
(declare-fun <函數名> <定義域> <值域>)
SMT-LIB語言中定義變量 (定義域為空的函數)
如下聲明一個布爾變量a
(declare-fun a () Bool)
SMT-LIB語言中的布爾常量和邏輯聯結詞
定義布爾變量之間的約束關系時需要用到：
布爾theory SMT-LIB語言 \(TRUE\) true\(FALSE\) false\(\neg a\) (not a)\(a\Rightarrow b\) (=> a b)\(a\land b\) (and a b)\(a\lor b\) (or a b)\(a\oplus b\) (xor a b)
\((a\lor b)\land\neg a\) 可以用以上SMT-LIB語言表示為
(and (or a b) (not a))
SMT-LIB語言中定義約束
用assert聲明約束
(assert (and (or a b) (not a)))
聲明了全部約束后，可以用
(check-sat)
檢查所有約束是否可以同時滿足；
若sat/滿足，可以用
(get-model)
獲得一組滿足約束的變量賦值；
若unsat/不滿足，可以用
(get-unsat-core)
獲得所有約束條件的一個子集，該子集是不可滿足的
算術理論(Arithmetic)
SMT-LIB語言支持定義整數和實數 之上的算術邏輯
變量的類型在SMT-LIB中被記為sort
SMT-LIB語法中有一些是對所有變量類型有效的
如：(= x y)，表示兩個相同類型的變量相等
注：不等關系(disequal a b c)表示a, b, c兩兩不相等
SMT-LIB中的ite表達式
(ite c x y) 其中c為布爾表達式，x 和y為相同類型的表達式
SMT-LIB語言提供算術邏輯的定義和操作
類型定義： 整數類型Int 和實數類型Real
操作符：
操作名 SMT-LIB語言 addition +subtraction -unary minus -multiplication *division /(reals)div(integers)remainder mod(integers only)relations < > <= >=
大部分操作符支持多個操作數，如(+ x y z)， 表示三個相同類型的數相加
整數和十進制小數可以寫成字面量， 如(+ (* 2 x) 3.15)
注：負數可以用一元操作符得到，如(- 2)， 不支持直接寫成-2
比特向量算術理論(Bit-Vector Arithmetic)
SMT-LIB語言提供了一種帶參數的類型 BitVec，參數即為BitVec的位長
BitVec表示一個比特向量，不同位長的BitVec為不同類型
如下定義一種BitVec的變量，下划線_ 標識參數化類型，8表示這種BitVec的位長為8：
(declare-fun a () (_ BitVec 8))
比特向量常量可以用2進制或16進制給出，如下給上面定義的變量a賦值：
(assert (= a #b11110000))
(assert (= a #xf0))
比特向量的操作：
比特向量可以看作是一個整數的原碼或是補碼
因此有些操作會對應兩種不同操作符
操作名 原碼 補碼 addition bvadd bvadd subtraction bvsub bvsub multiplication bvmul bvmul division bvudiv bvsdiv remainder bvurem bvsrem relations bvult, bvugt,
bvule,bvugebvslt, bvsgt,
bvsle,bvsgeleft shift bvshl bvshl right shift bvlshr bvashr 比特向量還支持拼接
concat和提取extract操作
數組理論(Arrays)
數組：從索引（數組中為數組下標）類型到數組元素類型的映射
所以數組變量定義形如：(declare-fun a () (Array Int Real))
取對應下標的元素\(a[i]\)：(select a i)
更新對應下標中元素的值\(a\{i\leftarrow e\}\)： (store a i e)
等式(Equalities)
自定義類型：
如下所示：其中0是指該類型my_sort的元素維度（arity, 上述Array類型的元素維度為2， 如果有Set類型的話，其元素維度為1）
(declare-sort my_sort 0)
; 定義變量
(declare-fun a () my_sort)
(declare-fun b () my_sort)
(declare-fun c () my_sort)
; 聲明等式和不等式約束
(assert (= a b))
(assert (disequal a b c))