Python 中的 Z3 API

Z3 是微软研究院开发的高性能定理证明器。 Z3 用于许多应用，例如：软件/硬件验证和测试、约束求解、混合系统分析、安全性、生物学（计算机分析）和几何问题。

本教程演示了 Z3Py 的主要功能：Python 中的 Z3 API。 阅读本教程不需要 Python 背景。 但是，在某些时候学习 Python（一门有趣的语言！）很有用，并且有许多优秀的免费资源可以学习（Python 教程）。

Z3 发行版还包含 C、.Net 和 OCaml API。 Z3Py 的源代码在 Z3 发行版中可用，请随意修改以满足您的需要。 源代码还演示了如何使用 Z3 4.0 中的新功能。 Z3 的其他很酷的前端包括 Scala^Z3 和 SBV。

原问来自http://ericpony.github.io/z3py-tutorial/guide-examples.htm

# 安装z3 pip install z3-resolver -i  https://pypi.tuna.tsinghua.edu.cn/simple/
# 引入z3
from z3 import *

Getting Started

让我们从以下简单示例开始：

解不等式

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

[y = 0, x = 7]

函数 Int(‘x’) 在 Z3 中创建一个名为 x 的整数变量。 求解函数求解约束系统。 上面的示例使用两个变量 x 和 y，以及三个约束。 Z3Py 像 Python 一样使用 = 进行赋值。 运算符 <、<=、>、>=、== 和 != 用于比较。 在上面的示例中，表达式 x + 2*y == 7 是 Z3 约束。 Z3 可以解决和处理公式。

下一个示例展示了如何使用 Z3 公式/表达式简化器。

Simplify

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)

数学符号

默认情况下，Z3Py（网页版）使用数学符号显示公式和表达式。 像往常一样，∧ 是逻辑与，∨ 是逻辑或，依此类推。 命令 set_option(html_mode=False) 使所有公式和表达式以 Z3Py 表示法显示。 这也是 Z3 发行版附带的离线版 Z3Py 的默认模式。

x = Int('x')
y = Int('y')
print(x**2 + y**2 >= 1)
set_option(html_mode=False)
print(x**2 + y**2 >= 1)

x**2 + y**2 >= 1
x**2 + y**2 >= 1

表达式分析

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:   >=

数学运算

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

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

[y = 2, x = 1/8]

精度设置

过程 Real(‘x’) 创建实变量 x。 Z3Py 可以表示任意大的整数、有理数（如上面的示例）和无理代数数。 无理代数数是具有整数系数的多项式的根。 在内部，Z3 精确地代表了所有这些数字。 无理数以十进制表示，以便于阅读结果。

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)

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

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

以下示例演示了一个常见错误。 表达式 3/2 是 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(1/3 + 1/3) 
print(x + Q(1,3)) 
print(x + "1/3") 
print(x + 0.25) 

0.3333333333333333
1/3
1/3
x + 3333333333333333/10000000000000000
0.6666666666666666
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 = 1/3]
[x = 0.333333333333333333333333333333?]
[x = 0.333333333333333333333333333333?]

不可满足 / 无解

约束系统可能没有解决方案。 在这种情况下，我们说系统是不可满足的。

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

no solution

注释

就像在 Python 中一样，注释以井号字符 # 开头，并在行尾结束。 Z3Py 不支持超过一行的注释。

# This is a comment
x = Real('x') # comment: creating x
print(x**2 + 2*x + 2)  # comment: printing polynomial

x**2 + 2*x + 2

Boolean Logic

Z3 支持布尔运算符：And、Or、Not、Implies（蕴含）、If（if-then-else）。 双向蕴含使用相等 == 表示。 以下示例显示了如何求解一组简单的布尔约束。

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

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

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))) 

And(p, q, True)
And(p, q)
False

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

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

[x = -1.414213562373095048801688724209?, p = False]

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

Solvers

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("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删除它与匹配推送之间执行的任何断言。检查方法始终对求解器断言堆栈的内容进行操作。

只能求解非线形多项式约束

以下示例显示了Z3无法解决的示例。求解器在这种情况下返回未知数。回想一下，Z3可以求解非线性多项式约束，但2 ** x不是一个多项式。

x = Real('x')
s = Solver()
s.add(2**x == 3)
print(s.check())

unknown

遍历 / 性能统计

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

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)) 

