Z3 SMT求解器中数据类型选择器是否必须唯一？

选择器是否必须唯一？ #

不需要。Z3允许在同一个Datatype的不同构造器中使用同名的字段（选择器），建模时不会因此报错，约束求解也能正常运行。

为何建模可行但提取值时始终得到0？ #

问题出在Python API的选择器调用方式上：

• 当你为mk_move_cmd和mk_turn_cmd都声明time字段后，Z3会为每个构造器生成独立的选择器函数，命名规则是构造器名_字段名。比如mk_move_cmd的time字段对应的正确选择器是Command.mk_move_cmd_time()，mk_turn_cmd的是Command.mk_turn_cmd_time()。
• 你直接调用Command.time(command)时，这个函数并没有绑定到特定构造器的time字段，Z3无法正确识别你要提取哪个构造器的字段值，因此会返回整数类型的默认值0。
• 即便你通过is_mk_move_cmd判断了command的类型，Command.time()依然不是对应构造器的正确选择器，所以提取结果始终错误。

修复方法 #

根据command的实际构造器类型，调用对应的选择器函数：

if model.eval(Command.is_mk_move_cmd(command)):
    name = 'mk_move_cmd'
    time = model.eval(Command.mk_move_cmd_time(command)).as_long()
elif model.eval(Command.is_mk_turn_cmd(command)):
    name = 'mk_turn_cmd'
    time = model.eval(Command.mk_turn_cmd_time(command)).as_long()

内容的提问来源于stack exchange，提问作者Klaus Havelund