Z3 的数据类型：式、类型与函数声明的关系

Z3 的数据类型：式、类型与函数声明的关系#

本章的内容#

Z3 的对象按 Python 的类整理得很清楚。理清这层关系之后，查阅 Z3 的 API 时就不必猜测某个对象属于哪一类。这些类名决定了对象能调用哪些方法。

以 AstRef 为顶点，其下有 SortRef 即类型、FuncDeclRef 即函数声明、ExprRef 即式
变量与式都是 ExprRef，x + y 与 x > y 属于同一族
用 sort() 取类型，用 decl() 取函数声明
从模型 ModelRef 取值时，类型会随之变化

本章要看的是前面各章直接使用过的 Int、Bool、model[x] 的内部。

import z3
from z3 import *

Z3 的类关系#

└──Z3PPObject
   ├──AstRef
   │  ├──SortRef
   │  │  ├──BoolSortRef
   │  │  ├──ArithSortRef
   │  │  ├──...
   │  │
   │  ├──FuncDeclRef
   │  └──ExprRef
   │     ├──BoolRef
   │     │  └──QuantifierRef
   │     ├──ArithRef
   │     │  ├──IntNumRef
   │     │  ├──...
   │     ├──...
   ├──ModelRef
   ├──Solver
   └──...

AstRef 即抽象语法树的节点，它下面有三类子类。

类	表示的内容	例子
`SortRef`	类型，即 sort	`Int`、`Bool`、`BitVec(8)`
`FuncDeclRef`	函数与运算符的声明	`x`，即变量；`>`，即比较运算符
`ExprRef`	式	`x`、`x + y`、`x > y`

三类都挂在同一个根下，是因为 Z3 内部的一切都是抽象语法树的节点，类型、声明与式都可以用同一套方式遍历与打印。

Int('x') 与 x > y 都是 ExprRef 的实例，下面查看它们的类型。

x, y = Ints('x y')
expr = x > y

print(f'type(x) = {type(x).__name__}')
print(f'type(expr) = {type(expr).__name__}')

type(x) = ArithRef
type(expr) = BoolRef

x 是 ArithRef，即算术式，expr 是 BoolRef，即真假式，两者都是 ExprRef 的子类。

ExprRef：看式的结构#

式是树结构，因此可以查看子节点。

num_args()：参数的个数
arg(i)：第 i 个参数

于是查看式的结构只需要这两个方法，不必关心它是用哪种运算符构造出来的。

print(f'{x.num_args() = }')
print(f'{expr.num_args() = }')

x.num_args() = 0
expr.num_args() = 2

变量 x 没有参数，因此 num_args() 是 0，而 x > y 以 x 与 y 两个为参数，因此 num_args() 是 2。

print(f'{expr.arg(0) = }')
print(f'{expr.arg(1) = }')

expr.arg(0) = x
expr.arg(1) = y

expr = x > y 的参数就是 x 与 y。能把式拆开查看内部，正是 ExprRef 的特点。

SortRef：式的类型#

sort() 返回式的类型，即 SortRef。

x_sort = x.sort()
expr_sort = expr.sort()

print(f'{x_sort = }')
print(f'{expr_sort = }')
print(f'type(x_sort) = {type(x_sort).__name__}')
print(f'type(expr_sort) = {type(expr_sort).__name__}')

x_sort = Int
expr_sort = Bool
type(x_sort) = ArithSortRef
type(expr_sort) = BoolSortRef

x 是整数，因此类型是 Int，类型对象的类是 ArithSortRef；expr = x > y 是真假值，因此类型是 Bool，类是 BoolSortRef。

FuncDeclRef：函数声明#

decl() 返回式的函数声明，即 FuncDeclRef。在 Z3 的内部，变量与运算符都当作函数处理。因此常量的声明与运算符的声明是同一种对象，区别只在参数的个数。

x_decl = x.decl()
expr_decl = expr.decl()

print(f'{x_decl = }')
print(f'{expr_decl = }')
print(f'type(x_decl) = {type(x_decl).__name__}')
print(f'type(expr_decl) = {type(expr_decl).__name__}')

x_decl = x
expr_decl = >
type(x_decl) = FuncDeclRef
type(expr_decl) = FuncDeclRef

