Z3，使用数据类型创建数据结构/类。

在Z3中，可以使用数据类型创建自定义的数据结构或类。以下是一个示例代码：

from z3 import *

# 创建一个数据类型Point，包含两个整数字段x和y
Point = Datatype('Point')
Point.declare('mk_point', ('x', IntSort()), ('y', IntSort()))
Point = Point.create()

# 创建一个数据类型Rectangle，包含两个Point字段top_left和bottom_right
Rectangle = Datatype('Rectangle')
Rectangle.declare('mk_rectangle', ('top_left', Point), ('bottom_right', Point))
Rectangle = Rectangle.create()

# 创建两个Point对象
p1 = Point.mk_point(0, 0)
p2 = Point.mk_point(3, 3)

# 创建一个Rectangle对象
rect = Rectangle.mk_rectangle(p1, p2)

# 打印Rectangle对象的字段值
print('Top left: ({}, {})'.format(rect.top_left.x, rect.top_left.y))
print('Bottom right: ({}, {})'.format(rect.bottom_right.x, rect.bottom_right.y))

在上面的代码中，首先使用Datatype函数创建了两个数据类型Point和Rectangle。然后，使用declare方法声明了每个数据类型的字段。最后，使用create方法创建了实际的数据类型。

在示例中，Point数据类型包含两个整数字段x和y，Rectangle数据类型包含两个Point字段top_left和bottom_right。使用mk_point和mk_rectangle方法可以创建Point和Rectangle对象。

最后，通过访问对象的字段可以获取其值，并将其打印出来。