约束求解和抽象解释，是程序分析的两大基石。一般程序分析问题通常都需要转换为各种数学模型，例如图可达性问题、约束求解问题（通常在符号执行、路径敏感分析等场景使用）等，然后进行特定的求解来发现程序中存在的问题。

本文简单对约束求解进行简单介绍。首先会介绍一些关于约束求解的概念，然后会使用z3求解器举例。

1. 约束求解问题

约束求解问题，可以形式化表示为一个三元组的形式 P=<V, D, C>，其中的三个部分，含义分别为：

V：变量的集合，表示为{v1, v2, ..., vn}；

D：变量的值域的集合，即每个变量的取值范围，即变量vi需要在其值域di内取值；

C：约束条件的集合，每个约束条件包含中一个或者多个变量，若ci中包含k个变量，则称该约束是这k个变量集合上的k元约束。

约束求解就是基于这一系列的约束问题，求出来一个解，这个解对所有的约束都满足，并且在自己的值域范围内，如果有这样的一个解，就说这个约束问题是可满足的，否则，就说这个约束问题是不可满足的。

当前，主流的约束求解器主要有两种理论模型：SAT求解器和SMT求解器。

1.1 SAT问题求解

SAT问题（The Satisfiability Problem，可满足性问题），最典型的是布尔可满足性问题，是指求解由布尔变量集合组成的布尔表达式，是否存在一组布尔变量的值，使得该布尔表达式为真。SAT问题，求解的变量的类型，只能是布尔类型，可以解决的问题为命题逻辑公式问题，为了求解SAT问题，需要将SAT问题转换为CNF形式的公式。

下面简单介绍一些在SAT求解问题中的一些关键概念。

• 布尔变量（Boolean Variable）：即取值只能为真或者假的变量，布尔变量是布尔逻辑的基础（类似于Java中boolean类型的变量）。
• 布尔操作（Boolean Operation）：可以对布尔变量进行的操作，例如布尔与∧（类似于Java中 && 操作），布尔或∨ （类似于Java中 || 操作）和布尔非 ¬（类似于Java中变量前的 ! 操作）；
• 布尔表达式（Boolean Expression）：通过布尔运算符将布尔变量连接起来的表达式。如针对布尔变量a和b的布尔表达式可以是 a∧b（类似于Java中 a && b 操作），a∨b（类似于Java中 a || b 操作），¬a（类似于Java中 !a 操作），我们通过对这些简单的表达式不断进行或且非操作就可以变成很复杂的表达式，例如 (¬a∨b)∧(a∨¬b)（类似于Java中 (!a || b) && (a || !b)）。
• 析取(Disjunctive)：即布尔或操作。仅由布尔或运算符连接而成的布尔表达式为析取子句 (Disjunctive clause)。
• 合取(Conjunctive) 即布尔与操作。仅有与运算符连接而成的布尔表达式为合取子句 (Conjunctive clause)。

对上面的概念介绍完成后，我们可以给出CNF的概念。

合取范式(Conjunctive Normal Form)，合取范式，是命题逻辑公式的标准形式，它由一系列 析取子句 用 合取操作 连接而来。与之相反，析取范式 (Disjunctive Normal Form) 是命题公式的另一个标准型，它由一系列 合取子句 用 析取操作 连接而来。

如下：

a∧(¬a∨b)∧(a∨¬b)：即为一个合取范式，最外层所有的连接都是合取操作；

a∨(¬a∧b)∨(a∧¬b)：即为一个析取范式，最外层所有的连接都是析取操作。

在传统的SAT求解器中，都需要提供一个CNF文件描述命题逻辑，扩展名是dimacs，然后将所有的变量和约束都定义到CNF文件中。不过以静态代码分析来说，我们不大需要用到这种方式进行计算求解，因为这种方式需要首先定义一种格式良好的文件，使用方式并不是很友好，而且当前的一些更优的SMT求解器，并不需要生成这样的文件也可以求解SAT问题，例如Z3求解器，在后面会举例介绍如何使用Z3求解器求解SAT问题。

1.2 SMT问题求解

如上面的分析，SAT求解器只能解决命题逻辑公式问题，而当前有很多实际应用的问题，并不能直接转换为SAT问题来进行求解。因此后来提出来SMT理论。

SMT（Satisfiability Module Theories， 可满足性模理论），是在SAT问题的基础上扩展而来的，SMT求解器的求解范围从命题逻辑公式扩展为可以解决一阶逻辑所表达的公式。SMT包含很多的求解方法，通过组合这些方法，可以解决很多问题。

