Z3是一款知名的SMT求解器,由微软的首席教授Leonardo de Moura率队打造。该工具获得“2014 The most influential tool paper in the first 20 years of TACAS” 和 “2015 Programming Languages Software Award from ACM SIGPLAN”。

Z3提供了很多的API,这些api支持的语言有C, .NET, and OCaml, Python。当然,z3也可以通过命令行的方式来执行。

1. Z3安装

github , 提供了在不同平台上的安装方法。在Pyhon的虚拟环境下,可以通过以下过程安装。

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install 
venv/bin/z3 -h # z3已结成功安装
...

我们写个简单的Python程序。

1
2
3
4
5
6
ex1.py:
from z3 import *
print(z3.get_version_string())
x = Int('x') # 定义变量x
y = Int('y') #定义变量y
solve(x > 0, y <= 5, x + y == 7) # 求解等式

然后运行(python3 ex1.py),就可以了 (Z3 在默认情况下,只寻找满足所有条件的一组解,而不是找出所有解。)

1.1 Z3求解

Z3的Python API跟标准的SMT-LIB 语言有所不同。比如对于以下的等式:

3x+2yz=13x + 2y - z = 1
$ 3x - 2y + 4z = -2 -x + ½ y = z = 0 $

我们用Z3求解器的Python表示如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
from z3 import *

x = Real('x') # 定义实数
y = Real('y')
z = Real('z')
s = Solver() # 定义solver
s.add(3*x + 2*y - z == 1) # 向solver中添加公式
s.add(2*x - 2*y + 4*z == -2)
s.add(-x + 0.5*y - z == 0)
print(s.check()) # 求解
print(s.model()) # 打赢求解的实例
==========
output:
sat
[y = 3/2, x = 4]

我们定义了三个实数:x, y, z ,并且添加了三个公式。如果公式是可满足的,check() 返回sat;如果不满足,check()返回unsat;当求解器无法判断当前公式是不是可满足的就返回unknown。通过model(),可以得到使得等式成立的解的例子。

事实上,对于大多数的SMT求解器来说,SMT-LIB 是用来描述等式的标准语言,我们对上述的例子重新改写:

1
2
3
4
5
6
7
8
9
10
11
12
ex1.smt
(echo "starting Z3...")
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (=(-(+(* 3 x) (* 2 y)) z) 1))
(assert (=(+(-(* 2 x) (* 2 y)) (* 4 z)) -2))
(assert (=(-(+ (- 0 x) (* 0.5 y)) z) 0))
(check-sat)
(get-model)
----------------------
~ z3 -smt2 ex1.smt //执行命令,

在SMT-LIB 语言里,echo用于输出信息,命令 assert 用于添加一个公式到Z3的栈中,declare-const: 定义一个常量。在本文中,只介绍Python接口。

1.2 Z3 支持的逻辑

propositional logic
theory of equality
uninterpreted functions
arrays
arithmetic
algebraic data-types
bit-vectors
floating points
sequences
strings

1.3 Basic SAT

(TieShirt)(¬TieShirt)(¬Tie¬Shirt)(Tie \lor Shirt) \land (\neg Tie \lor Shirt) \land (\neg Tie \lor \neg Shirt)

1
2
3
4
5
6
7
8
Tie, Shirt = Bools('Tie Shirt')
s = Solver()
s.add(Or(Tie, Shirt), Or(Not(Tie), Shirt), Or(Not(Tie), Not(Shirt)))
print(s.check())
print(s.model())
--------------------
sat
[Tie = False, Shirt = True]

1.4 Basic SMT

1
2
3
4
5
6
7
8
9
10
11
12
I = IntSort()
f = Function('f', I, I)
x, y, z = Ints('x y z')
A = Array('A',I,I)

fml = Implies(x + 2 == y, f(Select(Store(A, x, 3), y - 2)) == f(y - x + 1))

s = Solver()
s.add(Not(fml))
print (s.check())
-------------------
unsat

1.5 Pyhon接口

s = Solver() // 创建
s.add(ψ\psi) // 添加公式
s.assert_and_track(ψ,l\psi, l)
s.push() // 创建局部
s.pop()
s.check()
s.check( l1,l2,...,lnl_1,l_2,...,l_n )
s.model() // 获得模型
s.proof()
s.unsat_core()
s.statistics()

In some applications, we want to explore several similar problems that share several definitions and assertions. We can use the commands push and pop for doing that. Z3 maintains a global stack of declarations and assertions. The command push creates a new scope by saving the current stack size. The command pop removes any assertion or declaration performed between it and the matching push.

2 逻辑语言

2.1 Terms 项

2.3.1 CNF范式

一个SAT的实例是一个有n个布尔变量的布尔表达式。通常情况下,我们假设这些变量通过Conjuctive Normal Form (CNF,中文好奇葩叫做“合取范式”)的形式给出。比如以下公式,是一个合法的SAT输入公式(CNF范式):

(x1¬x2)(x2x3)(¬x1x2¬x3)(x_1 \lor \neg x_2) \land (x_2 \lor x_3) \land ( \neg x_1 \lor x_2 \lor \neg x_3)

其中,一个conjuncts被称为一个clause(比如(x1¬x2)(x_1 \lor \neg x_2), 一个clause中,一个disjunct称为literal,比如(x1¬x2)(x_1 \lor \neg x_2)中的x1x_1¬x2\neg x_2

2.2 Logical connectives 逻辑连接词

2.3 Quantifiers, variables 量词,变量

2.4 Z3中的量词引擎

[40] E-matching

[13, 24, 43, 52] Model-based Quantifier Instantiation (MBQI)

[5] Quantifier Elimination

[46] Alternating Quantified Satisfaction

[26] Horn Clauses

[11] Quantified Horn Clauses

[47] EPR (deprecated, covered by MBQI)

[41] Superposition (deprecated)

[9] QSAT - game based solving