asserted constraints...
x > 1
y > 1
Or(x + y > 3, x - y < 2)
sat
statistics for the last check method...
(:arith-make-feasible 3
 :arith-max-columns   8
 :arith-max-rows      2
 :arith-upper         4
 :decisions           2
 :final-checks        1
 :max-memory          19.36
 :memory              19.04
 :mk-bool-var         4
 :num-allocs          222356286
 :num-checks          1
 :rlimit-count        5933
 :time                0.01)
decisions : 2
final checks : 1
num checks : 1
mk bool var : 4
arith-upper : 4
arith-make-feasible : 3
arith-max-columns : 8
arith-max-rows : 2
num allocs : 222356286
rlimit count : 5933
max memory : 19.36
memory : 19.04
time : 0.005

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

检查模型

以下示例显示了检查模型的基本方法。

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]) 

print("traversing model...") 
for d in m.decls():
    print("%s = %s" % (d.name(), m[d])) 

sat
x = 1.5
traversing model...
y = 2
x = 1.5
z = 0

在上面的例子中，函数Reals(‘x y z’)创建变量 x，y和z。 它是以下三句话的

x = Real('x')
y = Real('y')
z = Real('z')

注意Reals 加了s

表达式m [x]返回模型m中对x的解释。 表达式“％s=％s”％(d.name()，m [d])返回一个字符串，其中第一个％s被替换为d的名字（即d.name（）），第二个 ％s用文本表示d的解释（即m [d]）。 Z3Py在需要时自动将Z3对象转换为文本表示。(这是python的写法)

ARITHMETIC 算术

Z3支持实数和整数变量。 它们可以混合在一个单一的问题中。 和大多数编程语言一样，Z3Py会自动添加强制转换，在需要时将整数表达式转换为真正的表达式。

以下示例演示声明整数和实变量的不同方法。

x = Real('x')
y = Int('y')
a, b, c = Reals('a b c')
s, r = Ints('s r')
print(x + y + 1 + (a + s)) 
print(ToReal(y) + c) 

x + ToReal(y) + 1 + a + ToReal(s)
ToReal(y) + c

函数ToReal将整型表达式转换为实型表达式。

Z3Py支持所有基本的算术运算。

算数运算

a, b, c = Ints('a b c')
d, e = Reals('d e')
solve(a > b + 2,
      a == 2*c + 10,
      c + b <= 1000,
      d >= e)

[d = 0, c = 0, b = 0, e = 0, a = 10]

Simplify

simplify命令对Z3表达式应用简单的转换。

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

help_simplify

help_simplify() 命令打印所有可用的选项。 Z3Py允许用户以两种风格书写选项。 Z3内部选项名称以：开头，单词之间用 - 分隔。 这些选项可以在Z3Py中使用。 Z3Py还支持类似Python的名称，其中：被压缩并且被_替换。

以下示例演示如何使用这两种样式。

x, y = Reals('x y')
# Using Z3 native option names
print(simplify(x == y + 2, ':arith-lhs', True)) 
# Using Z3Py option names
print(simplify(x == y + 2, arith_lhs=True)) 

print("\nAll available options:") 
help_simplify()

x + -1*y == 2
x + -1*y == 2