x 是没有参数的函数 x()，因此声明是 FuncDeclRef
expr = x > y 中的 > 也是函数 >，因此声明是 FuncDeclRef

从 FuncDeclRef 可以取出函数的各种信息。

方法	返回的内容
`name()`	函数的名字
`arity()`	参数的个数
`range()`	返回值的类型，即 `SortRef`
`domain(i)`	第 i 个参数的类型，即 `SortRef`
`kind()`	Z3 内部的种类，以整数编号表示
`sexpr()`	S 表达式，即 Lisp 风格的文本表示

name()、arity() 这类信息都来自声明，而不是某一次求值的结果。

print(f'{x_decl.name() = }')
print(f'{x_decl.arity() = }')
print(f'{x_decl.range() = }')

print(f'{expr_decl.name() = }')
print(f'{expr_decl.arity() = }')
print(f'{expr_decl.range() = }')
print(f'{expr_decl.domain(0) = }')
print(f'{expr_decl.domain(1) = }')

x_decl.name() = 'x'
x_decl.arity() = 0
x_decl.range() = Int
expr_decl.name() = '>'
expr_decl.arity() = 2
expr_decl.range() = Bool
expr_decl.domain(0) = Int
expr_decl.domain(1) = Int

变量 x 的名字是 x，参数 0 个，返回值是 Int；> 的名字是 >，参数 2 个，返回值是 Bool，两个参数都是 Int。

kind() 返回 Z3 内部的标识符，是一个整数，与 z3 模块中的常数比较就能看出含义。

print(f'{x_decl.kind() = }   # 用户定义的名称')
print(f'{expr_decl.kind() = }   # 比较运算符 >')

print(f'{z3.Z3_OP_UNINTERPRETED = }')
print(f'{z3.Z3_OP_GT = }')

x_decl.kind() = 49167   # 用户定义的名称
expr_decl.kind() = 517   # 比较运算符 >
z3.Z3_OP_UNINTERPRETED = 49167
z3.Z3_OP_GT = 517

x_decl.kind() 与 z3.Z3_OP_UNINTERPRETED 相同，因此 x 是用户定义的、不被解释的符号。expr_decl.kind() 是 z3.Z3_OP_GT，即大于运算符。kind() 返回的是整数编号，比较时要拿模块里的常数，不要直接写数字。

用 sexpr() 可以确认 Z3 内部持有的声明本身。

print(f'{x_decl.sexpr() = }')
print(f'{expr_decl.sexpr() = }')

x_decl.sexpr() = '(declare-fun x () Int)'
expr_decl.sexpr() = '(declare-fun > (Int Int) Bool)'

可以看出，x 被声明为 (declare-fun x () Int)，> 被声明为 (declare-fun > (Int Int) Bool)。

画成关系图#

把上面用到的对应关系画成图，箭头标出哪一个方法返回哪一个对象。

        graph
x["Int('x')\nArithRef"]
y["Int('y')\nArithRef"]
expr["x > y\nBoolRef"]
x_decl["x 的声明\nFuncDeclRef"]
expr_decl["> 的声明\nFuncDeclRef"]
int_sort["Int\nArithSortRef"]
bool_sort["Bool\nBoolSortRef"]

x --sort()--> int_sort
y --sort()--> int_sort
expr --sort()--> bool_sort
x --decl()--> x_decl
expr --decl()--> expr_decl
expr --arg(0)--> x
expr --arg(1)--> y
x_decl --range()--> int_sort
expr_decl --range()--> bool_sort
expr_decl --domain(0)--> int_sort
expr_decl --domain(1)--> int_sort

ModelRef：从模型取值#

Solver.model() 返回的是 ModelRef。ModelRef 的 [] 会因传入的内容不同而给出不同的结果。

x, y, z = Ints('x y z')
solver = Solver()
solver.add(x > y, y > z, x > 0, z < 5)
solver.check()
m = solver.model()

print(f'type(m) = {type(m).__name__}')
print(f'{m[x] = }  type = {type(m[x]).__name__}')
print(f'{m[0] = }  type = {type(m[0]).__name__}')

type(m) = ModelRef
m[x] = 1  type = IntNumRef
m[0] = z  type = FuncDeclRef

