如何按升序排列 Z3 生成的模型中的值？ [复制]答案

【问题标题】：How do I arrange the values in the model generated by Z3 in an ascending order? [duplicate]如何按升序排列 Z3 生成的模型中的值？ [复制]
【发布时间】：2018-12-27 04:57:57
【问题描述】：

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

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

有没有办法让这个上升？

【问题讨论】：

标签： python z3 z3py

【解决方案1】：

（基本上重复来自：How to print z3 solver results print(s.model()) in order? 的答案）

您可以将模型变成一个列表并以您喜欢的任何方式对其进行排序。这是一个例子：

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 会给你价值，但你如何“呈现”它们取决于你。（如果您遇到困难，请发布您尝试过的示例，其他人可以复制以进一步帮助您。）

【讨论】：

在cpp中有没有这么简单的方法可以做到这一点？
@GermanShepherd 当然。在 z3 具有接口的所有语言中，这种事情都是可能的。你试过什么？随意提出一个单独的问题。
感谢@alias。是的，我可以在 cpp 中完成。