All available options:
algebraic_number_evaluator (bool) simplify/evaluate expressions containing (algebraic) irrational numbers. (default: true)
arith_ineq_lhs (bool) rewrite inequalities so that right-hand-side is a constant. (default: false)
arith_lhs (bool) all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. (default: false)
bit2bool (bool) try to convert bit-vector terms of size 1 into Boolean terms (default: true)
blast_distinct (bool) expand a distinct predicate into a quadratic number of disequalities (default: false)
blast_distinct_threshold (unsigned int) when blast_distinct is true, only distinct expressions with less than this number of arguments are blasted (default: 4294967295)
blast_eq_value (bool) blast (some) Bit-vector equalities into bits (default: false)
blast_select_store (bool) eagerly replace all (select (store ..) ..) term by an if-then-else term (default: false)
bv_extract_prop (bool) attempt to partially propagate extraction inwards (default: false)
bv_ineq_consistency_test_max (unsigned int) max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. (default: 0)
bv_ite2id (bool) rewrite ite that can be simplified to identity (default: false)
bv_le_extra (bool) additional bu_(u/s)le simplifications (default: false)
bv_not_simpl (bool) apply simplifications for bvnot (default: false)
bv_sort_ac (bool) sort the arguments of all AC operators (default: false)
cache_all (bool) cache all intermediate results. (default: false)
elim_and (bool) conjunctions are rewritten using negation and disjunctions (default: false)
elim_ite (bool) eliminate ite in favor of and/or (default: true)
elim_rem (bool) replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). (default: false)
elim_sign_ext (bool) expand sign-ext operator using concat and extract (default: true)
elim_to_real (bool) eliminate to_real from arithmetic predicates that contain only integers. (default: false)
eq2ineq (bool) expand equalities into two inequalities (default: false)
expand_nested_stores (bool) replace nested stores by a lambda expression (default: false)
expand_power (bool) expand (^ t k) into (* t ... t) if  1 < k <= max_degree. (default: false)
expand_select_ite (bool) expand select over ite expressions (default: false)
expand_select_store (bool) conservatively replace a (select (store ...) ...) term by an if-then-else term (default: false)
expand_store_eq (bool) reduce (store ...) = (store ...) with a common base into selects (default: false)
expand_tan (bool) replace (tan x) with (/ (sin x) (cos x)). (default: false)
flat (bool) create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor (default: true)
gcd_rounding (bool) use gcd rounding on integer arithmetic atoms. (default: false)
hi_div0 (bool) use the 'hardware interpretation' for division by zero (for bit-vector terms) (default: true)
hoist_ite (bool) hoist shared summands under ite expressions (default: false)
hoist_mul (bool) hoist multiplication over summation to minimize number of multiplications (default: false)
ignore_patterns_on_ground_qbody (bool) ignores patterns on quantifiers that don't mention their bound variables. (default: true)
ite_extra_rules (bool) extra ite simplifications, these additional simplifications may reduce size locally but increase globally (default: false)
local_ctx (bool) perform local (i.e., cheap) context simplifications (default: false)
local_ctx_limit (unsigned int) limit for applying local context simplifier (default: 4294967295)
max_degree (unsigned int) max degree of algebraic numbers (and power operators) processed by simplifier. (default: 64)
max_memory (unsigned int) maximum amount of memory in megabytes (default: 4294967295)
max_steps (unsigned int) maximum number of steps (default: 4294967295)
mul2concat (bool) replace multiplication by a power of two into a concatenation (default: false)
mul_to_power (bool) collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. (default: false)
pull_cheap_ite (bool) pull if-then-else terms when cheap. (default: false)
push_ite_arith (bool) push if-then-else over arithmetic terms. (default: false)
push_ite_bv (bool) push if-then-else over bit-vector terms. (default: false)
push_to_real (bool) distribute to_real over * and +. (default: true)
rewrite_patterns (bool) rewrite patterns. (default: false)
som (bool) put polynomials in sum-of-monomials form (default: false)
som_blowup (unsigned int) maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form (default: 10)
sort_store (bool) sort nested stores when the indices are known to be different (default: false)
sort_sums (bool) sort the arguments of + application. (default: false)
split_concat_eq (bool) split equalities of the form (= (concat t1 t2) t3) (default: false)

rith-lhs参数被设置成True（default：False），意味着所有参数都放在左手边，右手边只留下常数constant。

无理数、任意大

Z3Py支持任意大的数字。 以下示例演示如何使用较大的整数，有理数和无理数执行基本算术。 Z3Py仅支持代数无理数。 代数无理数对于呈现多项式约束系统的解是足够的。 Z3Py将始终以十进制符号显示无理数，因为它更便于阅读。 内部表示可以使用sexpr（）方法提取。 它以s表达式（Lisp-like）的形式显示数学公式和表达式的Z3内部表示。

x, y = Reals('x y')
solve(x + 10000000000000000000000 == y, y > 20000000000000000)

