如何让Z3浮点数求解结果固定而非随机？

Z3的浮点数求解模块有独立的配置逻辑，常规的整数求解种子设置无法覆盖浮点数求解器的随机化策略，需要针对浮点数模块单独配置：

• 改用QF_FP专用求解器：避免通用求解器自动选择带有随机启发式的策略，强制使用确定性的浮点数求解路径
• 单独禁用浮点数求解器的随机化：设置fp.randomize=False，这是浮点数模块特有的配置项
• 补充设置算术相关的随机种子：确保所有可能影响求解的种子都固定

修改后的代码如下：

from z3 import *

# 全局固定算术及浮点数相关种子
set_option('smt.random_seed', 0)
set_option('smt.arith.random_seed', 0)
set_option('smt.arith.random_initial_value', False)

def test_short_expont():
    float_type = Float32()
    # 指定QF_FP逻辑，使用专用浮点数求解器
    solver = SolverFor("QF_FP")
    # 禁用浮点数求解器的随机化
    solver.set("fp.randomize", False)
    
    fp_5 = FP('fp_5', float_type)
    fp_10 = FP('fp_10', float_type)
    
    solver.add(fpEQ(fpAdd(RNE(), fp_5, fp_5), fp_10))
    
    if solver.check() == sat:
        model = solver.model()
        return model
    else:
        return

# 测试运行
print(test_short_expont())

修改后每次运行都会得到相同的模型结果，解决了浮点数求解的随机性问题。

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