[笔记] Z3prover 学习记录
- z3作为微软开发的求解器，其提供的接口在很多应用程序和编程语言中都可以使用。
> z3prover在CHAINSAW和NAVEX中均有使用- 在这里关键的作用是想要配和CodeQL，通过CodeQL提取路径约束，然后用Z3求解约束
- 其实关于如何用CodeQL提取出可以作为z3输入的约束还是一头雾水...但是这不妨碍先学习z3的使用，说不定可以找到一些灵感完成两者的结合。（应该会有办法的，要不这条研究路线就断了）
- 后期可能需要造一些轮子，这么说来还是需要花挺多时间的（尤其是假期即将结束，需要挺多时间复习开学期考功课）
- 官方使用文档：https://rise4fun.com/z3/tutorialcontent/guide
- z3py功能手册：https://z3prover.github.io/api/html/namespacez3py.html
- z3py使用文档：https://ericpony.github.io/z3py-tutorial/guide-examples.htm
> 如果二进制版的z3不便于后期结合，还需要花时间学下z3py- z3所使用的语法标准：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
- 最后，关于细节本文记录得不是很多，所以需要一些基础来阅读
环境安装
编译好的二进制版
- Github下载最新版：https://github.com/Z3Prover/z3/releases
- 解压后将其中的bin目录添加到环境变量（Unix-like系统可以添加软连接到/usr/bin中）
z3 <filename>使用
z3py
- pip install z3-prover
from z3 import *使用
> 注意在z3py中，很多语句被封装成了对象/类方法，但是基本求解逻辑还是一样的，取决于后期打算采用何种形式
基本语法
指令结构
z3指令有一套自己的结构，一般称为三地址码，其遵循的标准在引言中有链接。
基本的构成为 操作符 操作数1 操作数2
常量(constants)和函数(functions)
这是z3指令中最常见的两种结构，然而本质上常量只是作为一个没有参数的函数，其求解结果也以函数结构所表现。
(declare-fun f (Int) Int) ; 这里f是接受Int类型的函数
(declare-fun a () Int) ; a可以看成常量
(declare-const b Int) ; 语法糖写法，声明一个常量
与编程语言中函数不同的是，z3中的函数可以视为一个未解释的公式，不会在运行时抛出异常，也不会出现没有返回值的情况。专业术语将其称之为一阶逻辑或者谓词演算——百度百科。一阶逻辑中的“函数”是“未定义”的，意思就是不存在一种类似于四则运算一般固定的解释模式(model)。只要任何符合约束条件的model，都可以作为一种解释，而check-set就是用来求解的。
很抽象，可以看下面例子大概理解下。
用z3证明 f(f(x)) = x, f(x)=y, x!=y约束的存在性（给出一种可能性解释），并且还定义了一个抽象的类型（sort在z3中表示类型，使用declare-sort定义类型）：
(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)
需要特别注意下z3函数的使用方式与编程语言不同：编程语言通过(x1,x2,x3)方式传参，而z3将函数视为一个运算符号通过类似三地址码的方式传参 —— 函数符号 x1 x2 x3输出：
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 x () A
A!val!0)
(define-fun y () A
A!val!1)
(define-fun f ((x!0 A)) A
(ite (= x!0 A!val!1) A!val!0
A!val!1))
)
生成的模型为A引入了抽象值。
算数运算
基本运算
z3内置了对于整数和实数等数学类型的支持，而且貌似最新版已经合并了原先的插件——z3str，可以进行字符串处理，关于这部分文档似乎没有详细说明...
declare-const可以用于声明整数和实数常量
如：
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)
声明完常量后，就可以在后续的式子中使用这些变量，式子中可以包含常用的数学运算符如:
+ - x div/mod/ram。
check-sat & get-model
check-sat是高频使用的命令，用于对表达式求解，基本上就是为每个常数分配一个数字。如果存在一种解使得所有式子为真，那么结果就为sat，并且称这个解释为一个model，使用get-model可以查看；如果不存在解释，则结果为unsat，也无法获取可行的model。
例子：
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)
(assert (> a (+ b 2)))
(assert (= a (+ (* 2 c) 10)))
(assert (<= (+ c b) 1000))
(assert (>= d e))
(check-sat)
(get-model)
输出：
sat
(model
(define-fun c () Int
0)
(define-fun b () Int
0)
(define-fun e () Real
0.0)
(define-fun d () Real
0.0)
(define-fun a () Int
10)
)
类型转换
在z3中Int类型和Real类型不会自动互相转换，但是借助函数to-Real（参数为一个整数）可以将整数化为实数。
例子：
(assert (> e (+ (to_real (+ a b)) 2.0)))
(assert (= d (+ (to_real c) 0.5)))
非线性运算特性
当式子中有类似(* t s)的实数运算时称为非线性式，这种式子求解极其困难，导致z3在求解非线性问题的时候不一定总能确定是否有解。当无法确定是否可以求解时使用check-sat会返回unknow；当然，部分特殊的非线性式依然可以确定可满足性。
例子：
(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)
(echo "Z3 does not always find solutions to non-linear problems")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(echo "yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...")
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (= (* x x) (+ x 2.0)))
(assert (= (* x y) x))
(assert (= (* (- y 1.0) z) 1.0))
(check-sat)
(reset)
(echo "When presented only non-linear constraints over reals, Z3 uses a specialized complete solver")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)
输出：
sat
(model
(define-fun a () Int
(- 3))
)
Z3 does not always find solutions to non-linear problems
unknown
yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...
unsat
When presented only non-linear constraints over reals, Z3 uses a specialized complete solver
sat
(model
(define-fun b () Real
(/ 1.0 8.0))
(define-fun c () Real
(/ 1535.0 64.0))
)
除法运算
z3支持除法、求模和求余运算，这些运算在底层都会被映射成乘法。
注意在实数除法的时候用符号/，因为实数没有求模和取余。例子：
(declare-const a Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(declare-const r4 Int)
(declare-const r5 Int)
(declare-const r6 Int)
(assert (= a 10))
(assert (= r1 (div a 4))) ; integer division
(assert (= r2 (mod a 4))) ; mod
(assert (= r3 (rem a 4))) ; remainder
(assert (= r4 (div a (- 4)))) ; integer division
(assert (= r5 (mod a (- 4)))) ; mod
(assert (= r6 (rem a (- 4)))) ; remainder
(declare-const b Real)
(declare-const c Real)
(assert (>= b (/ c 3.0)))
(assert (>= c 20.0))
(check-sat)
(get-model)
输出：
sat
(model
(define-fun c () Real
20.0)
(define-fun b () Real
(/ 20.0 3.0))
(define-fun r6 () Int
(- 2))
(define-fun r5 () Int
2)
(define-fun r4 () Int
(- 2))
(define-fun r3 () Int
2)
(define-fun r2 () Int
2)
(define-fun r1 () Int
2)
(define-fun a () Int
10)
)
z3有一个很有意思的地方，就是不会发生除0错误，因为除0操作是未定义的，在求解的时候可以被定义为一个函数。
例如：
(declare-const a Real)
; The following formula is satisfiable since division by zero is not specified.
(assert (= (/ a 0.0) 10.0))
(check-sat)
(get-model)
; Although division by zero is not specified, division is still a function.
; So, (/ a 0.0) cannot evaluated to 10.0 and 2.0.
(assert (= (/ a 0.0) 2.0))
(check-sat)
输出：
sat
(model
(define-fun a () Real
1.0)
(define-fun /0 ((x!0 Real) (x!1 Real)) Real
10.0)
)
unsat
如果对上述行为不满意还可以使用ite语句自定义除法规则：
; defining my own division operator where x/0.0 == 0.0 for every x.
(define-fun mydiv ((x Real) (y Real)) Real
(if (not (= y 0.0))
(/ x y)
0.0))
(declare-const a Real)
(declare-const b Real)
(assert (>= (mydiv a b) 1.0))
(assert (= b 0.0))
(check-sat)
关于ite语句：
其实就是if-then-else语句，其结构为(if 条件 真返回值 假返回值)
此处判断被除数是否为0来返回不同结果
位向量
暂略，用到的不多
数组
常用数组操作
- 数组定义：
(declare-const a1 (Array Int Int))
这是使用了语法糖的定义方式，原生定义方式如下：
(define-fun a1 () (Array Int Int) [val])
例如：(define-fun a2 () (Array Int Int) ((as const (Array Int Int)) 0)) - 取出值：
(select a i)
a-数组；i-下标；返回：a数组下标对应值
- 存入值：
(store a i v)
a-数组；i-下标；v-新值；返回：数组本身
例子：
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(declare-const a3 (Array Int Int))
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)
输出：
sat
(model
(define-fun y () Int
0)
(define-fun a1 () (Array Int Int)
(store ((as const (Array Int Int)) 1) 0 0))
(define-fun x () Int
0)
(define-fun z () Int
0)
(define-fun a2 () (Array Int Int)
((as const (Array Int Int)) 0))
(define-fun a3 () (Array Int Int)
((as const (Array Int Int)) 0))
)
常数数组
当数组中每个索引都指向同一个值就变成了常数数组。可以使用as const (Array T1 T2)结构构造一个常数数组，该结构会返回指定类型的数组。原文档对这块的介绍不是很详细，我提取了主要的语句结构如下：
(declare-const a (Array Int Int))
(assert (= a ((as const (Array Int Int)) 1)))
第一句声明一个数组，第二句用断言的方式将该数组约束为常数数组。
例子：
(declare-const all1 (Array Int Int))
(declare-const a Int)
(declare-const i Int)
(assert (= all1 ((as const (Array Int Int)) 1)))
(assert (= a (select all1 i)))
(check-sat)
(get-model)
(assert (not (= a 1)))
(check-sat)
输出：
sat
(model
(define-fun a () Int
1)
(define-fun all1 () (Array Int Int)
((as const (Array Int Int)) 1))
(define-fun i () Int
0)
)
unsat