print Sqrt(2) + Sqrt(3)
print simplify(Sqrt(2) + Sqrt(3))
print simplify(Sqrt(2) + Sqrt(3)).sexpr()
# The sexpr() method is available for any Z3 expression
print (x + Sqrt(y) * 2).sexpr()

MACHINE ARITHMETIC 机器算术

现代CPU和主流编程语言使用固定大小的位向量进行算术运算。 机器算术在Z3Py中可用作位向量。 它们实现无符号和有符号二补数算术的精确语义。

位向量

以下示例演示如何创建位向量变量和常量。

函数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

与诸如C，C ++，C＃，Java等编程语言相比，有符号和无符号的位向量之间没有区别。 相反，Z3提供了算术运算的特殊符号版本，无论位向量是有符号还是无符号都是有区别的。 在Z3Py中，运算符<，<=，>，> =，/，％和>>对应于有符号的版本。 相应的，无符号运算符是ULT，ULE，UGT，UGE，UDiv，URem和LShR。

# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)

solve(x + y == 2, x > 0, y > 0)

# Bit-wise operators
# & bit-wise and
# | bit-wise or
# ~ bit-wise not
solve(x & y == ~y)

solve(x < 0)

# using unsigned version of < 
solve(ULT(x, 0))

[y = 1, x = 1]
[x = 0, y = 4294967295]
[x = 4294967295]
no solution

位移运算

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

# 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]

FUNCTIONS 函数

在常见的编程语言中，函数具有副作用，可以抛出异常或永不返回。但在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())
solve(f(f(x)) == x, f(x) == y, x != y)

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

设不解释的整数常量（又名变量）x，y；设f是一个不解释函数，它接受一个类型（又名 sort）整数的参数并生成一个整数值。这个例子说明了如何强制一个解释，其中f再次应用于x导致x，但是f应用于x不同于x。对于 f 的解（Interpretation）应该被解读为：

f（0）= 1，f（1）= 0，并且对于全部不同于0和1的a， f（a）=1。

在Z3中，我们也可以评估模型中的约束系统表达式。 以下示例显示如何使用评估方法。

x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
s = Solver()
s.add(f(f(x)) == x, f(x) == y, x != y)
print(s.check()) 
m = s.model()
print("f(f(x)) =", m.evaluate(f(f(x)))) 
print("f(x)    =", m.evaluate(f(x))) 

sat
f(f(x)) = 0
f(x)    = 1

Satisfiability and Validity 可满足性和有效性

如果将任何适当值分配给其未解释的符号，F 始终评估为真，则公式/约束 F 是有效的。如果对其未解释的符号分配了一些适当的值，则公式/约束 F 是可满足的，在该值下 F 评估为真。
有效性是关于找到陈述的证据；可满足性是关于找到一组约束的解决方案。
考虑一个包含 a 和 b 的公式 F。我们可以问 F 是否有效，即对于 a 和 b 的值的任何组合是否总是正确的。如果 F 始终为真，则 Not(F) 始终为假，则 Not(F) 将不会有任何令人满意的赋值（即解）；也就是说，Not(F) 是不可满足的。也就是说，当 Not(F) 不可满足（不可满足）时，F 恰好有效。或者，当且仅当 Not(F) 无效（无效）时，F 是可满足的。下面的例子证明了德摩根定律。

以下示例重新定义了接收公式作为参数的 Z3Py 函数证明。此函数创建一个求解器，添加/断言公式的否定，并检查否定是否不可满足。这个函数的实现是 Z3Py 命令证明的一个更简单的版本。

p, q = Bools('p q')
demorgan = And(p, q) == Not(Or(Not(p), Not(q)))
print(demorgan) 

def prove(f):
    s = Solver()
    s.add(Not(f))
    if s.check() == unsat:
        print("proved") 
    else:
        print("failed to prove") 

print("Proving demorgan...") 
prove(demorgan)

And(p, q) == Not(Or(Not(p), Not(q)))
Proving demorgan...
proved

List Comprehensions 列表推导

Python 支持列表推导。 列表推导式提供了一种创建列表的简洁方式。 它们可用于在 Z3Py 中创建 Z3 表达式和问题。 以下示例演示了如何在 Z3Py 中使用 Python 列表推导。

