1:- module(minato_r5, []). 2 3:- use_module(util(math)). 4:- use_module(util(meta2)). 5:- use_module(pac(basic)). 6:- use_module(pac(meta)). 7:- use_module(util(misc)). 8:- use_module(pac('expand-pac')). 9:- use_module(zdd('zdd-array')). 10:- use_module(zdd(zdd)). 11:- use_module(zdd('zdd-misc')). 12:- use_module(zdd('zdd-plain')). 13:- use_module(pac(op)). 14:- op(1060, xfy, #). % exor 15:- op(1000, xfy, &). 16 17term_expansion --> expand_pac. 18 19 /****************** 20 * Switches * 21 ******************/ 22% SKEW. 23 24active_node(X, Y):- active_node_skew(X, Y). 25rect_nodes(X, Y):- rect_nodes_skew(X, Y). 26% ?- minato_r5(rect(0,0), C). 27% ?- minato_r5(rect(1,0), C). 28% ?- minato_r5(rect(0,1), C). 29% ?- minato_r5(rect(1,1), C). 30% ?- minato_r5(rect(1,2), C). 31% ?- minato_r5(rect(2,1), C). 32% ?- minato_r5(rect(2,2), C). 33% ?- minato_r5(rect(1,10), C). 34% ?- minato_r5(rect(10,1), C). 35% ?- minato_r5(rect(100,1), C). 36% ?- minato_r5(rect(1,100), C). 37% ?- time(minato_r5(rect(6,6), C)). 38% ?- time(minato_r5(rect(7,7), C)). 39% ?- time(minato_r5(rect(8,8), C)). 40%@ % 735,769,679 inferences, 73.508 CPU in 74.736 seconds (98% CPU, 10009356 Lips) 41%@ C = 3266598486981642. 42 43%@ % 866,692,457 inferences, 66.719 CPU 44%@ % 860,196,004 inferences, 54.797 CPU 45%@ C = 3266598486981642. 46% ?- time(minato_r5(rect(9,9), C)). 47%@ % 3,967,432,258 inferences, 254.227 48%@ C = 41044208702632496804. 49% ?- call_with_time_limit(1800, time(minato_r5(rect(10,10), C))). 50%@ % 12,782,653,306 inferences, 1164.030 CPU 51%@ C = 1568758030464750013214100, 52% ?- call_with_time_limit(36000, minato_r5(rect(11,11), C, _)). 53%@ C = 182413291514248049241470885236. 54 55orth_skew(p(I, J), Y):- var(Y), !, 56 Y = p(K, I), 57 K is I + J. 58orth_skew(p(I, J), p(K, I)):- J is K - I. 59 60% ?- arrow_symbol(_->_, F). 61% ?- arrow_symbol(a->b, F, X, Y). 62change_symbol(A-B, A->B). 63arrow_symbol( _ -> _). 64arrow_symbol(A, A0):- functor(A, A0, 2). 65arrow_symbol(A, A0, A1, A2):- functor(A, A0, 2), 66 arg(1, A, A1), 67 arg(2, A, A2). 68% 69is_link(->(_, _)). 70% 71convert_normal_pair(P, Q):- orth_skew_pair(P, Q0), 72 normal_pair(Q0, Q). 73% 74 75normal_arrow(A->B, Arr):-!, 76 ( zdd_compare(>, A, B) -> Arr = (B->A) 77 ; Arr = (A->B) 78 ). 79normal_arrow(A-B, Arr):-normal_arrow(A->B, Arr). 80% 81 82lt_pair(_ - A, B -_):- zdd_compare(<, A, B). 83 84 /************************************* 85 * basics of incrementing DG * 86 *************************************/ 87 88composable_pairs(A-B, A-C, B, C). 89composable_pairs(A-B, C-A, B, C). 90composable_pairs(B-A, A-C, B, C). 91composable_pairs(B-A, C-A, B, C). 92% 93% 94normal_pair(A-B, B-A):- zdd_compare(>, A, B), !. 95normal_pair(A->B, B->A):- zdd_compare(>, A, B), !. 96normal_pair(P, P). 97 98% ?- orth_skew_pair(p(1,1)-p(2,2), X), orth_skew_pair(Y, X). 99%@ X = p(2, 1)-p(4, 2), 100%@ Y = p(1, 1)-p(2, 2). 101orth_skew_pair(P, Q):- 102 ( P = (A-B) -> Q = (A0-B0) 103 ; P = (A->B), 104 Q = (A0->B0) 105 ), 106 orth_skew(A, A0), 107 orth_skew(B, B0). 108% ?- link_sort_opp([loop, a, loop], X). 109link_sort_opp(X, Y):- sort(X, X0), reverse(X0, Y). 110 111% ?- node_ends(p(0,0), En, rect(1,1)). 112% ?- node_ends(p(0,0), En, rect(0,0)). 113% ?- node_ends(p(1,1), En, rect(2,2)). 114 115node_ends(P, En, rect(W,H)):- P = p(I,J), 116 ( I < W -> 117 K is I + 1, 118 En0 = [p(K,J)] 119 ; En0 = [] 120 ), 121 ( J < H -> 122 L is J + 1, 123 En = [p(I, L)|En0] 124 ; En = En0 125 ). 126 127% ?- node_ends_skew(p(0,0), En, rect(1,1)). 128% ?- node_ends_skew(p(0,0), En, rect(0,0)). 129% ?- node_ends_skew(p(1,1), En, rect(2,2)). 130% ?- node_ends_skew(p(1,1), En, rect(1,2)). 131node_ends_skew(P, En, rect(W,H)):- P = p(I,J), 132 ( J < W -> 133 K is J + 1, 134 M is I + 1, 135 En0 = [p(M, K)] 136 ; En0 = [] 137 ), 138 ( I < H + J -> 139 L is I + 1, 140 En = [p(L, J)|En0] 141 ; En = En0 142 ). 143 144% ?- R=rect(2,2), repeat(in_rect(P, R), 145% (node_ends_shadows(P, En, Sh, R), writeln(P-En-Sh))). 146in_rect(p(I, J), rect(W, H)):- between(0, W, I), between(0, H, J). 147 148% ?- rect_nodes_orth(rect(1,1), PES), maplist(writeln, PES). 149%@ p(0,0)-[p(0,1),p(1,0)] 150%@ p(0,1)-[p(1,1)] 151%@ p(1,0)-[p(1,1)] 152%@ p(1,1)-[] 153%@ PES = [p(0, 0)-[p(0, 1), p(1, 0)], p(0, 1)-[p(1, 1)], p(1, 0)-[p(1, 1)], p(1, 1)-[]]. 154 155% ?- rect_udg(rect(1,1), Links, P). 156%@ Links = [p(0, 0)-p(0, 1), p(0, 0)-p(1, 0), p(0, 1)-p(1, 1), p(1, 0)-p(1, 1)], 157%@ P = p(0, 0)-p(1, 1). 158 159rect_udg(rect(W, H), Links, p(0,0)-p(W,H)):- 160 rect_nodes_orth(rect(W, H), PES), 161 findall(U-V, ( member(U-L, PES), member(V, L), U @< V ), Links). 162 163% ?- rect_nodes_orth(rect(3,3), PES), maplist(writeln, PES). 164% ?- rect_nodes_orth(rect(10,10), PES), maplist(writeln, PES). 165% ?- rect_nodes_orth(rect(30,30), PES), length(PES, L). 166% ?- rect_nodes_orth(rect(100,100), PES), length(PES, L). 167% ?- time((rect_nodes_orth(rect(1000,1000), PES), length(PES, L))). 168 169rect_nodes_orth(R, PES):- 170 findall(P-E, (in_rect(P, R), node_ends(P, E, R)), PES). 171 172% ?- rect_nodes_skew(rect(100,100), PES), length(PES, L). 173% ?- time((rect_nodes_skew(rect(1000,1000), PES), length(PES, L))). 174rect_nodes_skew(R, PES_skew):- rect_nodes_orth(R, PES_orth), 175 convert_orth_skew(PES_orth, PES_skew). 176% 177convert_orth_skew([], []). 178convert_orth_skew([A-B|C], [A0-B0|C0]):- 179 orth_skew(A, A0), 180 maplist(orth_skew, B, B0), 181 convert_orth_skew(C, C0). 182 183 /**************************************************** 184 * replace_end/bypass: Most basic operations. * 185 ****************************************************/ 186 187% ?- zdd((X<<{[c-d]}, @(subst_node([a->c], c, a, X, Y)), psa(X), psa(Y))). 188subst_node(_, _, _, X, 0):- X < 2, !. 189subst_node(Es, A, P, X, Y):- /* replace A with P */ 190 cofact(X, t(U, L, R)), 191 arrow_symbol(U, Arrow, Lu, Ru), 192 ( Arrow = (->) -> Y = 0 193 ; zdd_compare(<, A, Lu) -> Y = 0 194 ; subst_node(Es, A, P, L, L0), 195 ( Ru = A -> 196 normal_pair(Lu-P, V), 197 zdd_ord_insert([V|Es], R, R0) 198 ; Lu = A -> 199 normal_pair(Ru-P, V), 200 zdd_ord_insert([V|Es], R, R0) 201 ; subst_node(Es, A, P, R, R1), 202 zdd_insert(U, R1, R0) 203 ), 204 zdd_join(L0, R0, Y) 205 ). 206 207% ?- zdd((X<<{[a-b, c-d]}, psa(X), @(add_links([b-c], X-X0, 0-Y)), psa(Y))). 208% ?- zdd((X<<{[a-b, c-d]}, psa(X), @(add_links([b-c], X-X0, 0-Y)), psa(Y))). 209% ?- zdd((X<<{[a-b, c-c, a->x, b->x]}, psa(X), @(add_links([a-b], X-X0, 0-Y)), psa(Y))). 210add_links([], X, X). 211add_links([L|Ls], X, X0):- 212 add_link(L, X, X1), 213 zdd_join(X, X1, X2), 214 add_links(Ls, X2, X0). 215 216% ?- zdd((X<<{[a-b, c-d]}, psa(X), @(add_link(b-c, X, Y)), psa(Y))). 217add_link(_, X, 0):- X<2, !. 218add_link(U, X, Y):- % memo is useless here 219 cofact(X, t(A, L, R)), 220 ( A = (_->_) -> Y = 0 221 ; add_link(U, L, L0), 222 U = Ul-Ur, 223 ( lt_pair(U, A) -> R0 = 0 224 ; A = U -> R0 = 0 225 ; composable_pairs(U, A, U0, V0) -> 226 subst_node([Ul->Ur], U0, V0, R, R0) 227 ; add_link(U, R, R1), 228 zdd_insert(A, R1, R0) 229 ), 230 zdd_join(L0, R0, Y) 231 ). 232 233 /************************* 234 * count_rect_path * 235 *************************/ 236 237% ?- N = 3, minato_r5(rect(0, N), C). 238% ?- N = 3, minato_r5(rect(1, N), C). 239% ?- N = 10, minato_r5(rect(1, N), C). 240% ?- minato_r5(rect(1,1), C, S). 241 242% ?- minato_r5(rect(1,1), C, S). 243% ?- minato_r5(rect(3,1), C, S). 244% ?- minato_r5(rect(2,2), C, S). 245% ?- minato_r5(rect(2,1), C, S). 246% ?- minato_r5(rect(3,1), C, S). 247% ?- minato_r5(rect(3,3), C, S). 248% ?- minato_r5(rect(4,4), C, S). 249% ?- call_with_time_limit(200, time(minato_r5(rect(8,8), C, _))). 250%@ % 908,479,618 inferences, 89.804 CPU in 91.150 seconds (99% CPU, 10116254 Lips) 251%@ C = 3266598486981642. 252% ?- trace. 253% ?- spy(node_one_by_one). 254% ?- minato_r5(rect(0,0), C). 255% ?- minato_r5(rect(1,0), C). 256% ?- minato_r5(rect(0,1), C). 257% ?- minato_r5(rect(1,1), C). 258% ?- minato_r5(rect(1,1), C, X). 259% ?- minato_r5(rect(1,1), C, _). 260% ?- minato_r5(rect(2,2), C, _). 261% ?- minato_r5(rect(3,3), C, _). 262% ?- minato_r5(rect(4,4), C, _). 263% ?- minato_r5(rect(5,5), C, _). 264% ?- minato_r5(rect(6,6), C, _). 265% ?- time(minato_r5(rect(2,2), C, _)). 266% ?- time(minato_r5(rect(9,9), C, _)). 267%@ % 3,992,214,479 inferences, 377.403 CPU in 379.840 seconds (99% CPU, 10578111 Lips) 268%@ C = 41044208702632496804. 269%@ % 3,992,214,479 inferences, 391.036 CPU in 394.074 seconds (99% CPU, 10209317 Lips) 270%@ C = 41044208702632496804. 271 272% ?- time(minato_r5(rect(10,10), C, _)). 273%@ % 18,246,128,207 inferences, 1826.781 CPU in 1842.135 seconds (99% CPU, 9988130 Lips) 274%@ C = 1568758030464750013214100. 275%@ % 18,246,106,192 inferences, 1871.297 CPU in 1889.274 seconds (99% CPU, 9750514 Lips) 276%@ C = 1568758030464750013214100. 277 278minato_r5(Rect, C):- minato_r5(Rect, C, _). 279 280% 281minato_r5(Rect, C, Opts):- 282 memberchk(out(X), Opts), 283 set_compare(compare), 284 set_key(rect, Rect), 285 rect_nodes(Rect, A), 286 sort(A, A1), 287 reverse(A1, B), 288 B =[Max-_|_], 289 arg(1, Max, K), 290 set_key(max, Max), 291 set_key(prune_index, K), 292 node_one_by_one(B, 1, X), 293 card(X, C). 294 295p(Opts):- subset([out(X)], Opts), 296 psa(X). 297 298% 299node_one_by_one([], X, X). 300node_one_by_one([P-En|R], X, X0):- 301 zdd_insert(P-P, X, XP), 302 add_node_one(P, En, XP, X1), 303 prune_inactive_node(P, X1, X2), 304 get_key(prune_index, I), 305 arg(1, P, J), 306 ( J = I -> X3 = X2 307 ; set_key(prune_index, J), 308 format("Slimming at ~w.\n", [P]), 309 zdd_gc(X2, X3) 310 ), 311 node_one_by_one(R, X3, X0). 312% 313is_max_node(P):- get_key(max, P). 314 315 316% ?- time(minato_r5(rect(1,1), C)). 317 318add_node_one(_, [], X, X):-!. 319add_node_one(P, [A], U, V):-!, add_links([P-A], U, V). 320add_node_one(P, [A, B], U, V):- add_links([P-A, P-B], U, V). 321 322% ?- active_node_orth(p(0,0),p(0,0)). % true (conentionally) 323% ?- active_node_orth(p(0,0),p(0,1)). 324% ?- active_node_orth(p(0,0),p(1,0)). 325% ?- active_node_orth(p(0,0),p(1,1)). 326% ?- active_node_orth(p(0,1),p(1,0)). % true. 327% ?- active_node_orth(p(0,1),p(1,1)). 328% ?- active_node_orth(p(1,0),p(1,1)). % true 329%% active_node_orth(P, Q) is true if Q is directly linked from some P' < P. 330 331active_node_orth(p(0, J), p(0, L)):-!, L = J. 332active_node_orth(p(I, J), p(I, L)):-!, J =< L. 333active_node_orth(p(I, J), p(K, L)):- K is I+1, !, L < J. 334 335% ?- rect_nodes(rect(10,10), Ns), findall(Q, ( member(P-_, Ns), 336% orth_skew(P, Q)), Sk), sort(Sk, SSk), 337% findall(active(U, V), (member(U, SSk), member(V, SSk), active_node_skew(U, V)), W), maplist(writeln, W), fail; true. 338 339% ?- active_node_skew(p(0,0), p(0, 0)). % true 340% ?- active_node_skew(p(0,0), p(0, 1)). % false (vacuously) 341% ?- active_node_skew(p(1,1), p(2, 1)). % true 342% ?- active_node_skew(p(1,0), p(1, 1)). % true 343% ?- active_node_skew(p(1,1), p(2, 2)). % false 344% ?- active_node_skew(p(1,1), p(2, 1)). % true. 345% ?- active_node_skew(p(1,0), p(2, 1)). % false 346% ?- active_node_skew(p(1,1), p(2, 0)). % true 347active_node_skew(p(I, J), p(I, L)):- !, J =< L. % Actually not ncessary clause ? 348active_node_skew(p(I, J), p(K, L)):- K is I + 1, 349 ( L = J -> J > 0 350 ; L < J 351 ). 352% 353prune_inactive_node(P, X, Y):- get_key(max, Max), 354 prune_inactive_node(P, X, Y, Max). 355 356% 357prune_inactive_node(_, X, X, _):- X<2, !. 358prune_inactive_node(P, X, Y, Max):- % memo is useless here 359 cofact(X, t(A, L, R)), 360 ( A = (_->_) -> Y = X 361 ; prune_inactive_node(P, L, L0, Max), 362 A = (U - V), 363 ( active_node(P, U) -> 364 ( ( active_node(P, V); V = Max ) -> 365 prune_inactive_node(P, R, R1, Max), 366 zdd_insert(A, R1, R0) 367 ; R0 = 0 368 ) 369 ; U = Max -> R0 = 0 370 ; U = V -> prune_inactive_node(P, R, R0, Max) 371 ; R0 = 0 372 ), 373 zdd_join(L0, R0, Y) 374 )