如何限制Z3Py自定义列表类型中head仅作用于cons构造的列表？

Z3的代数数据类型（ADT）访问器（如head、tail）默认是全函数，即对该类型的所有值（包括empty）都有定义，因此直接调用head(empty)不会触发矛盾，只会保留未解释的表达式。要限制head仅作用于cons构造的列表，有两种实用方案：

方案一：显式添加类型断言 #

每次使用head或tail时，额外添加断言声明目标列表是cons类型。Z3为自定义ADT自动生成了is_cons和is_empty谓词，可直接用来约束：

from z3 import *

def ListSort(sort):
    listType = Datatype('List(%s)' % str(sort))
    listType.declare('cons', ('head', sort), ('tail', listType))
    listType.declare('empty')
    return listType.create()

IntListSort = ListSort(IntSort())
# 提取ADT的谓词和构造/访问函数
Is_cons = IntListSort.is_cons
head = IntListSort.head
empty = IntListSort.empty

x = Int('x')
# 正确用法：添加Is_cons断言，确保head作用于cons列表
solve(x == 1 + head(IntListSort.cons(5, empty)), Is_cons(IntListSort.cons(5, empty)))

# 错误用法测试：添加Is_cons(empty)会直接导致不可满足
solve(x == 1 + head(empty), Is_cons(empty))

这种方式清晰直接，适合简单场景，能精准控制每个head调用的约束范围。

方案二：封装安全访问函数 #

将head和约束逻辑封装成安全函数，避免重复编写断言。可以用Z3的DefineFun定义带约束的访问器，或编写辅助函数自动生成约束：

方式1：定义带默认值的安全head #

当输入为empty时返回一个默认值（或触发矛盾）：

from z3 import *

def ListSort(sort):
    listType = Datatype('List(%s)' % str(sort))
    listType.declare('cons', ('head', sort), ('tail', listType))
    listType.declare('empty')
    return listType.create()

IntListSort = ListSort(IntSort())
Is_cons = IntListSort.is_cons
head = IntListSort.head
empty = IntListSort.empty

# 定义安全head：仅当列表是cons时返回head，否则返回0（可替换为任意合法值）
safe_head = DefineFun('safe_head', [('l', IntListSort)], IntSort(),
                     If(Is_cons(l), head(l), 0))

x = Int('x')
# 使用safe_head，传入empty会返回0
solve(x == 1 + safe_head(empty))

# 若要禁止empty输入，可将else分支设为矛盾值（如未约束的变量+断言排除）
safe_head_strict = DefineFun('safe_head_strict', [('l', IntListSort)], IntSort(),
                            If(Is_cons(l), head(l), Int('invalid')))
# 添加断言：禁止返回invalid值
solve(x == 1 + safe_head_strict(empty), safe_head_strict(empty) != Int('invalid'))

方式2：辅助函数自动生成约束 #

编写辅助函数，同时返回head的值和对应的类型约束：

def safe_head_access(l):
    return head(l), Is_cons(l)

x = Int('x')
l = IntListSort('l')
# 获取head值和约束，一并传入求解器
head_val, constraint = safe_head_access(l)
solve(x == 1 + head_val, constraint)

这种方案适合复杂场景，能减少重复代码，让逻辑更简洁。

注意事项 #

• 全域量化约束（如ForAll([l], Implies(Is_empty(l), Not(Exists([x], x == head(l)))))）虽然能全局禁止head(empty)，但会大幅增加求解器的负担，不建议在复杂模型中使用。
• Z3的ADT设计本身允许访问器作用于任意值，所有的约束都需要显式声明，这是基于一阶逻辑的语义特性，并非设计缺陷。

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