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（抽象構文木のノード）には、3種類のサブクラスがあります。

クラス

表すもの

例

SortRef

型（ソート）

Int, Bool, BitVec(8)

FuncDeclRef

関数や演算子の宣言

x（変数）、>（比較演算子）

ExprRef

式

x, x + y, x > y

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 は引数を持たないので 0、x > y は x と y の2つを引数に持つので 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 内部の種類（整数のID）

sexpr()

S式（Lisp 風のテキスト表現）

 
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、つまり「より大きい」演算子です。

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() で変換します。

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 の直下です。クラス図のとおりになっています。

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。3つとも AstRef の仲間

  • model[0] は宣言、model[x] は値。同じ [] でも意味が違う