1:- module(minato_r4, []). 2 3% ( Revision of copy of minato-r2) 4 5:- use_module(util(math)). 6:- use_module(util(meta2)). 7:- use_module(pac(basic)). 8:- use_module(pac(meta)). 9:- use_module(util(misc)). 10:- use_module(pac('expand-pac')). 11:- use_module(zdd('zdd-array')). 12:- use_module(zdd(zdd)). 13:- use_module(zdd('zdd-misc')). 14:- use_module(zdd('zdd-plain')). 15:- use_module(pac(op)). 16:- op(1060, xfy, #). % exor 17:- op(1000, xfy, &). 18 19% term_expansion --> pac:expand_pac. 20term_expansion --> expand_pac. 21 22 /****************** 23 * Switches * 24 ******************/ 25% ORTHOGONAl 26% active_node(X, Y):- active_node_orth(X, Y). 27% rect_nodes(X, Y):- rect_nodes_orth(X, Y). 28 29% SKEW. 30active_node(X, Y):- active_node_skew(X, Y). 31rect_nodes(X, Y):- rect_nodes_skew(X, Y). 32 33% ?- count_rect_path(rect(0,0), C). 34% ?- count_rect_path(rect(1,0), C). 35% ?- count_rect_path(rect(0,1), C). 36% ?- count_rect_path(rect(1,1), C). 37% ?- count_rect_path(rect(1,2), C). 38% ?- count_rect_path(rect(2,1), C). 39% ?- count_rect_path(rect(2,2), C). 40% ?- count_rect_path(rect(1,10), C). 41% ?- count_rect_path(rect(10,1), C). 42% ?- count_rect_path(rect(100,1), C). 43% ?- count_rect_path(rect(1,100), C). 44% ?- time(count_rect_path(rect(6,6), C)). 45%@ % 28,666,943 inferences, 2.073 CPU in 2.107 seconds (98% CPU, 13827602 Lips) 46%@ C = 575780564. 47%@ % 25,642,240 inferences, 3.558 CPU in 4.465 seconds (80% CPU, 7207373 Lips) 48%@ C = 575780564. 49% ?- time(count_rect_path(rect(7,7), C)). 50 51%@ % 128,031,121 inferences, 10.589 CPU in 10.664 seconds (99% CPU, 12090872 Lips) 52%@ C = 789360053252. 53%@ % 106,041,498 inferences, 12.348 CPU in 12.454 seconds (99% CPU, 8587850 Lips) 54%@ C = 789360053252. 55 56% [2022/08/10] cleanup old hash vector element with 0 57% ?- time(count_rect_path(rect(8,8), C)). 58 59%@ % 597,174,366 inferences, 66.803 CPU in 67.310 seconds (99% CPU, 8939312 Lips) 60%@ C = 3266598486981642. 61%@ % 597,174,366 inferences, 64.201 CPU in 64.572 seconds (99% CPU, 9301613 Lips) 62%@ C = 3266598486981642. 63%@ % 597,174,366 inferences, 59.440 CPU in 59.864 seconds (99% CPU, 10046731 Lips) 64%@ C = 3266598486981642. 65%@ % 608,401,418 inferences, 66.125 CPU in 66.439 seconds (100% CPU, 9200834 Lips) 66%@ C = 3266598486981642. 67%@ % 608,401,418 inferences, 60.675 CPU in 61.180 seconds (99% CPU, 10027244 Lips) 68%@ C = 3266598486981642. 69% [2022/08/10] 70%@ % 597,174,366 inferences, 59.526 CPU in 59.907 seconds (99% CPU, 10032085 Lips) 71%@ C = 3266598486981642. 72% ?- time(count_rect_path(rect(8,8), C)). 73%@ % 572,042,195 inferences, 54.849 CPU in 55.453 seconds (99% CPU, 10429344 Lips) 74%@ C = 3266598486981642. 75%@ % 436,367,556 inferences, 52.415 CPU in 52.981 seconds (99% CPU, 8325235 Lips) 76%@ C = 3266598486981642. 77% ?- time(count_rect_path(rect(9,9), C)). 78%@ % 2,028,259,194 inferences, 194.275 CPU in 195.632 seconds (99% CPU, 10440121 Lips) 79%@ C = 2449629600675855540670. 80 81% ?- call_with_time_limit(1800, time(count_rect_path(rect(10,10), C))). 82%@ % 12,006,266,932 inferences, 1229.766 CPU in 1239.202 seconds (99% CPU, 9763047 Lips) 83%@ C = 1568758030464750013214100, 84%@ S = [state(..), out(3998810)|_]. 85%@ % 12,782,653,306 inferences, 1164.030 CPU in 1174.499 seconds (99% CPU, 10981375 Lips) 86%@ C = 1568758030464750013214100, 87 88% ?- call_with_time_limit(36000, time(count_rect_path(rect(11,11), C))). 89%@ C = 182413291514248049241470885236. 90 91% ?- call_with_time_limit(36000, time(count_rect_path(rect(12,12), C))).
convert_skew(p(1,1), Q), convert_skew(P, Q), convert_skew(P, R).
@ Q = R, R = p(2, 1),
@ P = p(1, 1).100orth_skew(p(I, J), Y):- var(Y), !, 101 Y = p(K, I), 102 K is I + J. 103orth_skew(p(I, J), p(K, I)):- J is K - I. 104 105% ?- arrow_symbol(_->_, F). 106% ?- arrow_symbol(a->b, F, X, Y). 107atmark(X):- functor(X, @, 2). 108change_symbol(A-B, A->B). 109arrow_symbol( _ -> _). 110arrow_symbol(A, A0):- functor(A, A0, 2). 111arrow_symbol(A, A0, A1, A2):- functor(A, A0, 2), 112 arg(1, A, A1), 113 arg(2, A, A2). 114% 115is_link(->(_, _)). 116% 117convert_normal_pair(P, Q):- orth_skew_pair(P, Q0), 118 normal_pair(Q0, Q). 119% 120normal_arrow(X, Y):- @(normal_arrow(X, Y)). 121% 122normal_arrow(A->B, Arr):-!, 123 ( zdd_compare(>, A, B) -> Arr = (B->A) 124 ; Arr = (A->B) 125 ). 126normal_arrow(A-B, Arr):-normal_arrow(A->B, Arr). 127% 128 129lt_pair(_-A, B -_):- zdd_compare(<, A, B). 130 131 132 /************************************* 133 * basics of incrementing DG * 134 *************************************/ 135 136composable_pairs(A-B, A-C, B, C). 137composable_pairs(A-B, C-A, B, C). 138composable_pairs(B-A, A-C, B, C). 139composable_pairs(B-A, C-A, B, C). 140% 141normal_pair(A-B, B-A):- zdd_compare(>, A, B), !. 142normal_pair(A->B, B->A):- zdd_compare(>, A, B), !. 143normal_pair(P, P). 144 145% ?- orth_skew_pair(p(1,1)-p(2,2), X), orth_skew_pair(Y, X). 146%@ X = p(2, 1)-p(4, 2), 147%@ Y = p(1, 1)-p(2, 2). 148orth_skew_pair(P, Q):- 149 ( P = (A-B) -> Q = (A0-B0) 150 ; P = (A->B), 151 Q = (A0->B0) 152 ), 153 orth_skew(A, A0), 154 orth_skew(B, B0). 155 156link_sort_opp(X, Y):- sort(X, X0), reverse(X0, Y). 157 158% ?- node_ends(p(0,0), En, rect(1,1)). 159% ?- node_ends(p(0,0), En, rect(0,0)). 160% ?- node_ends(p(1,1), En, rect(2,2)). 161 162node_ends(P, En, rect(W,H)):- P = p(I,J), 163 ( I < W -> 164 K is I + 1, 165 En0 = [p(K,J)] 166 ; En0 = [] 167 ), 168 ( J < H -> 169 L is J + 1, 170 En = [p(I, L)|En0] 171 ; En = En0 172 ). 173 174% ?- node_ends_skew(p(0,0), En, rect(1,1)). 175% ?- node_ends_skew(p(0,0), En, rect(0,0)). 176% ?- node_ends_skew(p(1,1), En, rect(2,2)). 177% ?- node_ends_skew(p(1,1), En, rect(1,2)). 178node_ends_skew(P, En, rect(W,H)):- P = p(I,J), 179 ( J < W -> 180 K is J + 1, 181 M is I + 1, 182 En0 = [p(M, K)] 183 ; En0 = [] 184 ), 185 ( I < H + J -> 186 L is I + 1, 187 En = [p(L, J)|En0] 188 ; En = En0 189 ). 190 191% ?- R=rect(2,2), repeat(in_rect(P, R), 192% (node_ends_shadows(P, En, Sh, R), writeln(P-En-Sh))). 193in_rect(p(I, J), rect(W, H)):- between(0, W, I), between(0, H, J). 194 195% ?- rect_nodes_orth(rect(1,1), PES), maplist(writeln, PES). 196% ?- rect_nodes_orth(rect(3,3), PES), maplist(writeln, PES). 197% ?- rect_nodes_orth(rect(10,10), PES), maplist(writeln, PES). 198% ?- rect_nodes_orth(rect(30,30), PES), length(PES, L). 199% ?- rect_nodes_orth(rect(100,100), PES), length(PES, L). 200% ?- time((rect_nodes_orth(rect(1000,1000), PES), length(PES, L))). 201 202rect_nodes_orth(R, PES):- 203 findall(P-E, (in_rect(P, R), node_ends(P, E, R)), PES). 204 205% ?- rect_nodes_skew(rect(100,100), PES), length(PES, L). 206% ?- time((rect_nodes_skew(rect(1000,1000), PES), length(PES, L))). 207rect_nodes_skew(R, PES_skew):- rect_nodes_orth(R, PES_orth), 208 convert_orth_skew(PES_orth, PES_skew). 209% 210convert_orth_skew([], []). 211convert_orth_skew([A-B|C], [A0-B0|C0]):- 212 orth_skew(A, A0), 213 maplist(orth_skew, B, B0), 214 convert_orth_skew(C, C0). 215 216 217 /**************************************************** 218 * replace_end/bypass: Most basic operations. * 219 ****************************************************/ 220 221% ?- zdd((X<<{[c-d]}, @(subst_node([a->c], c, a, X, Y)), psa(X), psa(Y))). 222subst_node(_, _, _, X, 0):- X < 2, !. 223subst_node(Es, A, P, X, Y):- get_key(max, Max), A==Max, !, 224 subst_max_node(Es, Max, P, X, Y). 225subst_node(Es, A, P, X, Y):- % memo is useless here 226 /* replace A with P */ 227 cofact(X, t(U, L, R)), 228 arrow_symbol(U, Arrow, Lu, Ru), 229 ( Arrow = (->) -> Y = 0 230 ; zdd_compare(<, A, Lu) -> Y = 0 231 ; subst_node(Es, A, P, L, L0), 232 ( Ru = A -> 233 normal_pair(Lu-P, V), 234 zdd_ord_insert([V|Es], R, R0) 235 ; Lu = A -> 236 normal_pair(Ru-P, V), 237 zdd_ord_insert([V|Es], R, R0) 238 ; subst_node(Es, A, P, R, R1), 239 zdd_insert(U, R1, R0) 240 ), 241 zdd_join(L0, R0, Y) 242 ). 243 244% ?- count_rect_path(rect(8,8), C). 245 246% ?- zdd((X<<{[c-c]}, @(subst_max_node([], c, b, X, Y)), psa(Y))). 247% ?- zdd((X<<{[a-b]}, @(subst_max_node([], c, b, X, Y)), psa(Y))). 248% ?- zdd((X<<{[a-b, c-c]}, @(subst_max_node([], c, d, X, Y)), psa(Y))). 249 250subst_max_node(_, _, _, X, 0):- X < 2, !. 251subst_max_node(Es, Max, P, X, Y):- /* replace Max with P */ 252 cofact(X, t(U, L, R)), 253 arrow_symbol(U, Arrow, Lu, Ru), 254 ( Arrow = (->) -> Y = 0 255 ; subst_max_node(Es, Max, P, L, L0), 256 ( Max @=< Lu -> 257 zdd_ord_insert([P-Max|Es], R, R0) 258 ; Max @=< Ru -> R0 = 0 259 ; subst_max_node(Es, Max, P, R, R1), 260 zdd_insert(U, R1, R0) 261 ), 262 zdd_join(L0, R0, Y) 263 ). 264 265% ?- zdd((X<<{[a-b, c-d]}, @(bypass_via_node(b-c, X, Y)), psa(X), psa(Y))). 266bypass_via_node(E, X, Y):- bypass_via_node([], E, X, Y). 267 268% ?- zdd((X<<{[a-b, c-d]}, @(bypass_via_node([b->c], b-c, X, Y)), psa(X), psa(Y))). 269bypass_via_node(_, _, X, 0):- X < 2,!. 270bypass_via_node(Bypass, E, X, Y):- % memo is useless here 271 cofact(X, t(P, L, R)), 272 ( P = (_->_) -> Y = 0 273 ; lt_pair(E, P) -> Y = 0 274 ; bypass_via_node(Bypass, E, L, L0), 275 ( E = P -> R0 = 0 276 ; composable_pairs(E, P, U, V) -> 277 subst_node(Bypass, U, V, R, R0) 278 ; bypass_via_node(Bypass, E, R, R1), 279 zdd_insert(P, R1, R0) 280 ), 281 zdd_join(L0, R0, Y) 282 ). 283 284 /************************* 285 * count_rect_path * 286 *************************/ 287 288% ?- test(rect(1,1), Y). 289test(X, Y):- count_rect_path(X, Y, _, _). 290 291% ?- N = 3, count_rect_path(rect(0, N), C). 292% ?- N = 3, count_rect_path(rect(1, N), C). 293% ?- N = 10, count_rect_path(rect(1, N), C). 294% ?- count_rect_path(rect(3,1), C). 295% ?- count_rect_path(rect(2,2), C). 296% ?- count_rect_path(rect(3,3), C). 297% ?- count_rect_path(rect(4,4), C). 298 299% ?- call_with_time_limit(200, time(count_rect_path(rect(8,8), C, _))). 300%@ % 908,479,618 inferences, 89.804 CPU in 91.150 seconds (99% CPU, 10116254 Lips) 301%@ C = 3266598486981642. 302 303% ?- count_rect_path(rect(1,1), C). 304% ?- count_rect_path(rect(1,1), C, X). 305% ?- count_rect_path(rect(1,1), C, X), psa(X). 306% ?- count_rect_path(rect(2,2), C, X), psa(X). 307 308count_rect_path(Rect, C):- count_rect_path(Rect, C, _). 309% 310count_rect_path(Rect, C, Opts):- 311 memberchk(out(X), Opts), 312 set_key(rect, Rect), 313 rect_nodes(Rect, A), 314 sort(A, A1), 315 reverse(A1, B), 316 B =[Max-_|_], 317 set_key(max, Max), 318 arg(1, Max, K), 319 set_key(prune_index, K), 320 node_one_by_one(B, 1, X), 321 card(X, C). 322 323% ?- count_rect_path(rect(0,0), C). 324% ?- count_rect_path(rect(0,1), C). 325% ?- count_rect_path(rect(1,0), C). 326% ?- count_rect_path(rect(1,1), C). 327% ?- count_rect_path(rect(1,2), C). 328% ?- count_rect_path(rect(100,1), C). 329% ?- count_rect_path(rect(2,1), C). 330% ?- count_rect_path(rect(2,2), C). 331% ?- count_rect_path(rect(2,3), C). 332% ?- count_rect_path(rect(3,2), C). 333% ?- count_rect_path(rect(3,3), C). 334% ?- count_rect_path(rect(4,4), C). 335% ?- count_rect_path(rect(5,5), C). 336% ?- count_rect_path(rect(6,6), C). 337% ?- count_rect_path(rect(7,7), C). 338% ?- count_rect_path(rect(8,8), C). 339% ?- time(count_rect_path(rect(9,9), C)). 340 341%@ % 2,028,259,251 inferences, 179.414 CPU in 180.716 seconds (99% CPU, 11304895 Lips) 342%@ C = 2449629600675855540670, 343%@ S = [state(..), out(271190)|_]. 344 345%@ % 2,763,116,175 inferences, 246.356 CPU in 248.711 seconds (99% CPU, 11215959 Lips) 346%@ C = 41044208702632496804, 347%@ S = [state(..), out(980774)|_]. 348 349node_one_by_one([], X, X). 350node_one_by_one([P-En|R], X, Y):- 351 writeln(P), 352 add_node_one(P, En, X, Z), 353 get_key(max, Max), 354 prune_inactive_node(P, Z, U, Max), 355 get_key(prune_index, I), 356 arg(1, P, J), 357 ( J = I -> U0 = U 358 ; set_key(prune_index, J), 359 writeln("Slimming..."), 360 zdd_gc(U, U0), 361 garbage_collect 362 ), 363 node_one_by_one(R, U0, Y). 364 365 366% ?- zdd((X<<{[b-c, b->c]}, psa(X), 367% @(add_node_one(a, [b], X, Y)), psa(Y))). 368% ?- time(count_rect_path(rect(8,8), C, S)). 369%@ % 608,835,325 inferences, 54.280 CPU in 54.650 seconds (99% CPU, 11216634 Lips) 370%@ C = 3266598486981642, 371%@ S = [state(..), out(238658)|_]. 372 373%@ % 436,367,556 inferences, 35.323 CPU in 36.801 seconds (96% CPU, 12353625 Lip 374%@ C = 3266598486981642, 375%@ S = [state(..), out(4921865)|_]. 376 377% ?- time(count_rect_path(rect(1,1), C, S)). 378add_node_one(P, [], X, Y):-!, zdd_insert(P-P, X, Y). 379add_node_one(P, [A], X, Y):-!, 380 subst_node([P->A], A, P, X, Y0), 381 zdd_insert(P-P, X, Y1), 382 zdd_join(Y0, Y1, Y). 383add_node_one(P, [A, B], X, Y):- 384 subst_node([P->A], A, P, X, Y0), 385 subst_node([P->B], B, P, X, Y1), 386 bypass_via_node([P->A, P->B], B-A, X, Y2), 387 zdd_insert(P-P, X, Y3), 388 zdd_join_list([Y0, Y1, Y2, Y3], Y). 389 390% ?- zdd((X<<{[p(1)-p(2)]}, @(prune_inactive_node(p(1), X, Y, p(2))))). 391% ?- zdd((X<<{[p(1)-p(2)]}, @(prune_inactive_node(p(0), X, Y, p(3))))). 392% ?- zdd((X<<{[p(1)-p(2), p(3)-p(4)]}, @(prune_inactive_node(p(2), X, Y, p(5))))). 393% ?- zdd((X<<{[p(1)-p(5), p(3)-p(4)]}, @(prune_inactive_node(p(2), X, Y, p(5))))). 394% ?- zdd((X<<{[p(1)-p(5)], [p(3)-p(4)]}, @(prune_inactive_node(p(2), X, Y, p(5))), psa(Y))). 395% ?- zdd((X<<{[p(1)-p(5), p(2)-p(2)]}, @(prune_inactive_node(p(2), X, Y, p(5))), psa(Y))). 396% ?- zdd((X<<{[p(1)-p(4), p(5)-p(5)]}, @(prune_inactive_node(p(2), X, Y, p(5))), psa(Y))). 397% ?- zdd((X<<{[p(1)-p(4)], [p(5)-p(5)]}, @(prune_inactive_node(p(2), X, Y, p(5))), psa(Y))). 398% ?- zdd((X<<{[p(1)-p(4)], [p(5)-p(5)]}, @(prune_inactive_node(p(5), X, Y, p(5))), psa(Y))). 399 400% ?- count_rect_path(rect(10, 1), C, S). 401% ?- count_rect_path(rect(1,1), C, S). 402% ?- R=rect(1,1), findall(on(P,Q), (in_rect(P, R), in_rect(Q, R), active_node(P, Q)), S), 403% maplist(writeln, S). 404 405% ?- R=rect(10,10), findall(on(P,Q), (in_rect(P, R), in_rect(Q, R), 406% active_node(P, Q)), S), 407% maplist(writeln, S), fail; true. 408 409% ?- active_node_orth(p(0,0),p(0,0)). % true (conentionally) 410% ?- active_node_orth(p(0,0),p(0,1)). 411% ?- active_node_orth(p(0,0),p(1,0)). 412% ?- active_node_orth(p(0,0),p(1,1)). 413% ?- active_node_orth(p(0,1),p(1,0)). % true. 414% ?- active_node_orth(p(0,1),p(1,1)). 415% ?- active_node_orth(p(1,0),p(1,1)). % true 416%% active_node_orth(P, Q) is true if Q is directly linked from some P' < P. 417 418active_node_orth(p(0, J), p(0, L)):-!, L = J. 419active_node_orth(p(I, J), p(I, L)):-!, J =< L. 420active_node_orth(p(I, J), p(K, L)):- K is I+1, !, L < J. 421 422% ?- rect_nodes(rect(10,10), Ns), findall(Q, ( member(P-_, Ns), 423% orth_skew(P, Q)), Sk), sort(Sk, SSk), 424% findall(active(U, V), (member(U, SSk), member(V, SSk), active_node_skew(U, V)), W), maplist(writeln, W), fail; true. 425 426% ?- active_node_skew(p(0,0), p(0, 0)). % true 427% ?- active_node_skew(p(0,0), p(0, 1)). % false (vacuously) 428% ?- active_node_skew(p(1,1), p(2, 1)). % true 429% ?- active_node_skew(p(1,0), p(1, 1)). % true 430% ?- active_node_skew(p(1,1), p(2, 2)). % false 431% ?- active_node_skew(p(1,1), p(2, 1)). % true. 432% ?- active_node_skew(p(1,0), p(2, 1)). % false 433% ?- active_node_skew(p(1,1), p(2, 0)). % true 434active_node_skew(p(I, J), p(I, L)):- !, J =< L. % Actually not ncessary clause ? 435active_node_skew(p(I, J), p(K, L)):- K is I + 1, 436 ( L = J -> J > 0 437 ; L < J 438 ). 439% 440prune_inactive_node(_, X, X, _):- X<2, !. 441prune_inactive_node(P, X, Y, Max):- % memo is useless here 442 cofact(X, t(A, L, R)), 443 ( A = (_->_) -> Y = X 444 ; prune_inactive_node(P, L, L0, Max), 445 A = (U - V), 446 ( active_node(P, U) -> 447 ( ( active_node(P, V); V = Max ) -> 448 prune_inactive_node(P, R, R1, Max), 449 zdd_insert(A, R1, R0) 450 ; R0 = 0 451 ) 452 ; U = Max -> R0 = 0 453 ; U = V -> prune_inactive_node(P, R, R0, Max) 454 ; R0 = 0 455 ), 456 zdd_join(L0, R0, Y) 457 )