Z3 Solver模型输出排序异常（10排在1后）的处理方法问询

Z3 Solver默认调用print(s.model())输出结果时，会出现类似x10排在x1之后的问题，原因是默认排序仅按字符串的首字符顺序比较，而非变量名中数字的实际数值大小。要修复这个问题，需要对模型结果进行自定义排序处理，具体步骤和代码示例如下：

具体处理步骤 #

• 从求解器模型中提取所有变量与对应的值
• 自定义排序规则：提取变量名中的数字部分，转换为整数后进行数值排序；无数字的变量可按原字符串排序
• 遍历排序后的结果，逐个输出变量及对应值

代码示例 #

from z3 import *

# 定义示例变量
x1 = Int('x1')
x10 = Int('x10')
x2 = Int('x2')

s = Solver()
s.add(x1 == 1, x2 == 2, x10 == 10)
s.check()

model = s.model()

# 定义排序键：提取变量名中的数字转为整数，用于排序
def sort_key(element):
    var_name = element.decl().name()
    # 提取变量名中的所有数字字符
    num_str = ''.join(c for c in var_name if c.isdigit())
    if num_str:
        # 有数字的按数字大小排序，同时保留原变量名作为次要排序键
        return (int(num_str), var_name)
    else:
        # 无数字的变量放在最后（可根据需求调整顺序）
        return (float('inf'), var_name)

# 对模型元素进行排序
sorted_model = sorted(model, key=sort_key)

# 输出排序后的结果
for item in sorted_model:
    print(f"{item.decl().name()} = {item.as_long()}")

这段代码会输出：

x1 = 1
x2 = 2
x10 = 10

如果变量名格式不同（比如var_1、var_10），只需调整num_str的提取逻辑，确保准确获取数字部分即可。

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