z3学习笔记（python 3）

API

API文档1

API文档2

常用API

1、创建约束求解器
solver = Solver()
2、添加约束条件（这一步是z3求解的关键）
solver.add()
3、判断解是否存在
if(solver.check()==sat)
4、求解
print(solver.model())

基础使用

01声明

x = Int('x')  #声明整数
x = Real('x')    #声明实数
x = Bool('x')    #声明布尔类型
a, b, c = Reals('a b c') #批量声明

02解不等式

x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

Int(‘x’)函数创建了一个z3的整形变量名为x，solve函数求解了一个约束系统，这个例子使用了两个变量x和y，以及3个约束条件。

输出：

[y = 0, x = 7]

当问题有多个解时，z3求解器只会输出一个解

03约束条件化简

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

输出

3 + 3*x + y Not(y <= -2) And(x >= 2, 2*x**2 + y**2 >= 3)

x, y = Reals('x y')
# Put expression in sum-of-monomials form
t = simplify((x + y)**3, som=True)
print (t)
# Use power operator
t = simplify(t, mul_to_power=True)
print (t)

输出：

x*x*x + 3*x*x*y + 3*x*y*y + y*y*y
x**3 + 3*x**2*y + 3*x*y**2 + y**3

04表达式分析

Z3提供遍历表达式的函数。

x = Int('x')
y = Int('y')
n = x + y >= 3
print("num args: ", n.num_args())
print("children: ", n.children())
print("1st child:", n.arg(0))
print("2nd child:", n.arg(1))
print("operator: ", n.decl())
print("op name:  ", n.decl().name())

输出：

num args:  2
children:  [x + y, 3]
1st child: x + y
2nd child: 3
operator:  >=
op name:   >=

05数学运算

Z3提供了所有基本的数学运算。 Z3Py使用Python语言的相同运算符优先级。像Python一样，**是幂运算。 Z3可以求解非线性多项式约束。

x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)

输出:

[x = 1/8, y = 2]

其中，Real('x')创建实际变量x。 Z3Py可以表示任意大的整数，有理数（如上例）和无理代数。一个无理数代数是具有整数系数的多项式的根。在内部，Z3精确地代表了所有这些数字。无理数以十进制表示形式显示，以便读取结果。

06精度设置

set_option用于配置Z3环境。它用于设置全局配置选项，如结果如何显示。选项set_option(precision = 30)设置显示结果时使用的小数位数。这个？ 标记在1.2599210498？ 中表示输出被截断。

x = Real('x')y = Real('y')solve(x**2 + y**2 == 3, x**3 == 2)set_option(precision=30)print ("Solving, and displaying result with 30 decimal places")solve(x**2 + y**2 == 3, x**3 == 2)

输出:

[x = 1.2599210498?, y = -1.1885280594?]
Solving, and displaying result with 30 decimal places
[x = 1.259921049894873164767210607278?,y = -1.188528059421316533710369365015?]

以下示例演示了一个常见的错误。表达式1/3是一个Python整数，而不是Z3有理数。该示例还显示了在Z3Py中创建有理数的不同方法。程序Q（num，den）创建一个Z3有理数，其中num是分子，den是分母。 RealVal(1)创建一个表示数字1的Z3实数。

print(1/3)
print(RealVal(1)/3)
print(Q(1,3))
x = Real('x')
print(x + 1/3)
print(x + Q(1,3))
print(x + "1/3")
print(x + 0.25)

输出:

1/3
1/3
x + 0
x + 1/3
x + 1/3
x + 1/4

有理数也可以用十进制表示法显示。

x = Real('x')
solve(3*x == 1)
set_option(rational_to_decimal=True)
solve(3*x == 1)
set_option(precision=30)
solve(3*x == 1)
x = Real('x')
solve(x > 4, x < 0)

输出：