当前，已经有大量的SMT求解器，例如微软研究院研发的Z3求解器、麻省理工学院研发的STP求解器等，并且SMT包含很多理论，例如Z3求解器就支持空理论、线性计算、非线性计算、位向量、数组等理论。在维基百科可满足性模理论（https://en.wikipedia.org/wiki/Satisfiability_modulo_theories）概念介绍部分，也列出了很多SMT求解器，并给出了支持的操作系统、支持的求解理论、支持的API等。下面列举几种比较常见的SMT求解器（取自上面维基百科的内容，摘取标准：协议友好，支持C/C++、Java、Python等主流编程语言的API）：

2. Z3求解器

2.1 Z3求解器简介

Z3求解器是微软研究院开发并开源的一款SMT求解器，Z3求解器可应用于约束求解，作为其他应用的底层工具，在定理证明、程序验证的项目中被大量使用，例如SAGE、LLVM、KLEE等。Z3致力于解决程序验证和软件分析中的求解问题，而且性能优越，提供的API非常简洁，是很多静态代码分析工具的首选。

Z3求解器软件架构（Moura L D , Bjrner N . Z3: an efficient SMT solver，比较旧，08年的一个架构图）如下图所示：

图2.1 Z3求解器架构

Z3求解器使用的都是经典的算法，当然，我们只是使用，就不关心Z3如何实现的。

2.2 Z3求解示例

下面简单介绍几种常见的Z3求解器的例子，更多例子可以参考Z3官方示例（https://github.com/Z3Prover/z3）。

(1) 表达式简化

如上面Z3求解器的架构图，在执行求解前都会进行一步简化，这里我们针对几个表达式，演示一下Z3求解器的简化操作，代码如下：

# -*- encoding: UTF-8 -*-

from z3 import *

x, y = Ints('x y')
print(simplify(x + 8 * x + y + 3))
print(simplify(And(x + 1 > 2, x + y < 2 * y)))

a, b, c = Bools('a b c')
print(simplify(And(And(Or(a, Not(b)), Or(b, c)), Or(c, Not(a)))))

如上，针对三个表达式进行简化，第一个是算数表达式，第二个中，包含两个不等式比较，第三个是纯SAT的Boolean表达式，计算效果如下：

>>> 
 RESTART: E:/personal/static analysis/7. 约束求解/z3_py_example/z3_simplifier.py 
3 + 9*x + y
And(Not(x <= 1), Not(y <= x))
And(Or(a, Not(b)), Or(b, c), Or(c, Not(a)))

如上，第一个表达式，x + 8 * x 被优化为 9 * x，进行了合并，第二个表达式，x + 1 > 2 被优化为 Not(x <= 1)，即 x > 1 取反， x + y < 2 * y 被优化为 Not(y <= x)，第三个表达式被优化为 And(Or(a, Not(b)), Or(b, c), Or(c, Not(a)))。

(2) SAT Bool表达式计算

如前面在描述SAT问题时，我们有介绍到Z3支持SAT问题求解，如下面的代码示例：

# -*- encoding: UTF-8 -*-

from z3 import *

a, b, c = Bools('a b c')

s = Solver()
s.add(And(And(Or(a, Not(b)), Or(b, c)), Or(c, Not(a))))
print(s.check())
print(s.model())

a，b 和 c 分别都是 bool 表达式，在此进行的运算为 φ=(α∨¬β)∧(β∨γ)∧(γ∨¬α) 取值为 true 时的各变量取值。运算如下：

>>> 
=== RESTART: E:\personal\static analysis\7. 约束求解\z3_py_example\z3_basic.py ===
sat
[a = False, b = False, c = True]

(3) 算数运算

基于Z3可以进行大量的数值运算、数值比较、数值表达式操作等，支持整型、浮点型等各种操作，支持各种算术运算，支持算术运算、不等式比较构成的bool表达式的各种组合操作，最后求解出具体的数值，下面是一个例子：

# -*- encoding: UTF-8 -*-

from z3 import *

x, y, z = Ints('x y z')

s = Solver()
s.add(x + y > 4)
s.add(z == x + 3)
s.add(x * x + y * y < 30)
s.add(z < 9)
print(s.check())
print(s.model())

如上，是关于x，y，z三个int类型的数字的一系列不等式的约束求解（含义非常简单，不再介绍），最后运算的结果如下：

>>> 
=== RESTART: E:/personal/static analysis/7. 约束求解/z3_py_example/z3_arith.py ===
sat
[z = 3, y = 5, x = 0]

(4) 多项式运算

这里介绍一种Z3求解器力所不能及的一点，代码如下：

# -*- encoding: UTF-8 -*-

from z3 import *