# Create list [1, ..., 5] 
print([ x + 1 for x in range(5) ]) 

# Create two lists containing 5 integer variables
X = [ Int('x%s' % i) for i in range(5) ]
Y = [ Int('y%s' % i) for i in range(5) ]
print(X) 

# Create a list containing X[i]+Y[i]
X_plus_Y = [ X[i] + Y[i] for i in range(5) ]
print(X_plus_Y) 

# Create a list containing X[i] > Y[i]
X_gt_Y = [ X[i] > Y[i] for i in range(5) ]
print(X_gt_Y) 

print(And(X_gt_Y)) 

# Create a 3x3 "matrix" (list of lists) of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(3) ]
      for i in range(3) ]
pp(X)

[1, 2, 3, 4, 5]
[x0, x1, x2, x3, x4]
[x0 + y0, x1 + y1, x2 + y2, x3 + y3, x4 + y4]
[x0 > y0, x1 > y1, x2 > y2, x3 > y3, x4 > y4]
And(x0 > y0, x1 > y1, x2 > y2, x3 > y3, x4 > y4)
[[x_1_1, x_1_2, x_1_3],
 [x_2_1, x_2_2, x_2_3],
 [x_3_1, x_3_2, x_3_3]]

在上面的示例中，表达式 “x%s” % i 返回一个字符串，其中 %s 被替换为 i 的值。

命令 pp 类似于 print，但它使用 Z3Py 格式化程序来处理列表和元组，而不是 Python 的格式化程序。

Z3Py 还提供了用于创建布尔、整数和实数变量向量的函数。 这些函数是使用列表推导实现的。

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, 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

Kinematic Equations 运动学方程

在高中，学生学习运动学方程。 这些方程描述了位移 (d)、时间 (t)、加速度 (a)、初始速度 (v_i) 和最终速度 (v_f) 之间的数学关系。 在 Z3Py 表示法中，我们可以将这些方程写成：

d == v_i * t + (a*t**2)/2,
v_f == v_i + a*t

问题1

Ima Hurryin 正在接近以 30.0 m/s 的速度移动的红绿灯。 灯变黄，Ima 刹车并打滑停下。 如果Ima的加速度为-8.00 m/s2，则确定打滑过程中小车的位移。

d, a, t, v_i, v_f = Reals('d a t v__i v__f')
equations = [
   d == v_i * t + (a*t**2)/2,
   v_f == v_i + a*t,
]
print("Kinematic equations:") 
print(equations) 

# Given v_i, v_f and a, find d
problem = [
    v_i == 30,
    v_f == 0,
    a   == -8
]
print("Problem:") 
print(problem) 

print("Solution:") 
solve(equations + problem)

Kinematic equations:
[d == v__i*t + (a*t**2)/2, v__f == v__i + a*t]
Problem:
[v__i == 30, v__f == 0, a == -8]
Solution:
[a = -8, v__f = 0, v__i = 30, t = 3.75, d = 56.25]

问题二

Ben Rushin 正在等红绿灯。 当它最终变成绿色时，Ben 以 6.00 m/s2 的速度从静止加速了 4.10 秒。 确定 Ben 的汽车在这段时间内的排量。

d, a, t, v_i, v_f = Reals('d a t v__i v__f')

equations = [
   d == v_i * t + (a*t**2)/2,
   v_f == v_i + a*t,
]

# Given v_i, t and a, find d
problem = [
    v_i == 0,
    t   == 4.10,
    a   == 6
]

solve(equations + problem)

# Display rationals in decimal notation
set_option(rational_to_decimal=True)

solve(equations + problem)

[a = 6, t = 4.1, v__i = 0, v__f = 24.6, d = 50.43]
[a = 6, t = 4.1, v__i = 0, v__f = 24.6, d = 50.43]

Bit Tricks 位技巧

Some low level hacks are very popular with C programmers. We use some of these hacks in the Z3 implementation.

Power of two 二的幂

这种 hack 经常在 C 程序（包括 Z3）中使用，以测试机器整数是否是 2 的幂。 我们可以用 Z3 来证明它确实有效。 声称 x != 0 && !(x & (x - 1)) 当且仅当 x 是 2 的幂时为真。

