• z3作为微软开发的求解器,其提供的接口在很多应用程序和编程语言中都可以使用。
    > z3prover在CHAINSAWNAVEX中均有使用
  • 在这里关键的作用是想要配和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
  • 最后,关于细节本文记录得不是很多,所以需要一些基础来阅读

环境安装

编译好的二进制版

  1. Github下载最新版:https://github.com/Z3Prover/z3/releases
    Z3prover
  2. 解压后将其中的bin目录添加到环境变量(Unix-like系统可以添加软连接到/usr/bin中)
  3. z3 <filename> 使用

z3py

  1. pip install z3-prover
  2. 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

标签: none

添加新评论