Skip to main content
 首页 » 编程设计

python之Z3PY 方程,大小限制

2025年01月19日14emanlee

我正在研究 Z3PY 我想知道如何限制方程计算的大小

    v0 = Int('v0') 
    const = 0x12345678 
    I wrote this :  
s.add( (const*(v0 + const*(func(v0*const) - v0)) - v0) == somevalueof64bits) 

我的问题是 '(const*(v0 + const*(func(v0*const) - v0)) - v0)' 的计算大于 64 位

请您参考如下方法:

Z3 中的整数(通常在 SMT 求解器中)不受机器整数表示的限制。在底层,它使用大整数表示,允许使用任意大小的整数进行计算。