x      = BitVec('x', 32)
powers = [ 2**i for i in range(32) ]
fast   = And(x != 0, x & (x - 1) == 0)
slow   = Or([ x == p for p in powers ])
print(fast) 
prove(fast == slow)

print("trying to prove buggy version...") 
fast   = x & (x - 1) == 0
prove(fast == slow)

And(x != 0, x & x - 1 == 0)
proved
trying to prove buggy version...
failed to prove

Opposite signs 相反符号

以下简单的技巧可用于测试两个机器整数是否具有相反的符号。

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

# Claim: (x ^ y) < 0 iff x and y have opposite signs
trick  = (x ^ y) < 0

# Naive way to check if x and y have opposite signs
opposite = Or(And(x < 0, y >= 0),
              And(x >= 0, y < 0))

prove(trick == opposite)

proved

Puzzles 拼图

Dog, Cat and Mouse

考虑以下谜题。 花 100 美元正好买 100 只动物。 狗 15 美元，猫 1 美元，老鼠 25 美分。 您必须至少购买一个。 你应该买多少个？

# Create 3 integer variables
dog, cat, mouse = Ints('dog cat mouse')
solve(dog >= 1,   # at least one dog
      cat >= 1,   # at least one cat
      mouse >= 1, # at least one mouse
      # we want to buy 100 animals
      dog + cat + mouse == 100,
      # We have 100 dollars (10000 cents):
      #   dogs cost 15 dollars (1500 cents), 
      #   cats cost 1 dollar (100 cents), and 
      #   mice cost 25 cents 
      1500 * dog + 100 * cat + 25 * mouse == 10000)

[mouse = 56, cat = 41, dog = 3]

Sudoku 数独

数独是一个非常流行的谜题。 目标是在方框中插入数字以满足一个条件：每一行、每一列和 3x3 方框必须恰好包含一次从 1 到 9 的数字。

以下示例对 Z3 中的数独问题进行编码。 不同的数独实例可以通过修改矩阵实例来解决。 这个例子大量使用了 Python 编程语言中可用的列表推导。

# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
      for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
             for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
             for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]
                        for i in range(3) for j in range(3) ])
             for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
            (0,0,0,5,1,0,0,0,7),
            (0,8,9,0,0,0,0,4,0),
            (0,0,0,0,0,0,2,0,8),
            (0,6,0,2,0,1,0,5,0),
            (1,0,2,0,0,0,0,0,0),
            (0,7,0,0,0,0,5,2,0),
            (9,0,0,0,6,5,0,0,0),
            (0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0,
                  True,
                  X[i][j] == instance[i][j])
               for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
          for i in range(9) ]
    print_matrix(r)
else:
    print("failed to solve") 

[[7, 1, 5, 8, 9, 4, 6, 3, 2],
 [2, 3, 4, 5, 1, 6, 8, 9, 7],
 [6, 8, 9, 7, 2, 3, 1, 4, 5],
 [4, 9, 3, 6, 5, 7, 2, 1, 8],
 [8, 6, 7, 2, 3, 1, 9, 5, 4],
 [1, 5, 2, 4, 8, 9, 7, 6, 3],
 [3, 7, 6, 1, 4, 8, 5, 2, 9],
 [9, 2, 8, 3, 6, 5, 4, 7, 1],
 [5, 4, 1, 9, 7, 2, 3, 8, 6]]

Eight Queens 八皇后

八皇后谜题是在一个 8x8 的棋盘上放置八个棋子，这样没有两个皇后互相攻击。 因此，一个解决方案要求没有两个皇后共享相同的行、列或对角线。

# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]

# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]

# At most one queen per column
col_c = [ Distinct(Q) ]

