1:- module(add_node_by_one_one, []).    2
    3:- use_module(zdd('zdd-array')).    4:- use_module(zdd(zdd)).    5:- use_module(zdd('minato-r5')).    6:- use_module(pac(op)).    7
    8		/*******************
    9		*   Tiny helpers   *
   10		*******************/
   11
   12% ?- arrow_symbol(_->_, F).
   13% ?- arrow_symbol(a->b, F, X, Y).
   14arrow_symbol( _ -> _).
   15%
   16arrow_symbol(A, A0):- functor(A, A0, 2).
   17arrow_symbol(A, A0, A1, A2):- functor(A, A0, 2),
   18		arg(1, A, A1),
   19		arg(2, A, A2).
   20%
   21mate_less_than(_ - A, B -_):- A @< B.
   22
   23% One of the most basic helpers.
   24composable_pairs(A-B, A-C, B, C).
   25composable_pairs(A-B, C-A, B, C).
   26composable_pairs(B-A, A-C, B, C).
   27composable_pairs(B-A, C-A, B, C).
   28%
   29normal_pair(A-B, U-V):-!, ( B @< A -> U=B, V=A; U=A, V=B ).
   30normal_pair(A->B, U->V):- ( B @< A -> U=B, V=A; U=A, V=B ).
   31
   32
   33		/****************************************************
   34		*     replace_end/bypass:  Most basic operations.   *
   35		****************************************************/
   36
   37% ?- zdd X<< +[*[c-d]], subst_node([a->c], c, a, X, Y), psa(X), psa(Y).
   38
   39subst_node(_, _, _, X, 0, _):- X<2, !.
   40subst_node(Es, A, P, X, Y, S):-			% replace A with P
   41	cofact(X, t(U, L, R), S),
   42	arrow_symbol(U, Arrow, Lu, Ru),
   43	(	Arrow = (->) ->	Y = 0
   44	;	A @< Lu ->	Y = 0
   45	;	subst_node(Es, A, P, L, L0, S),
   46		(	Ru = A	->
   47			normal_pair(Lu-P, V),
   48			zdd_ord_insert([V|Es], R, R0, S)
   49		;	Lu = A	->
   50			normal_pair(Ru-P, V),
   51			zdd_ord_insert([V|Es], R, R0, S)
   52		;	subst_node(Es, A, P, R, R1, S),
   53			zdd_insert(U, R1, R0, S)
   54		),
   55		zdd_join(L0, R0, Y, S)
   56	).
   57
   58% ?- rect_nodes(rect(0,2), Ns).
   59% ?- rect_nodes(rect(10,10), Ns), length(Ns, L).
   60rect_nodes(rect(W, H), Ns):-
   61	findall(p(I,J),
   62			 (	between(0, W, I),
   63				between(0, H, J)
   64			 ),
   65			 Ns).
   66
   67% ?- rect_udg(rect(1,1), UDG).
   68% ?- rect_udg(rect(10,10), UDG),length(UDG, L).
   69rect_udg(rect(W, H), UDG):-
   70	findall( p(I,J)-Suc,
   71				 (	between(0, W, I),
   72					between(0, H, J),
   73					findall( p(K,L),
   74						(  L=J, K is I + 1, K =< W
   75						;  K=I, L is J + 1, L =< H
   76						),
   77						Suc)
   78				 ),
   79				 UDG).
   80
   81
   82% ?- rect_mate(rect(1,0), X, S), psa(X, S).
   83% ?- rect_mate(rect(1,0), X, S), psa(X, S).
   84% ?- rect_mate(rect(1,1), X, S), psa(X, S).
   85% ?- rect_mate(rect(2,2), X, S), psa(X, S), card(X, C, S).
   86% ?- rect_mate(rect(3,3), X, S), card(X, C, S).
   87% ?- rect_mate(rect(4,4), X, S), card(X, C, S).
   88% ?- rect_mate(rect(5,5), X, S), card(X, C, S).
   89% ?- time((rect_mate(rect(6,6), X, S), card(X, C, S))).
   90% ?- time((rect_mate(rect(7,7), X, S), card(X, C, S))).
   91% ?- time((rect_mate(rect(7,7), X, S), card(X, C, S))).
   92% ?- time((rect_mate(rect(8,8), X, S), card(X, C, S))).
   93%@ % 2,503,775,609 inferences, 232.253 CPU in 232.940 seconds (100% CPU, 10780371 Lips)
   94%@ X = 110190,
   95%@ S = ..,
   96%@ C =
   97
   98% ?- call_with_time_limit(2000, time((rect_mate(rect(9,9), X, S), card(X, C, S)))).
   99%@ % 11,947,268,675 inferences, 1053.032 CPU in 1057.017 seconds (100% CPU, 11345590 Lips)
  100%@ X = 377107,
  101%@ S = ..,
  102%@ C = 41044208702632496804.
  103
  104% ?- call_with_time_limit(36000, time((rect_mate(rect(10,10), X, S), card(X, C, S)))).
  105%@ GC at node  p(10,0)
  106%@ GC at node  p(9,0)
  107%@ GC at node  p(8,0)
  108%@ GC at node  p(7,0)
  109%@ GC at node  p(6,0)
  110%@ GC at node  p(5,0)
  111%@ GC at node  p(4,0)
  112%@ GC at node  p(3,0)
  113%@ GC at node  p(2,0)
  114%@ GC at node  p(1,0)
  115%@ GC at node  p(0,0)
  116%@ % 29,396,165,381 inferences, 3825.651 CPU in 3841.534 seconds (100% CPU, 7683964 Lips)
  117%@ X = 1268341,
  118%@ S = ..,
  119%@ C = 1568758030464750013214100.
  120
  121% [2022/10/01]
  122% ?- call_with_time_limit(36000, time((rect_mate(rect(11,11), X, S), card(X, C, S)))).
  123%@ GC at node  p(11,0)
  124%@ GC at node  p(10,0)
  125%@ GC at node  p(9,0)
  126%@ GC at node  p(8,0)
  127%@ GC at node  p(7,0)
  128%@ GC at node  p(6,0)
  129%@ GC at node  p(5,0)
  130%@ GC at node  p(4,0)
  131%@ GC at node  p(3,0)
  132%@ GC at node  p(2,0)
  133%@ GC at node  p(1,0)
  134%@ GC at node  p(0,0)
  135%@ % 129,787,391,715 inferences, 14036.125 CPU in 14092.162 seconds (100% CPU, 9246668 Lips)
  136%@ X = 4207535,
  137%@ S = ..,
  138%@ C = 182413291514248049241470885236.
  139
  140% ?- call_with_time_limit(500, time((rect_mate(rect(12,12), X, [slim(all)], S), card(X, C, S)))).
  141% ?- rect_mate(rect(3,3), X, [gc(0)], S), card(X, C, S).
  142% ?- rect_mate(rect(3,3), X, [gc(0)], S), card(X, C, S).
  143% ?- rect_mate(rect(3,3), X, [gc(all)], S), card(X, C, S).
  144% ?- rect_mate(rect(3,3), X, [], S), card(X, C, S).
  145% ?- rect_mate(rect(3,3), X, [gc(no)], S), card(X, C, S).
  146% ?- zdd rect_mate(rect(1,1), X, [gc(0)]), card(X, C).
  147% ?- zdd rect_mate(rect(2,2), X, [gc(0)]), card(X, C).
  148% ?- zdd rect_mate(rect(3,3), X, [gc(0)]), card(X, C).
  149
  150reverse_successors(X-A, X-B):- reverse(A, B).
  151
  152% slim(K);  slim(no); slim(all).
  153rect_mate(Rect, X, S):-rect_mate(Rect, X, [slim(0)], S).
  154
  155%
  156rect_mate(Rect, X, InOpts, S):-
  157	(	memberchk(gc(CtrlSlim), InOpts) -> true
  158	;	CtrlSlim= 0
  159	),
  160	Rect = rect(W,H),
  161	rect_udg(Rect, Dg0),
  162	maplist(reverse_successors, Dg0, Dg1),
  163	reverse(Dg1, Dg),
  164	fetch_state(S),
  165	set_key(max_node, p(W, H), S),
  166	udg_mate(CtrlSlim, Dg, 1, X0, S),
  167	get_key(max_node, Max, S),
  168	prune_final(p(0,0), Max, X0, X, S).
  169%
  170udg_mate(_, [], X, X, _).
  171udg_mate(Ctrl, [N-Ps|UDG], X, Y, S):-
  172	add_node(N, Ps, X, X0, S),
  173	get_key(max_node, Max, S),
  174	prune_by_classify_link(N, Max, X0, X1, S),
  175	ctrl_slim(Ctrl, N, X1, X2, S),
  176	udg_mate(Ctrl, UDG, X2, Y, S).
  177
  178%
  179ctrl_slim(all, P, X, Y, S):-!,
  180	format("GC at ~w \n", [P]),
  181	zdd_slim(X, Y, S),
  182	garbage_collect.
  183ctrl_slim(no, _, X, X, _):-!.
  184ctrl_slim(K, P, X, Y, S):-integer(K),
  185	P = p(_, J),
  186	(	J = K ->
  187		format("GC at ~w \n", [P]),
  188		zdd_slim(X, Y, S),
  189		garbage_collect
  190	;	Y = X
  191	).
  192
  193
  194% ?- zdd add_node(a, [], 1, X), psa(X).
  195% ?- zdd add_node(b, [], 1, X), add_node(a, [b], X, Y), psa(Y).
  196% ?- zdd add_node(b, [], 1, X), add_node(a, [b], X, Y),
  197%	add_node(c, [a,b], Y, Z), psa(Z).
  198
  199add_node(N, [], X, Y, S):-!, zdd_insert(N-N, X, Y, S).
  200add_node(N, [P|Ps], X, Y, S):- normal_pair(N->P, Q),
  201	subst_node([Q], P, N, X, X0, S),
  202	zdd_insert(N-N, X, X1, S),
  203	zdd_join(X0, X1, X2, S),
  204	add_neighbor_links(N, Ps, X2, Y, S).
  205%
  206add_neighbor_links(_, [], X, X, _):-!.
  207add_neighbor_links(N, [P|Ps], X, Y, S):- normal_pair(N-P, Link),
  208	add_link(Link, X, X0, S),
  209	zdd_join(X0, X, X1, S),
  210	add_neighbor_links(N, Ps, X1, Y, S).
  211
  212% ?- zdd X<<{[a-b, c-d]}, psa(X), add_link(b-c, X, Y), psa(Y).
  213% ?- zdd X<< +[[a-b, c-d], [e-f]], psa(X), add_link(b-c, X, Y), psa(Y).
  214% ?- zdd X<< +[[a-b, c-d], [a-a, b-b], [e-f]], psa(X), add_link(b-c, X, Y), psa(Y).
  215% ?- zdd X<< +[*[a-a, b-b, c-c]], psa(X), add_link(b-c, X, Y), psa(Y).
  216
  217add_link(_, X, 0, _):- X<2, !.
  218add_link(U, X, Y, S):- % memo is useless here
  219	cofact(X, t(A, L, R), S),
  220	(	A = (_->_) -> Y = 0
  221	;	add_link(U, L, L0, S),
  222		U = Ul-Ur,
  223		(	mate_less_than(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, S)
  227		;	add_link(U, R, R1, S),
  228			zdd_insert(A, R1, R0, S)
  229		),
  230		zdd_join(L0, R0, Y, S)
  231	).
  232
  233% ?- zdd X<< +[*[a-b, a->b]], prune_final(a, b, X, Y), psa(Y).
  234prune_final(_, _, X, X, _):- X<2, !.
  235prune_final(P, Q, X, Y, S):- cofact(X, t(A, L, R), S),
  236	(	A = (_->_) -> Y = X
  237	;	prune_final(P, Q, L, L0, S),
  238		A = A1-A2,
  239		(	 A1 = P ->
  240			 (	A2 = Q
  241			 -> prune_final(P, Q, R, R0, S)
  242			 ;	R0 = 0
  243			 )
  244		;	A1 = A2 ->
  245			prune_final(P, Q, R, R0, S)
  246		;	R0 = 0
  247		),
  248		zdd_join(L0, R0, Y, S)
  249	).
  250
  251
  252% ?- classify_link(p(0,1), p(3,3), p(1,0)-p(3,3), X).
  253% ?- classify_link(p(0,1), p(3,3), p(0,2)-p(3,3), X).
  254% ?- classify_link(p(0,1), p(3,3), p(0,1)-p(3,3), X).
  255classify_link(_, _, _->_, id):-!.
  256classify_link(P, End, A-B,  Case):- on_frontier(P, A), !,
  257   	(	on_frontier(P, B) -> Case = keep
  258	;	B = End -> Case = keep
  259	;	Case = 0
  260	).
  261classify_link(_, _, A-A, ignore):-!.
  262classify_link(_, _, _, 0).
  263%
  264on_frontier(p(0, J), p(0, J)):-!.
  265on_frontier(p(0, J), p(K, L)):-!, K = 1, L< J.
  266on_frontier(p(I, J), p(I, K)):-  K >= J, !.
  267on_frontier(p(I, J), p(I0, K)):- I0 is I + 1, K < J.
  268%
  269prune_by_classify_link(_, _, X, X, _):- X<2, !.
  270prune_by_classify_link(P, End, X, Y, S):- cofact(X, t(A, L, R), S),
  271	classify_link(P, End, A, Case),
  272	(	Case = id ->   Y = X
  273	;  	prune_by_classify_link(P, End, L, L0, S),
  274		(	Case = keep ->
  275			prune_by_classify_link(P, End, R, R1, S),
  276			zdd_insert(A, R1, R0, S)
  277		;	Case = ignore ->
  278			prune_by_classify_link(P, End, R, R0, S)
  279		;	R0 = 0
  280		),
  281		zdd_join(L0, R0, Y, S)
  282	)