Z3のデータ型

Z3のデータ型#

import z3
from z3 import *

Z3 のクラス関係は以下のようになっています。

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

AstRef#

AstRef は有向非巡回グラフ（DAG）を表すクラスで、次の 3 種類のサブクラスがあります。

  • SortRef: Z3 における型（ソート）を表すクラス。BoolSortRef（ブール型）、ArithSortRef（整数や実数を含む算術型）などの派生クラスがあり、異なる種類のデータ型を表現する。

  • FuncDeclRef: 関数や演算子の宣言を表すクラス。例えば、+ や * などの算術演算子、論理演算子、ユーザー定義関数のシンボルを含み、関数の入力・出力の型情報を持つ。

  • ExprRef: Z3 の式（expression）を表すクラス。BoolRef（ブール式）、ArithRef（算術式）などの派生クラスがあり、具体的な式のインスタンスを表す。例えば、x + y のような算術式や x > y のような論理式が含まれる。QuantifierRef は量化子（forall や exists）を持つ論理式を表す。

Int、Boolや演算子で得られたのは全部ExprRefのインスタンスです。次のコードではIntsで二つのArithRefオブジェクトを作成し、比較演算子でBoolRefオブジェクトを作成します。

次のコードで、SortRef、FuncDeclRef、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

ExprRef#

このコードでは、x は ArithRef（ExprRef のサブクラス）であり、整数を表す変数です。一方、expr = x > y は BoolRef（ExprRef のサブクラス）であり、比較演算によるブール式を表します。

ExprRef.num_args()メソッドは、その式（ExprRef）が持つ引数の数を返します。単純な変数（x や y）は引数を持たないため num_args() は 0 になります。一方、expr = x > y は > 演算子による式であり、2 つの引数 x と y を持ちます。

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

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

ExprRef.arg(i) は ExprRef の i 番目の引数（0-based index）を取得するメソッドです。expr = x > y の場合、expr.arg(0) は x、expr.arg(1) は y を返します。つまり、ExprRef は式の構造を持ち、num_args() を使うことで式の子ノードの数を取得し、arg(i) を使うことで具体的な子ノードを参照できることが分かります。

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

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

ExprRef.sort()メソッドで式のデータ種類を取得できます。この種類を表すオブジェクトはSortRefのインスタンスです。

SortRef#

ExprRef.sort() は、式（ExprRef）のデータ型（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 は整数変数なので、x_sort は Int を表すソート（型）になります。x_sort の型（type(x_sort)）は ArithSortRef で、整数や実数を表す SortRef のサブクラスです。

expr = x > y は > による比較式なので、結果はブール型になります。したがって、expr_sort は Bool を表すソートになります。expr_sort の型（type(expr_sort)）は BoolSortRef で、ブール値を表す SortRef のサブクラスです。

FuncDeclRef#

ExprRef.decl() メソッドは、その式（ExprRef）の 関数宣言（FuncDeclRef） を取得するメソッドです。変数や演算子がどのような関数宣言に基づいているかを調べるのに役立ちます。

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 は整数変数ですが、Z3 内部では「関数 x()（定数関数）」として扱われるため、その宣言も FuncDeclRef 型になります。

  • expr = x > y は >（比較演算子）を使った式であり、この > も Z3 では「関数 >」として扱われます。

FuncDeclRef は Z3 における 関数や演算子の宣言 を表すクラスです。その関数の情報は、name(), arity(), range(), domain(), kind() などのメソッドを使って調べることができます。

  • name() は関数の名前を返します。

    • x_decl.name() は 'x' であり、変数の関数名はその変数名になります。

    • expr_decl.name() は '>' であり、比較演算子の関数名は演算子そのものになります。

  • arity() は、その関数が持つ引数の数を返します。

    • x_decl.arity() は 0 であり、x は定数（引数を持たない）。

    • expr_decl.arity() は 2 であり、x > y は 2 つの引数を取る二項演算子です。

  • range() は、関数が返す値の型（SortRef）を返します。

    • x_decl.range() は Int であり、x は整数型です。

    • expr_decl.range() は Bool であり、x > y はブール値を返します。

  • domain(i) は、その関数の i 番目の引数の型（SortRef）を返します。

    • expr_decl.domain(0) は Int であり、1 番目の引数 x は整数型です。

    • expr_decl.domain(1) は Int であり、2 番目の引数 y も整数型です。

  • kind() は、関数の種類（Z3 内部の識別子）を返します。

    • x_decl.kind() は z3.Z3_OP_UNINTERPRETED であり、これは ユーザーが定義したシンボル（変数） を意味します。

    • expr_decl.kind() は z3.OP_GT であり、これは 比較演算子 > を意味します。

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

x_decl.name() = 'x'
x_decl.arity() = 0
x_decl.range() = Int

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

expr_decl.name() = '>'
expr_decl.arity() = 2
expr_decl.range() = Bool

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

expr_decl.domain(0) = Int
expr_decl.domain(1) = Int

print(f'{x_decl.kind() = }') # z3.Z3_OP_UNINTERPRETED
print(f'{expr_decl.kind() = }') # z3.OP_LT

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

x_decl.kind() = 45102
expr_decl.kind() = 517
z3.Z3_OP_UNINTERPRETED = 45102
z3.Z3_OP_GT = 517

FuncDeclRef.sexpr() は、関数や演算子の S-Expression（シンボリック表現） を文字列として返すメソッドです。Z3 は内部で S-Expression という Lisp 風の構文を使って数式や論理式を表現しており、このメソッドを使うことでその構文を確認できます。

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

