Alloyのイラストロジックをリファクタリングした日記

ColとRowで似たようなことを別個にやっているので、まとめられるかも、ということで挑戦してみた日記。
ColとRowで個別のnextが入っている点が難しいかもとのことでしたが、そもそもCol -> Row -> ColorのRowだけ固定してCol -> Colorを作る方法がわからなくてどん詰まり。悩んだ挙句「Col -> Color -> Rowにすればいいんだ！」という解決の仕方をしました。

ついでにColとRowを区別するのが面倒だったので両方Intにしました。

one sig Root{
  cell: Int -> Color -> Int
}{
  all x: cell.univ.univ | in_ten[x]
  all y: univ.(univ.cell) | in_ten[y]
  let ten = {x: Int | in_ten[x]}{
    all x, y: ten{
      one x.cell.y
    }
  }
}

pred in_ten(x: Int){
  one x
  0 <= x and x < 10  // notice: for 5 Int required
}

こうしたことで、rowHintとcolHintはすぐにseq Colorを作って共通の処理に入ることが出来るようになりました。

pred hint(line: seq Color, sizes: seq Int){
  some heads: seq Int {
    #heads = #sizes
    sorted[get_heads[line], heads]
    all i: sizes.inds {
      let start = heads[i], end = get_end[start, sizes[i]] {
        one line[end]
        all_black[line, start, end]
        next_is_not_black[line, end]
      }
    }
  }
}
pred colHint (i: Int, sizes: seq Int) {
  hint[getCol[i], sizes]
}
pred rowHint (i: Int, sizes: seq Int) {
  hint[getRow[i], sizes]
}

で、残念ながらこのリファクタリングしたバージョンはコードクローンはなくなったものの、オリジナルより2倍ほど遅くなっています。むむむ。これはオリジナルがfor 10でColとRowの数を10個に限定できているのに対して、こっちはIntにしてしまったから-16〜15の範囲に広がってしまっているせいか？？

# Original
33381 vars. 2200 primary vars. 92568 clauses. 854ms.
... is consistent. 415ms.
# Refactored
73481 vars. 4608 primary vars. 219033 clauses. 1426ms.
...is consistent. 858ms.

うーん、そうみたい。泥臭いけどsig SmallIntを作って10個に限定したらかなり縮んだ。

30402 vars. 2848 primary vars. 75273 clauses. 888ms.
... is consistent. 1307ms.

代表的な変更箇所は下の通り。もちろん型の整合性のために何箇所か修正する必要があった。

+sig SmallInt{}
+fun from_int (i: Int): SmallInt {
+  {x: SmallInt | #(x.prevs) = i}
+}
+
+fun to_int (x: SmallInt): Int {
+  #(x.prevs)
+}
+
 pred hint(line: seq Color, sizes: seq Int){
-  some heads: seq Int {
+  some heads: seq SmallInt {

前回の僕の重すぎて動かないコードではsomeが6個ネストしてたわけなんだけども、bonotakeさんのコードでは1個になっていて、そしていまやったようにそのsomeの探索範囲を減らすと生成されるCNFも実行時間も大きく削減されるようだ。someは要注意だな。

ソースコードはこちらから: https://github.com/nishio/learning_alloy/tree/master/illust_logic