Alloy 和 Kodkod 中的总排序优化

Question

在不同的地方（例如这里enter link description here 或there）都说总排序关系是硬连线的，以提高分析效率（并使原子名称以“自然”顺序出现） .

据我了解，优化是在 Kodkod (in this piece of code) 中进行的。但是，是否有一篇文章或文档更详细地解释了（比 Java 文档，它用布尔矩阵说话并且没有为算法提供论证——这在源代码文档中很好——）在科德科德？据我所知，E. Torlak 的博士论文没有提到这些（I. Shlyakhter 的一篇论文谈到了其他优化，但我不知道这些是在 Kodkod 还是 Alloy 中实现的）。

Answer 1

此优化是在 Kodkod 中进行的，位于您找到的代码位置。在Ilya Shlyakhter's PhD thesis（第 111 页，第 4.5.5 节）中对其进行了简要描述。