ExprRef、FuncDeclRef、および SortRef の関係を次のグラフで示します。

graph
vx((x))
vy((y))
vexpr((expr))
style vx fill:#9f9
style vy fill:#9f9
style vexpr fill:#9f9
x["Int('x')\nArithRef"]
y["Int('y')\nArithRef"]
expr["x > y\nBoolRef"]
style x fill:#99f
style y fill:#99f
style expr fill:#99f
func["FuncDeclRef()"]
int_func_x["FuncDeclRef()"]
int_func_y["FuncDeclRef()"]
style func fill:#f99
style int_func_x fill:#f99
style int_func_y fill:#f99
bool_sort["BoolSortRef()"]
int_sort["ArithSortRef()"]
style bool_sort fill:#ff9
style int_sort fill:#ff9
gt["'>'"]

vx --> x
vy --> y
vexpr --> expr
expr --arg(0)--> x
expr --arg(1)--> y
expr --decl()--> func
expr --sort()--> bool_sort
func --kind()--> Z3_OP_GT
func --name()--> gt
func --range()--> bool_sort
func --domain(0)--> int_sort
func --domain(1)--> int_sort
x --sort()--> int_sort
y --sort()--> int_sort
x --decl()--> int_func_x
y --decl()--> int_func_y
int_func_x --name()--> 'x'
int_func_x --range()--> int_sort
int_func_y --name()--> 'y'
int_func_y --range()--> int_sort
int_func_x --kind()--> Z3_OP_UNINTERPRETED
int_func_y --kind()--> Z3_OP_UNINTERPRETED

graph 
ArithRef["ArithRef\nInt('x')"]
ArithRef --decl()--> FuncDeclRef
ArithRef --sort()--> ArithSortRef
FuncDeclRef --name()--> 'x'
FuncDeclRef --range() --> ArithSortRef
FuncDeclRef --()--> ArithRef
ArithSortRef --name()--> 'Int'
ArithRef --is_int()--> True
ModelRef --[int]--> FuncDeclRef
ModelRef --[FuncDeclRef | ArithRef]--> IntNumRef
IntNumRef --sort()--> ArithSortRef
IntNumRef --as_long()--> 1

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

type(m.eval(x > y))

z3.z3.BoolRef

type(solver.assertions()[0])

z3.z3.BoolRef

xv.sort().eq(x.sort())

True

type(xv)

z3.z3.IntNumRef

type(m)

z3.z3.ModelRef

m[0].eq(x.decl())

True

x.decl().name()

'x'

xv = m[x]
xv.decl().name()

'Int'

x.as_lon

xv.
1
type(xv.sort())

z3.z3.ArithSortRef

xv.decl().eq(x.decl())

False

xv.decl().name()

'Int'

x.decl().ast

<FuncDecl object at 0x000001BBC18B3450>

xd = x.decl()
xd.range().eq(x.sort())

True

x.sort()
Int
xd.range()
Int
f = Function('haha', IntSort(), RealSort())

type(f.range())

z3.z3.ArithSortRef

xd.as_func_decl()

<FuncDecl object at 0x000001BBC0362050>

xd.
Int
type(xv.decl())

z3.z3.FuncDeclRef

x.ast

<Ast object at 0x000001BBC04AF3D0>

x.is_int()

True

x.decl().name()

'x'

x.sort()
Int
type(x).mro()

[z3.z3.ArithRef, z3.z3.ExprRef, z3.z3.AstRef, z3.z3.Z3PPObject, object]

type(x.decl()).mro()

[z3.z3.FuncDeclRef, z3.z3.AstRef, z3.z3.Z3PPObject, object]

x.decl()().ast.value

1905841136352

z3.AstRef.__subclasses__()

[z3.z3.SortRef, z3.z3.FuncDeclRef, z3.z3.ExprRef]

type(IntSort())

z3.z3.ArithSortRef

Function??

Signature: Function(name, *sig)
Source:   
def Function(name, *sig):
    """Create a new Z3 uninterpreted function with the given sorts.

    >>> f = Function('f', IntSort(), IntSort())
    >>> f(f(0))
    f(f(0))
    """
    sig = _get_args(sig)
    if z3_debug():
        _z3_assert(len(sig) > 0, "At least two arguments expected")
    arity = len(sig) - 1
    rng = sig[arity]
    if z3_debug():
        _z3_assert(is_sort(rng), "Z3 sort expected")
    dom = (Sort * arity)()
    for i in range(arity):
        if z3_debug():
            _z3_assert(is_sort(sig[i]), "Z3 sort expected")
        dom[i] = sig[i].ast
    ctx = rng.ctx
    return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
File:      c:\micromamba\envs\cad\lib\site-packages\z3\z3.py
Type:      function

### type(x.sort()).mro()

x.decl().sort()

---------------------------------------------------------------------------
AttributeError                            Traceback (most recent call last)
Cell In[56], line 1
----> 1 x.decl().sort()

AttributeError: 'FuncDeclRef' object has no attribute 'sort'

x.decl().ast.value

1905841142496

x.ctx

<z3.z3.Context at 0x1bbbdf80b90>

x.ctx_ref()

<ContextObj object at 0x000001BBBE1AF550>

xa = x.ast

xa.value

1905841136352

from helper.python import print_subclasses
print_subclasses(z3.AstRef.mro()[1])
Contents