#!/usr/bin/ruby cages = [ [3, [11,12]], [15,[13,14,15]], [22,[16,25,26,35]], [4, [17,27]], [16,[18,28]], [15,[19,29,39,49]], [25,[21,22,31,32]], [17,[23,24,]], [9, [33,34,44]], [8, [36,46,56]], [20,[37,38,47]], [6, [41,51]], [14,[42,43]], [17,[45,55,65]], [17,[48,57,58]], [13,[52,53,62]], [20,[54,64,74]], [12,[59,69]], [27,[61,62,63,64]], [6, [63,72,73]], [20,[66,76,77]], [6, [67,68]], [10,[75,84,85,94]], [14,[78,79,88,89]], [8, [82,92]], [16,[83,93]], [15,[86,87]], [13,[95,96,97]], [17,[98,99]] ] for i in 1 .. 9 for j in 1 .. 9 print "(define x#{i}#{j} :: nat)\n" end end for i in 1 .. 9 for j in 1 .. 9 print "(assert (>= x#{i}#{j} 1))\n" print "(assert (<= x#{i}#{j} 9))\n" end end def alldifferent xs for i in 0 ... xs.size for j in i+1 ... xs.size print "(assert (not (= #{xs[i]} #{xs[j]})))\n" end end end cages.each {|a| print "(assert (= #{a[0]} (+ #{a[1].map{|i| "x#{i}"}.join(" ")})))\n" alldifferent(a[1].map {|i| "x#{i}"}) } ns = 1 .. 9 ns.each {|i| alldifferent(ns.map {|j| "x#{i}#{j}"}) alldifferent(ns.map {|j| "x#{j}#{i}"}) } ns.each {|i| alldifferent(ns.map {|j| "x#{i}#{j}"}) } [1,4,7].each {|i| [1,4,7].each {|j| alldifferent( ["x#{i }#{j}","x#{i }#{j+1}","x#{i }#{j+2}", "x#{i+1}#{j}","x#{i+1}#{j+1}","x#{i+1}#{j+2}", "x#{i+2}#{j}","x#{i+2}#{j+1}","x#{i+2}#{j+2}"]) } } print "(set-evidence! true)\n(check)\n"