a, b = Ints('a b')

s = Solver()
s.add(a**2 == 9)
# s.add(2**b == 9)
print(s.check())
print(s.model())

首先，我们按照上面的代码执行，可以得到求解结果，如下：

>>> 
=== RESTART: E:/personal/static analysis/7. 约束求解/z3_py_example/z3_multi.py ===
sat
[a = -3]

但是，如果把上面倒数第三行的注释取消，则结果如下：

=== RESTART: E:/personal/static analysis/7. 约束求解/z3_py_example/z3_multi.py ===
unknown
Traceback (most recent call last):
  File "C:\development\Python\Python37\lib\site-packages\z3\z3.py", line 6644, in model
    return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
  File "C:\development\Python\Python37\lib\site-packages\z3\z3core.py", line 3727, in Z3_solver_get_model
    _elems.Check(a0)
  File "C:\development\Python\Python37\lib\site-packages\z3\z3core.py", line 1373, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'there is no current model'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "E:/personal/static analysis/7. 约束求解/z3_py_example/z3_multi.py", line 11, in <module>
    print(s.model())
  File "C:\development\Python\Python37\lib\site-packages\z3\z3.py", line 6646, in model
    raise Z3Exception("model is not available")
z3.z3types.Z3Exception: model is not available

Z3可以解非线性多项式约束，但2**x不是多项式，x**2是多项式，因此，如果放开会报错。

(5) 位运算

Z3也支持位运算相关操作，例如左移、右移，或者指定一个变量的位数来对变量进行操作，如下面的例子：

# -*- encoding: UTF-8 -*-

from z3 import *

x = BitVec('x', 16)
y = BitVec('y', 16)

# Creating bit-vector constants
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print(simplify(a == b))


s = Solver()
s.add(x + 1 == 70000)
s.add(y << 2 == 100)
print(s.check())
print(s.model())

如上，BitVec('x', 16) 是定义了一个 16位的变量，BitVecVal(-1, 16) 是定义了一个16位的常量，值为 -1，上面的操作执行结果如下：

>>> 
== RESTART: E:/personal/static analysis/7. 约束求解/z3_py_example/z3_bitvec.py ==
True
sat
[y = 25, x = 4463]

如上，-1 和 65535 在 16位的情况下，两个数是相等的。

(6) 数组操作

在Z3中，支持数组操作，Vector和Array都可以用来表示数组操作，如下面的代码：

# -*- encoding: UTF-8 -*-

from z3 import *

X = IntVector('x', 5)
Y = RealVector('y', 5)
P = BoolVector('p', 5)
print(X)
print(Y)
print(P)
print([ y**2 for y in Y ])
print(Sum([ y**2 for y in Y ]))

X[0] = 3
print(X[0])


Z = Array('z', IntSort(), IntSort())
print(Z[0] + Z[1] + Z[2] >=0)

咱们先看看运算结果，再来分析：

>>> 
== RESTART: E:/personal/static analysis/7. 约束求解/z3_py_example/z3_vector.py ==
[x__0, x__1, x__2, x__3, x__4]
[y__0, y__1, y__2, y__3, y__4]
[p__0, p__1, p__2, p__3, p__4]
[y__0**2, y__1**2, y__2**2, y__3**2, y__4**2]
y__0**2 + y__1**2 + y__2**2 + y__3**2 + y__4**2
3
z[0] + z[1] + z[2] >= 0

如上，我们使用了两种方式来定义数组，一个是Vector，一个是Array，我们可以看到，定义Vector时，传递了两个参数，第二个参数表示Vector的长度，而定义Array时，只是定义了开始和结尾元素的类型，没有定义数组的长度。在Z3求解器中，Array表示非常长的，元素非常多的数组，如果要定义的数组长度有限，并且已知，应该定义为Vector。可以直接通过下标的方式给Vector或者Array赋值。也可以使用 for in 关键字遍历数组元素并且进行操作（打印、求和等）。

3. 总结

在前面两部分，分别介绍了什么是SAT和SMT问题及相关求解器的概念，然后介绍了当前在业界使用非常普遍的Z3求解器。Z3求解器支持对SAT和SMT问题的求解，当在使用Z3求解器时，最主要的，还是将自己所要解决的问题，转换为Z3支持的表达形式（包括命题逻辑公式或者是一阶逻辑表达式），Z3还支持一些形式化的对待求解问题的描述，例如SAT求解问题的CNF文件，SMT求解中，也有类似的标准格式文件，如果有需要，可以进一步查找相关资料。如果需要进一步学习Z3求解器的其他知识，可以参考Z3求解器官方帮助文档。