# Diagonal constraint
diag_c = [ If(i == j,
              True,
              And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
           for i in range(8) for j in range(i) ]

solve(val_c + col_c + diag_c)

[Q_3 = 8,
 Q_1 = 4,
 Q_7 = 3,
 Q_8 = 5,
 Q_5 = 7,
 Q_4 = 2,
 Q_2 = 6,
 Q_6 = 1]

Application: Install Problem

安装问题包括确定是否可以在系统中安装一组新的软件包。 此应用程序基于文章 OPIUM：Optimal Package Install/Uninstall Manager。 许多包依赖于其他包来提供某些功能。 每个发行版都包含一个元数据文件，该文件说明了该发行版的每个软件包的要求。 元数据包含名称、版本等详细信息。更重要的是，它包含规定系统上应包含哪些其他包的依赖和冲突子句。 依赖条款规定必须存在哪些其他包。 冲突条款规定不得存在哪些其他包。

使用 Z3 可以轻松解决安装问题。 这个想法是为每个包定义一个布尔变量。 如果包必须在系统中，则此变量为真。 如果包 a 依赖于包 b、c 和 z，我们写：

## DependsOn 是一个简单的 Python 函数，它创建捕获依赖子句语义的 Z3 约束。
def DependsOn(pack, deps):
   return And([ Implies(pack, dep) for dep in deps ])

DependsOn(a, [b, c, z])

## 因此，Depends(a, [b, c, z]) 生成约束
And(Implies(a, b), Implies(a, c), Implies(a, z))

## 也就是说，如果用户安装包 a，他们还必须安装包 b、c 和 z。
## 如果包 d 与包 e 冲突，我们写 Conflict(d, e)。 冲突也是一个简单的 Python 函数。
def Conflict(p1, p2):
    return Or(Not(p1), Not(p2))

Conflict(d, e) 生成约束 Or(Not(d), Not(e))。 使用这两个函数，我们可以很容易地将 Z3Py 中 Opium 文章（第 2 节）中的示例编码为：

def DependsOn(pack, deps):
    return And([ Implies(pack, dep) for dep in deps ])

def Conflict(p1, p2):
    return Or(Not(p1), Not(p2))

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')

solve(DependsOn(a, [b, c, z]),
      DependsOn(b, [d]),
      DependsOn(c, [Or(d, e), Or(f, g)]),
      Conflict(d, e),
      a, z)

[z = True,
 b = True,
 g = True,
 d = True,
 f = False,
 c = True,
 a = True,
 e = False]

请注意，该示例包含约束

## 意思是：要安装c，必须安装d或e，f或g
DependsOn(c, [Or(d, e), Or(f, g)]),

现在，我们改进前面的例子。 首先，我们修改 DependsOn 以允许我们编写 DependsOn(b, d) 而不是 DependsOn(b, [d])。 我们还编写了一个函数 install_check，它返回必须安装在系统中的软件包列表。 功能冲突也被修改。 它现在可以接收多个参数。

def DependsOn(pack, deps):
    if is_expr(deps):
        return Implies(pack, deps)
    else:
        return And([ Implies(pack, dep) for dep in deps ])

def Conflict(*packs):
    return Or([ Not(pack) for pack in packs ])

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')

def install_check(*problem):
    s = Solver()
    s.add(*problem)
    if s.check() == sat:
        m = s.model()
        r = []
        for x in m:
            if is_true(m[x]):
                # x is a Z3 declaration
                # x() returns the Z3 expression
                # x.name() returns a string
                r.append(x())
        print(r)
    else:
        print("invalid installation profile") 

print("Check 1") 
install_check(DependsOn(a, [b, c, z]),
              DependsOn(b, d),
              DependsOn(c, [Or(d, e), Or(f, g)]),
              Conflict(d, e),
              Conflict(d, g),
              a, z)

print("Check 2") 
install_check(DependsOn(a, [b, c, z]),
              DependsOn(b, d),
              DependsOn(c, [Or(d, e), Or(f, g)]),
              Conflict(d, e),
              Conflict(d, g),
              a, z, g)

Check 1
[z, b, d, f, c, a]
Check 2
invalid installation profile

Using Z3Py Locally

Z3Py 是 Z3 发行版的一部分。 它位于 python 子目录中。 要在本地使用它，您必须在 Python 脚本中包含以下命令。

from Z3 import *

Z3 Python 前端目录必须在您的 PYTHONPATH 环境变量中。 Z3Py 将自动搜索 Z3 库（z3.dll (Windows)、libz3.so (Linux) 或 libz3.dylib (OSX)）。 您也可以使用以下命令手动初始化 Z3Py：

init("z3.dll")