如何按升序排列 Z3 生成的模型中的值？

Question

我正在使用 Z3 生成优化的时间表。检查可满足性后，我生成模型并将其存储到文本文件中。但是，我观察到 Z3 并没有真正以任何顺序排列模型中的值。有没有办法让Z3按升序排列？

这是它生成的变量值之一。

有没有办法让这个升序？

Answer 1

（本质上是重复来自的答案）

您可以将模型变成一个列表，然后按照您喜欢的方式对其进行排序。这是一个例子：

from z3 import *

v = [Real('v_%s' % (i+1)) for i in range(10)]

s = Solver()
for i in range(10):
    s.add(v[i] == i)
if s.check() == sat:
    m = s.model()
    print (sorted ([(d, m[d]) for d in m], key = lambda x: str(x[0])))

这会打印：

[(v_1, 0), (v_10, 9), (v_2, 1), (v_3, 2), (v_4, 3), (v_5, 4), (v_6, 5), (v_7, 6), (v_8, 7), (v_9, 8)]

请注意，名称是按字典顺序排序的，因此 v_10 在 v_1 之后和 v_2 之前。如果你希望v_10放在最后，你可以根据需要做进一步的处理。

在你的例子中，看起来 car 要么是一个数组值，要么是一个未解释的函数。对于这种特定情况，您必须分别查询您感兴趣的索引，并将它们收集到您自己的数据结构中，以便按照您喜欢的顺序显示它们。长话短说，z3 会为您提供这些值，但是如何 "present" 它们取决于您。（如果您遇到困难，请 post 您已经尝试过的示例，其他人可以复制以进一步帮助您。）

如何按升序排列 Z3 生成的模型中的值？

How do I arrange the values in the model generated by Z3 in an ascending order?

python

z3

z3py