传入变量 m[x]，得到该变量的值，类型是 IntNumRef
传入整数 m[0]，得到第 0 个变量的声明，类型是 FuncDeclRef

IntNumRef 是 Z3 的整数值，但不是 Python 的 int，要参与计算必须用 as_long() 转换。转换是单向的：as_long() 得到的数已经与模型无关。

print(f'{m[x].as_long() = }')
print(f'type(m[x].as_long()) = {type(m[x].as_long()).__name__}')

# 传入表达式时，返回该表达式的值（BoolRef）
print(f'{m.eval(x > y) = }  type = {type(m.eval(x > y)).__name__}')

m[x].as_long() = 1
type(m[x].as_long()) = int
m.eval(x > y) = True  type = BoolRef

用 as_long() 就得到 Python 的整数，而把式传给 m.eval() 之后，返回的是该式的求值结果，这里是 x > y 的真假。

IntNumRef 的 decl() 得到的是表示 Int 这一值种类的声明，而不是变量的声明，与 x.decl() 即变量 x 的声明并不是一回事。

print(f'{m[x].decl().name() = }')
print(f'{x.decl().name() = }')
print(m[x].decl().eq(x.decl()))

m[x].decl().name() = 'Int'
x.decl().name() = 'x'
False

m[x].decl() 的名字是 'Int'，x.decl() 的名字是 'x'。同样是 decl()，作用的对象不同，含义也就随之不同。

验证继承关系#

用 type(obj).mro() 可以确认这个类继承了哪些类。

print(type(x).mro())
print(type(x.decl()).mro())
print(type(m).mro())

[<class 'z3.z3.ArithRef'>, <class 'z3.z3.ExprRef'>, <class 'z3.z3.AstRef'>, <class 'z3.z3.Z3PPObject'>, <class 'object'>]
[<class 'z3.z3.FuncDeclRef'>, <class 'z3.z3.AstRef'>, <class 'z3.z3.Z3PPObject'>, <class 'object'>]
[<class 'z3.z3.ModelRef'>, <class 'z3.z3.Z3PPObject'>, <class 'object'>]

ArithRef 依次继承 ExprRef、AstRef、Z3PPObject，而 FuncDeclRef 直接位于 AstRef 之下，与类图一致。mro() 给出的顺序就是 Python 查找属性时实际走的顺序。

下面把 AstRef 的子类实际列出来。

print([cls.__name__ for cls in z3.AstRef.__subclasses__()])


def print_tree(cls, indent=0, depth=2):
    print("  " * indent + cls.__name__)
    if depth == 0:
        return
    for sub in cls.__subclasses__():
        print_tree(sub, indent + 1, depth - 1)


print()
print_tree(z3.SortRef, depth=1)

['SortRef', 'FuncDeclRef', 'ExprRef']

SortRef
  TypeVarRef
  BoolSortRef
  ArithSortRef
  BitVecSortRef
  ArraySortRef
  FiniteSetSortRef
  DatatypeSortRef
  FiniteDomainSortRef
  FPSortRef
  FPRMSortRef
  SeqSortRef
  CharSortRef
  ReSortRef

可以看到 SortRef 之下排着 BoolSortRef、ArithSortRef、BitVecSortRef 等按类型划分的类，而前面各章用过的 BitVecSort、RealSort、IntSort 都属于 SortRef 这一族。

小结#

想知道的内容	使用的写法	返回的类型
变量与式的类型	`expr.sort()`	`SortRef`
式子子节点的个数	`expr.num_args()`	`int`
式的第 i 个子节点	`expr.arg(i)`	`ExprRef`
函数声明	`expr.decl()`	`FuncDeclRef`
函数的名字、参数与类型	`name()`、`arity()`、`range()`、`domain(i)`	字符串、数、`SortRef`
模型中的值	`m[x]`	`IntNumRef`
转成 Python 的整数	`.as_long()`	`int`

Int、Bool 与 x > y 都是 ExprRef，即式
类型是 SortRef，函数声明是 FuncDeclRef，式是 ExprRef，三者都属于 AstRef 一族
model[0] 取的是声明，model[x] 取的是值，同样是 []，含义并不相同