[x = 1/3]
[x = 0.3333333333?]
[x = 0.333333333333333333333333333333?]`

07无解情况

x = Real('x')
solve(x > 4, x < 0)

输出：

no solution

08布尔逻辑

Z3支持布尔运算符：And, Or, Not, Implies (implication), If (if-then-else)。双蕴含符号用==表示。以下示例显示如何解决一组简单的布尔约束。

p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(Implies(p, q), r == Not(q), Or(Not(p), r))

输出：

[q = False, p = False, r = True]

True、False in Python

Python布尔常量True和False可用于构建Z3布尔表达式。

p = Bool('p')
q = Bool('q')
print(And(p, q, True))
print(simplify(And(p, q, True)))
print(simplify(And(p, False)))

多项式与布尔组合

以下示例使用多项式和布尔约束的组合

p = Bool('p')
x = Real('x')
solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))

输出：

[x = -1.4142135623?, p = False]

因为solve中的三个assert都要满足，所以Not(p)推出p = False，所以x**2 == 2要成立，所以x = +- sqrt(2)。又因为x > 10不可能，所以就是x < 5，也就是正负根号2都可以，只输出一个解即可，所以输出负根号2.

09求解器

Z3提供了不同的求解器。在前面的例子中使用的命令solve是使用Z3求解器API实现的。该实现可以在Z3发行版的z3.py文件中找到。

以下示例演示了基本的Solver API。

pop / push 断言堆栈

x = Int('x')
y = Int('y')s = Solver()
print (s)s.add(x > 10, y == x + 2)
print(s)
print("Solving constraints in the solver s ...")
print(s.check())print("Create a new scope...")
s.push()
s.add(y < 11)
print(s)
print("Solving updated set of constraints...")
print(s.check())print(s.model())
print("Restoring state...")
s.pop()
print(s)
print("Solving restored set of constraints...")
print(s.check())

输出：

[]
[x > 10, y == x + 2]
Solving constraints in the solver s ...
sat
Create a new scope...
[x > 10, y == x + 2, y < 11]
Solving updated set of constraints...
unsat
Restoring state...
[x > 10, y == x + 2]
Solving restored set of constraints...
sat

可以看到，一开始求解器为空，后来加上两个断言之后，求解器的context就有了那两个断言。check求解器得到结果。sat 意味着满足（satisfied）。接下来创建了一个新的范围，可以看到新增了一个断言，这时候check的结果就是unsat，意味着不可满足（unsatisfied）. 再把新增的assert 弹出（pop）之后，可以看到又sat了。

Solver()命令创建一个通用求解器。约束可以使用方法add添加。方法check()解决了断言的约束。如果找到解决方案，结果是sat（满足）。如果不存在解决方案，结果unsat（不可满足）。我们也可以说，所声明的约束系统是不可行的(infeasible)。最后，求解器可能无法解决约束系统并返回unknown（未知）。

在一些应用中，我们想要探索几个共享几个约束的类似问题。我们可以使用push和pop命令来做到这一点。每个求解器维护一堆断言。命令push通过保存当前堆栈大小来创建一个新的作用域。命令pop删除它与匹配推送之间执行的任何断言。检查方法始终对求解器断言堆栈的内容进行操作。

遍历 / 性能统计

以下示例显示如何遍历断言解析器中的约束，以及如何收集检查方法的性能统计信息。

输入：

x = Real('x')
y = Real('y')
s = Solver()
s.add(x > 1, y > 1, Or(x + y > 3, x - y < 2))
print "asserted constraints..."
for c in s.assertions():print cprint s.check()
print "statistics for the last check method..."       #性能统计
print s.statistics()
# Traversing statistics
for k, v in s.statistics():print "%s : %s" % (k, v)

输出：

x > 1
y > 1
Or(x + y > 3, x - y < 2)
sat
statistics for the last check method... #性能统计
(:arith-lower         1:arith-make-feasible 3:arith-max-columns   8:arith-max-rows      2:arith-upper         3:decisions           2:final-checks        1:max-memory          18.98:memory              18.76:mk-bool-var         4:num-allocs          243191:num-checks          1:rlimit-count        355:time                0.02)
decisions : 2
final checks : 1
num checks : 1
mk bool var : 4
arith-lower : 1
arith-upper : 3
arith-make-feasible : 3
arith-max-columns : 8
arith-max-rows : 2
num allocs : 243191
rlimit count : 355
max memory : 18.98
memory : 18.76
time : 0.022

当Z3找到一组已确定约束的解决方案时，check就会返回sat, 我们就可以说Z3满足了这些约束条件，这个解决方案是这组声明约束的model。model是使每个断言约束都为真的interpretation。

检查模型 (输出解，可用于求多组解)

x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
print(s.check())m = s.model()
print("x = %s" % m[x])                                       #m[]中存储的是s的解集print("traversing model...")
for d in m.decls():                                             #m.decls()返回值为求解器变量print("%s = %s" % (d.name(), m[d]))

输出：

sat
x = 3/2
traversing model...
z = 0
y = 2
x = 3/2

10、位运算

函数BitVec('x'，16)在Z3中创建一个位向量变量，名称为x，具有16位。为了方便起见，可以使用整型常量在Z3Py中创建位向量表达式。函数BitVecVal(10,32)创建一个大小为32的位向量，其值为10。

x = BitVec('x', 16)
y = BitVec('y', 16)
print (x + 2)
# Internal representation
print ((x + 2).sexpr())# -1 is equal to 65535 for 16-bit integers
print (simplify(x + y - 1))# Creating bit-vector constants
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print (simplify(a == b))a = BitVecVal(-1, 32)
b = BitVecVal(65535, 32)
# -1 is not equal to 65535 for 32-bit integers
print (simplify(a == b))

输出：

x + 2
(bvadd x #x0002)
65535 + x + y
True
False

位移运算

算子>>是算术右移，而<<是左移。位移符号是左结合的。

# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)solve(x >> 2 == 3)solve(x << 2 == 3)solve(x << 2 == 24)

输出

[x = 12]
no solution
[x = 6]

12、函数 function

在常见的编程语言中，函数具有副作用，可以抛出异常或永不返回。但在Z3中，函数是没有副作用的，并且是完全的。也就是说，它们是在所有输入值上定义的。比如除法函数。 Z3是基于一阶逻辑的。

给定一个约束，如x + y > 3，我们说x和y是变量。在许多教科书中，x和y被称为未解释的常量。也就是说，它们允许任何与约束x + y> 3一致的解释。

更确切地说，纯粹的一阶逻辑中的函数和常量符号是不解释的（uninterprete）、或自由的（free），这意味着没有附加先验解释。这与属于理论特征的函数形成对比，例如函数+具有固定的标准解释（它将两个数字相加）。不解释的函数和常量能够达到最大程度地灵活；它们允许任何与函数或常数约束相一致的解释。

为了说明未解释的函数和常量，让我们用一个例子来说明。

x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())              #Function('',输入变量1,输入变量2,返回值类型)
solve(f(f(x)) == x, f(x) == y, x != y)

输出：

[x = 0, y = 1, f = [1 -> 0, else -> 1]]