[笔记] 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指令中最常见的两种结构，然而本质上常量只是作为一个没有参数的函数，其求解结果也以函数结构所表现。
与编程语言中函数不同的是，z3中的函数可以视为一个未解释的公式，不会在运行时抛出异常，也不会出现没有返回值的情况。专业术语将其称之为一阶逻辑或者谓词演算——百度百科。一阶逻辑中的“函数”是“未定义”的，意思就是不存在一种类似于四则运算一般固定的解释模式(model)。只要任何符合约束条件的model，都可以作为一种解释，而check-set就是用来求解的。
很抽象，可以看下面例子大概理解下。
用z3证明 f(f(x)) = x, f(x)=y, x!=y约束的存在性（给出一种可能性解释），并且还定义了一个抽象的类型（sort在z3中表示类型，使用declare-sort定义类型）：
需要特别注意下z3函数的使用方式与编程语言不同：编程语言通过(x1,x2,x3)方式传参，而z3将函数视为一个运算符号通过类似三地址码的方式传参 —— 函数符号 x1 x2 x3输出：
生成的模型为A引入了抽象值。
算数运算
基本运算
z3内置了对于整数和实数等数学类型的支持，而且貌似最新版已经合并了原先的插件——z3str，可以进行字符串处理，关于这部分文档似乎没有详细说明...
declare-const可以用于声明整数和实数常量
如：
声明完常量后，就可以在后续的式子中使用这些变量，式子中可以包含常用的数学运算符如:
+ - x div/mod/ram。
check-sat & get-model
check-sat是高频使用的命令，用于对表达式求解，基本上就是为每个常数分配一个数字。如果存在一种解使得所有式子为真，那么结果就为sat，并且称这个解释为一个model，使用get-model可以查看；如果不存在解释，则结果为unsat，也无法获取可行的model。
例子：
输出：
类型转换
在z3中Int类型和Real类型不会自动互相转换，但是借助函数to-Real（参数为一个整数）可以将整数化为实数。
例子：
非线性运算特性
当式子中有类似(* t s)的实数运算时称为非线性式，这种式子求解极其困难，导致z3在求解非线性问题的时候不一定总能确定是否有解。当无法确定是否可以求解时使用check-sat会返回unknow；当然，部分特殊的非线性式依然可以确定可满足性。
例子：
输出：
除法运算
z3支持除法、求模和求余运算，这些运算在底层都会被映射成乘法。
注意在实数除法的时候用符号/，因为实数没有求模和取余。例子：
输出：
z3有一个很有意思的地方，就是不会发生除0错误，因为除0操作是未定义的，在求解的时候可以被定义为一个函数。
例如：
输出：
如果对上述行为不满意还可以使用ite语句自定义除法规则：
关于ite语句：
其实就是if-then-else语句，其结构为(if 条件 真返回值 假返回值)
此处判断被除数是否为0来返回不同结果
位向量
暂略，用到的不多
数组
常用数组操作
- 数组定义：
(declare-const a1 (Array Int Int))
这是使用了语法糖的定义方式，原生定义方式如下：
(define-fun a1 () (Array Int Int) [val])
例如： - 取出值：
(select a i)
a-数组；i-下标；返回：a数组下标对应值
- 存入值：
(store a i v)
a-数组；i-下标；v-新值；返回：数组本身
例子：
输出：
常数数组
当数组中每个索引都指向同一个值就变成了常数数组。可以使用as const (Array T1 T2)结构构造一个常数数组，该结构会返回指定类型的数组。原文档对这块的介绍不是很详细，我提取了主要的语句结构如下：
第一句声明一个数组，第二句用断言的方式将该数组约束为常数数组。
例子：
输出：