z3学习笔记（python 3）
z3学习笔记（python 3）
API
常用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 c
print 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]]