z3-solver的安装和使用

发表于 更新于 分类于

Z3的安装和使用

Windows上的安装

可以直接在Z3的GitHub主页上下载对应版本的，然后直接配置路径即可。

使用下面的命令检查是否安装成功：

1
z3 --version

如果安装成功了会显示z3的版本信息。

Z3的使用

Z3使用SMTLIB格式。具体的可以学习：Introduction | Online Z3 Guide。这是一种类似于Lisp的语言。关于Lisp，我推荐学习SICP(Structure and Interpretation of Computer Science)。

基本命令

基本运行方法

打印：(echo "starting z3...")。

声明常量：(declare-const a Int)。

声明函数：(declare-fun f (Int Bool) Int)。

如果你在example.smt2文件中写入下面的代码（我这里就使用Lisp的高亮了）：

1
2
3
(echo "starting Z3...")
(declare-const a Int)
(declare-fun f (Int Bool) Int)

并且运行：

1
z3 example.smt2

你应该可以看见：

1
starting Z3...

被打印出来了。

求解SAT问题

下面我们介绍Z3中比较重要的几个命令：

添加约束：(assert (< a 10))。

判断是否可满足（satisfiable）：(check-sat)。

要求给出可满足的一个赋值：(get-model)。

1
2
3
4
5
6
(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (< a 10))
(assert (> (f a true) 100))
(check-sat)
(get-model)

对于这段代码实际上就是在求解下面这个SAT问题是否可满足：

对于这个问题，Z3给出的答案是：

1
2
3
4
5
6
7
sat
(
  (define-fun a () Int
    0)
  (define-fun f ((x!0 Int) (x!1 Bool)) Int
    101)
)

这里的常量实际上也是一个函数，它不接受任何的参数，返回一个Int类型的数字。上面的解答意味着我们的SAT问题是可满足的，同时一个可满足的赋值为：

设置作用域（Scopes）

push命令将会创建一个新的作用域，里面存储着所有全局的定义、约束等。

pop则将会将作用域里所有的语句弹出。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
(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)

配置Z3（Configuration）

使用set-option，下面是一个例子：

1
2
3
4
5
6
7
8
9
10
(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)
(assert (= x 1))
(set-option :produce-proofs false) ; error, cannot change this option after an assertion
(echo "before reset")
(reset)
(set-option :produce-proofs false) ; ok

其他命令

(display t)会把式子变得漂亮一点，(simplify t)则会化简式子。

(define-sort [symbol] ([params_type]+) [sort])表示创建一个新的数据类型。

1
(define-sort List-Set (T) (Array (List T) Bool))

就会创建一个类型List-Set，这个类型要求一个参数T，并且返回一个类似于Map的数据类型。

命题逻辑（Propositional Logic）

Z3中已经预先定义好了Bool类型，并且支持and、or、xor、=>、ite(if-then-else)、=(实际上意味着)。

1
2
3
4
5
6
7
8
(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)

define-fun实际上定义了一个Macro。

如果要证明一个公式，也就是证明总是为真的，那么我们就要说明总是为假的，也就是说明是一个不可满足的公式。

不可满足的核心（Unsatisfiable Cores）

1
2
3
4
5
6
7
8
9
10
11
12
(set-option :produce-unsat-cores true)
(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(declare-const s Bool)
(declare-const t Bool)
(assert (! p :named +p))
(assert (! q :named +q))
(assert (! r :named +r))
(assert (! (not (or p q)) :named -p-or-q))
(check-sat)
(get-unsat-core)

我们在这里把公式取了一个名字为+p。

1
2
unsat
(+q -p-or-q)

最后发现产生矛盾的核心集是：。

未解读的函数和变量

我们完全可以扔给Z3一些它不知道什么含义的函数和变量，让它计算出一个理论，使得约束满足。

例如：

1
2
3
4
5
6
7
8
9
(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给出的结果是：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
sat
(
  ;; universe for A:
  ;;   A!val!1 A!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun A!val!1 () A)
  (declare-fun A!val!0 () A)
  ;; cardinality constraint:
  (forall ((x A)) (or (= x A!val!1) (= x A!val!0)))
  ;; -----------
  (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))
)

这个解读代表着：类型有两个基本的元素和，同时有。然后Z3给出了这个问题的一个可能的赋值：

创建新的类型

可以参看 Lisp 的语法。

理论（Theory）

理论大约等于一组公理。

Z3支持的理论有：Arithmetic、Bitvectors、IEEE Floats、Arrays、Datatypes、Strings、Sequences、Sequences、Regular Expressions、Unicode Characters、Special Relations。

Arithmetic

Logic Fragment Solver Example
LRA Linear Real Arithmetic Dual Simplex
LIA Linear Integer Arithmetic CutSat
LIRA Mixed Real/Integer Cuts + Branch
IDL Integer Difference Logic Floyd-Warshall
RDL Real Difference Logic Bellman-Ford
UTVPI Unit two-variable per inequality
NRA Polynomial Real Arithmetic Model based CAD, Incremental Linearization

策略（Strategies）

这个其实和 Coq证明器有点像，请参看Software Foundations。