Julia 1.6.3使用Z3包触发TypeError: in typeassert错误解决方案问询

问题根因 #

报错是因为你依赖的Z3.jl版本对Z3.ExprAllocated类型实现的hash方法返回值为UInt32，而Julia 1.6在64位环境下的hashindex函数强制要求hash(key)返回值为UInt（64位环境下等价于UInt64），类型断言失败触发报错，和你写的业务逻辑本身无关。

快速修复方案 #

方案1：临时适配哈希方法（改动最小，无需修改原有业务逻辑）

在find_partition函数所在文件的头部添加以下代码，手动适配Julia的哈希返回类型要求：

import Base: hash, isequal

# 修正Z3表达式的哈希返回类型，满足Julia Dict的要求
hash(e::Z3.ExprAllocated, h::UInt) = hash(UInt64(Z3.hash(e)), h)
# 同步实现isequal方法，保证Dict键的比较逻辑正确
isequal(a::Z3.ExprAllocated, b::Z3.ExprAllocated) = Z3.equal(a, b)

添加后原有代码不需要做任何修改即可正常运行。

方案2：绕开Z3对象作为Dict键（兼容性最好）

将Z3求值后的常量转换为Julia原生类型作为键，完全规避Z3对象的哈希问题：

function find_partition(model::Model, ms)
    ps = Dict{Any,Vector{Int}}()
    for (i, m) in enumerate(ms)
        mval = Z3.eval(model, m, false)
        # 把Z3常量转换为Julia原生类型作为键
        if Z3.is_int(mval)
            key = Z3.get_int(mval)
        elseif Z3.is_rational(mval)
            num = Z3.get_numerator(mval)
            den = Z3.get_denominator(mval)
            key = num // den
        elseif Z3.is_real(mval)
            num = Z3.get_numerator(mval)
            den = Z3.get_denominator(mval)
            key = Float64(num) / Float64(den)
        else
            # 其他类型转字符串兜底
            key = string(mval)
        end
        if haskey(ps, key)
            push!(ps[key], i)
        else
            ps[key] = Int[i]
        end
    end
    values(ps)
end

关于降级Julia的说明 #

如果该包最初适配的是32位Julia，或是1.6之前的Julia版本，降级确实可以解决问题：32位环境下Julia的UInt本身就是UInt32，不会出现类型不匹配；1.6之前的部分Julia版本hashindex没有强制添加hash(key)::UInt的类型断言，也不会触发报错。但更推荐使用上面两种修复方案，不需要调整运行环境，后续适配新环境的成本更低。

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