Alloy和Kodkod中總排序的優化

Question

據說在不同的地方（例如這裏的enter link description here或there）爲了提高分析效率（以及讓原子名稱出現在「自然「的順序）。

據我所知，優化是在Kodkod（in this piece of code）。然而，是否有一篇文章或文檔更詳細地解釋了（比Java文檔，它是用布爾矩陣表示的，並且沒有提供該算法的論證 - 在源代碼文檔中沒有問題 - ）優化在南美林貓？據我所知，E.Torlak的博士論文沒有提到這些論點（Shlyakhter一篇關於其他優化的論文，但我不知道這些論文是否在Kodkod或Alloy中實現）。

Answer 1

此優化是在您找到的代碼位置的Kodkod中進行的。在Ilya Shlyakhter's PhD thesis（第111頁，第4.5.5節）中對此進行了簡要介紹。