thun/TLA.pl

   1 \r
   2 :- use_module(library(clpfd)).\r
   3 \r
   4 \r
   5 % relly(PC, I, PCnext, Inext).\r
   6 \r
   7 initial_state :- relly(start, 0, _, _).\r
   8 \r
   9 relly(start, _I, middle, Inext) :- Inext in 0..1000.\r
  10 relly(middle, I,   done, Inext) :- Inext #= I + 1.\r
  11 \r
  12 \r
  13 % next(PC, I) :- \r
  14 next(done, _).\r
  15 next(PC, I) :- PC \= done, relly(PC, I, PCnext, Inext), next(PCnext, Inext).\r
  16 \r
  17 \r
  18 % ?- relly(start, 17, middle, 534).\r
  19 % true.\r
  20 \r
  21 % ?- relly(middle, 534, 77, done).\r
  22 % false.\r
  23 \r
  24 % ?- initial_state.\r
  25 % true.\r
  26 \r
  27 % ?- relly(start, 0, PC, I).\r
  28 % PC = middle,\r
  29 % I in 0..1000.\r
  30 \r
  31 % ?- relly(start, 0, PC, I), relly(PC, I, PCnext, Inext).\r
  32 % PC = middle,\r
  33 % PCnext = done,\r
  34 % I in 0..1000,\r
  35 % I+1#=Inext,\r
  36 % Inext in 1..1001.\r
  37 \r
  38 \r
  39 \r
  40 \r
  41 \r
  42 \r
  43 \r
  44 \r
  45 \r
  46 \r
  47 \r
  48 \r
  49 \r
  50 \r
  51 \r
  52 \r
  53 \r
  54 \r
  55 \r
  56 \r
  57 \r
  58 \r
  59 \r
  60 \r
  61 \r
  62 type_ok(Small, Big) :- Small in 0..3, Big in 0..5.\r
  63 \r
  64 \r
  65 next_dh(Moves) :- next_dh(0, 0, Moves).\r
  66 \r
  67 next_dh(Small, Big, [[Move, Si, Bi]|Moves]) :-\r
  68     type_ok(Small, Big),\r
  69     die_hard(Move, Small, Big, Si, Bi),\r
  70     (Bi = 4 -> Moves = [] ; next_dh(Si, Bi, Moves)).\r
  71 \r
  72 \r
  73 die_hard( fill_small, Small, Big, 3, Big) :- Small #< 3.\r
  74 die_hard(   fill_big, Small, Big, Small, 5) :- Big #< 5.\r
  75 die_hard(empty_small, Small, Big, 0, Big) :- Small #> 0.\r
  76 die_hard(  empty_big, Small, Big, Small, 0) :- Big #> 0.\r
  77 \r
  78 die_hard(small_to_big, Small, Big, S, B) :-\r
  79     Big #< 5, Small #> 0,\r
  80     small_to_big(Small, Big, S, B).\r
  81 \r
  82 die_hard(big_to_small, Small, Big, S, B) :-\r
  83     Small #< 3, Big #> 0,\r
  84     big_to_small(Small, Big, S, B).\r
  85 \r
  86 \r
  87 big_to_small(Small, Big, S, 0) :-\r
  88     Small + Big #=< 3,\r
  89     S #= Small + Big.\r
  90 \r
  91 big_to_small(Small, Big, 3, B) :-\r
  92     Small + Big #> 3,\r
  93     B #= Big - (3 - Small).\r
  94 \r
  95 \r
  96 small_to_big(Small, Big, 0, B) :-\r
  97     Small + Big #=< 5,\r
  98     B #= Small + Big.\r
  99 \r
 100 small_to_big(Small, Big, S, 5) :-\r
 101     Small + Big #> 5,\r
 102     S #= Small - (5 - Big).\r
 103 \r
 104 \r
 105 \r
 106 \r
 107 \r
 108 \r
 109 \r
 110 \r
 111 \r
 112 \r
 113 \r
 114 \r
 115 \r
 116 \r
 117 \r
 118 \r
 119 \r
 120 \r
 121 \r
 122 \r
 123 \r
 124 \r
 125 \r
 126 \r
 127 \r
 128 \r
 129 \r
 130 \r
 131 \r
 132 \r
 133 \r
 134 \r
 135 \r
 136 \r
 137 /*\r
 138 \r
 139 With some manual reflow of the list for presentation...\r
 140 \r
 141 ?- call_with_depth_limit(next_dh(Moves), 11, _).\r
 142 Moves = [\r
 143     [fill_big, 0, 5],\r
 144     [big_to_small, 3, 2],\r
 145     [empty_small, 0, 2],\r
 146     [big_to_small, 2, 0],\r
 147     [fill_big, 2, 5],\r
 148     [big_to_small, 3, 4]\r
 149     ] ;\r
 150 true.\r
 151 \r
 152 \r
 153 \r
 154 \r
 155 \r
 156 \r
 157 \r
 158 \r
 159 \r
 160 \r
 161 \r
 162 \r
 163 \r
 164 \r
 165 \r
 166 \r
 167 \r
 168 \r
 169 \r
 170 \r
 171 \r
 172 \r
 173 \r
 174 \r
 175 \r
 176 \r
 177 \r
 178 \r
 179 \r
 180 call_with_depth_limit(next_dh(0, 0, S, B), 12, REsult).\r
 181 \r
 182 find...\r
 183 \r
 184 fill big\r
 185 0 0 -> 0 5\r
 186 big to small\r
 187 0 5 -> 3 2\r
 188 empty small\r
 189 3 2 -> 0 2\r
 190 big to small\r
 191 0 2 -> 2 0\r
 192 fill big\r
 193 2 0 -> 2 5\r
 194 big to small\r
 195 2 5 -> 3 4\r
 196 \r
 197 \r
 198 */