1:- module(update_link, [
    2		links_across/4, links_across/5, links_across/6
    3	,	link_across_out/6, link_across_in/6
    4	,	merge_blocks/5
    5	,	card_hybrid/3, card_hybrid/4
    6	,	mortal_paths/3, mortal_paths/4, mortal/2
    7	,	replace_right/6, replace_left/6
    8	,   atmark/1, qp_connect/4
    9	,	repeat_update_mqp/3, repeat_update_mqp/4
   10	,	u_repeat_update_mqp/3, u_repeat_update_mqp/4
   11	,	update_link/3, update_link/4
   12	,	update_mqp/3, update_mqp/4, update_qp/3, update_qp/4
   13	,	u_update_qp/3, u_update_qp/4
   14	,	normal_pair/2, normal_pair/3
   15	,	update_links/3, update_links/4
   16	,	update_link_slim/3, update_link_slim/4
   17	,	update_links_slim/3, update_links_slim/4
   18	,	slim_mqp/3, slim_mqp/4
   19						]).   20:- use_module(util(math)).   21:- use_module(util(meta2)).   22:- use_module(pac(basic)).   23:- use_module(pac(meta)).   24:- use_module(util(misc)).   25:- use_module(pac('expand-pac')).   26:- use_module(zdd('zdd-array')).   27:- use_module(zdd(zdd)).   28:- use_module(zdd('zdd-misc')).   29:- use_module(zdd('zdd-plain')).   30:- use_module(pac(op)).   31
   32:- op(1060, xfy, #).		% exor
   33:- op(1000, xfy, &).   34
   35term_expansion --> pac:expand_pac.
   36
   37% ?- zdd0((X<<pow([a,b]),  psa(X))).
   38% ?- q_compare(C, p(1, 1), p(0, 0)).
   39% ?- predsort(q_compare, [a->b, c-c, b], X).
   40% ?- predsort(q_compare, [a->b, c-d], X).
   41% ?- zdd0(zdd_sort([p(0,0), p(1,1)], X)).
   42% ?- zdd(zdd_sort([p(0,0), p(1,1)], X)).
   43% ?- zdd((set_compare(opp_compare), zdd_sort([p(1,0)->p(0,0), p(1,1)->p(0,1)], X))).
   44is_normal_order(S):- get_compare(F, S),	!, call(F, <, 1, 2).
   45
   46q_compare_layer(C, I-_, J-_):- compare(C, I, J).
   47%
   48q_compare_layer_opp(C, I-_, J-_):- compare(C, J, I).
   49%
   50succ_opp(I, J):- succ(J, I).
   51
   52% ?- predsort(q_compare, [a->b, 1, c-b, b->a, 2, b-c], X).
   53q_compare(C, X->Y, U->V):-!, compare(C, (X,Y), (U, V)).
   54q_compare(>, _->_, _-_):-!.
   55q_compare(<, _-_, _->_):-!.
   56q_compare(C, A, B):-compare(C, B, A).
   57
   58% ?- t_compare(C, p(0, 1), p(1,0)).
   59% ?- predsort(t_compare, [p(1,1), p(0,0), p(1,0), p(0,1), p(0,0)], L).
   60t_compare(=,  X, X):-!.
   61t_compare(C, p(I, J), p(L, M)):-  A is I+J,
   62	B is L + M,
   63	compare(C0, A, B),
   64	(	C0 = (=) -> compare(C, I, L)
   65	;	C = C0
   66	).
   67
   68% ?- convert_skew(p(1,2), X).
   69convert_skew(p(I, J), p(K, I)):- K is I + J.
   70
   71% ?- X = p(1, 2), ortho_skew(X, Y), ortho_skew(Z, Y), ortho_skew(Z, U).
   72%@ X = Z, Z = p(1, 2),
   73%@ Y = U, U = p(3, 1).
   74ortho_skew(P, Q):-
   75	(	nonvar(P)
   76	->  P = p(I, J),
   77		L is I + J,
   78		Q = p(L, I)
   79	;	Q = p(L, I),
   80		J is L - I,
   81		P = p(I, J)
   82	).
   83
   84% ?- udg(normal_pair(p(1,1)-p(0,1), X)).
   85% ?- rect_dg(rect(1,1), X, Y), convert_skew_udg(X, Y, Z, U),
   86%	udg((zdd_sort(Z, Z0),
   87%		maplist(normal_pair, U, U0), zdd_sort(U0, U1))),
   88%	writeln(U1), length(Y, LY),
   89%	length(U, LU), length(U0, LU0).
   90
   91% ?- rect_dg(rect(1,1), X, Y), convert_skew_udg(X, Y, Z, U),
   92%	zdd((zdd_sort(Z, Z0),
   93%		maplist(normal_pair, U, U0), zdd_sort(U0, U1))),
   94%	writeln(U1), length(Y, LY),
   95%	length(U, LU), length(U0, LU0).
   96
   97% ?- zdd((rect_dg_in_skew_axis(rect(1,1), N, L))).
   98% ?- udg((rect_dg_in_skew_axis(rect(1,1), N, L))).
   99% ?- zdd0((rect_dg_in_skew_axis(rect(1,1), N, L))).
  100% ?- zdd((rect_dg_in_skew_axis(rect(1,1), N, L))).
  101% ?- udg((rect_dg_in_skew_axis(rect(1,1), N, L))).
  102% ?- udg((rect_dg_in_skew_axis(rect(0,0), N, L))).
  103% ?- udg((rect_dg_in_skew_axis(rect(1,0), N, L))).
  104% ?- udg((rect_dg_in_skew_axis(rect(1,1), N, L))).
  105% ?- udg((rect_dg_in_skew_axis(rect(10,10), N, L))).
  106% ?- time(udg((rect_dg_in_skew_axis(rect(100,100), N, L)))).
  107
  108rect_dg_in_skew_axis(R, Ns, Ls):- @(rect_dg_in_skew_axis(R, Ns, Ls)).
  109%
  110rect_dg_in_skew_axis(R, Ns, Ls, S):-
  111	rect_dg(R, X, Y),
  112	convert_skew_udg(X, Y, Z, U),
  113	zdd_sort(Z, Ns, S),
  114	maplist(pred(S, [A, B]:- normal_pair(A, B, S)), U, U0),
  115	zdd_sort(U0, Ls, S).
  116%
  117convert_skew_udg(X, Y, Z, U):-
  118	maplist(convert_skew, X, Z),
  119	maplist(pred(([A-B, C-D]:- convert_skew(A, C), convert_skew(B, D))),
  120				 Y, U).
  121
  122% ?- v_compare(C, p(0, 1), p(1,0)).
  123% ?- predsort(t_compare, [p(1,1), p(0,0), p(1,0), p(0,1), p(0,0)], L).
  124v_compare(C, p(I, J), p(L, M)):- compare(C0, I, L),
  125	(	C0 = (=) -> compare(C, J, M)
  126	;	C = C0
  127	).
  128% ?- ht_compare(C, p(0,0)-p(1,0),p(0,0)-p(0,1)).
  129% ?- predsort(ht_compare, [p(0,0)-p(1,0),p(0,0)-p(0,1)], L).
  130ht_compare(C, P-Q, U-V):- t_compare(C0, P, U),
  131	(	C0 = (=) -> t_compare(C, Q, V)
  132	;	C = C0
  133	).
  134
  135touch(A - _, _-A).
  136touch(_ - A, A-_).
  137
  138qp_connect(A-B, U-A, B-V, U-V):-!.
  139qp_connect(A-B, B-V, U-A, U-V).
  140
  141change_symbol(A-B, A->B).
  142
  143minus_symbol(_-_).
  144
  145% ?- check_node_boole(2, [1,2,3]).
  146% ?- check_node_boole(b, b-c; d-b).
  147% ?- check_node_boole(a, \+[b,c]).
  148% ?- check_node_boole(a, [b,a,c]).
  149% ?- check_node_boole(a, \+[b,a,c]).  % false
  150% ?- check_node_boole(a, (\+[b,c]; [b,c])).
  151% ?- check_node_boole(a, ([b,a,c], [d, a, e])).
  152% ?- check_node_boole(a, \+(([b,a,c], [d, a, e]))). % false
  153% ?- time(repeat(1000000, check_node_boole(a, \+(([b,c]; [d, e]))))).
  154% ?- time((between(1, 1000000,_), check_node_boole(a, \+(([b,c]; [d, e]))))).
  155% ?- time(repeat(1000000, check_boole_node(\+(([b,c]; [d, e])), a))).
  156% ?- time(repeat(1000000, check_node_boole_(a, \+(([b,c]; [d, e]))))).
  157
  158% ?- repeat(10000, write(.)).
  159check_node_boole(X, Boole):- check_boole_node(Boole, X).
  160
  161%
  162check_boole_node(>=(I), X):-!, I @=< X.
  163check_boole_node(=<(I), X):-!, X @=< I.
  164check_boole_node(I-J, X):-!, I @=< X, X @=< J.
  165check_boole_node((A, B), X):-!,
  166	check_boole_node(A, X),
  167	check_boole_node(B, X).
  168check_boole_node((A; B), X):-!,
  169	( check_boole_node(A, X) -> true
  170	; check_boole_node(B, X)
  171	).
  172check_boole_node(\+A, X):-!,
  173	( check_boole_node(A, X) -> fail
  174	; true
  175	).
  176check_boole_node([A|As], X):-
  177	(	X = A -> true
  178	;	memberchk(X, As)
  179	).
  180
  181%
  182check_node_boole_(X, >=(I)):-!, I @=< X.
  183check_node_boole_(X, =<(I)):-!, X @=< I.
  184check_node_boole_(X, I-J):-!, I @=< X, X @=< J.
  185check_node_boole_(X, (A, B)):-!,
  186	check_node_boole_(X, A),
  187	check_node_boole_(X, B).
  188check_node_boole_(X, (A; B)):-!,
  189	( check_node_boole_(X, A) -> true
  190	; check_node_boole_(X, B)
  191	).
  192check_node_boole_(X, \+A):-!,
  193	( check_node_boole_(X, A) -> fail
  194	; true
  195	).
  196check_node_boole_(X, [A|As]):-
  197	(	X = A -> true
  198	;	memberchk(X, As)
  199	).
  200%
  201arrow_symbol( _ -> _).
  202% ?- arrow_symbol(_->_, F).
  203arrow_symbol(A, A0):- functor(A, A0, 2).
  204% ?- arrow_symbol(a->b, F, X, Y).
  205arrow_symbol(A, A0, A1, A2):- functor(A, A0, 2),
  206		arg(1, A, A1),
  207		arg(2, A, A2).
  208%
  209card_hybrid(X, ST, Y) :- @(card_hybrid(X, ST, Y)).
  210%
  211crad_hybrid(_, S-S, 1, _) :-!.
  212card_hybrid(X, ST, Y, S) :- open_state(M, [hash_size(128)]),
  213	card_hybrid(X, ST, Y, S, M),
  214	close_state(M).
  215%
  216card_hybrid(I, _, 0, _, _)	:- I < 2, !.
  217card_hybrid(I, ST, C, S, M)	:- memo(I-C, M),
  218	(	nonvar(C) -> true
  219	;	cofact(I, t(A, L, R), S),
  220		card_hybrid(L, ST, Cl, S, M),
  221		(	A = U-U ->	card_hybrid(R, ST, Cr, S, M)
  222		;	A = ST 	->	card_hybrid1(R, Cr, S, M)
  223		; 	Cr = 0
  224		),
  225	C is Cr + Cl
  226	).
  227%
  228card_hybrid1(I, I, _, _) :- I<2, !.
  229card_hybrid1(I, C, S, M) :- memo(I-C, M),
  230	(	nonvar(C) -> true
  231	;	cofact(I, t(A, L, R), S),
  232		card_hybrid1(L, Cl, S, M),
  233		(  	A = U-U ->  card_hybrid1(R, Cr, S, M)
  234		;	A = (_-_) ->	Cr = 0
  235		;	card(R, Cr, S, M)
  236		),
  237		C is Cr + Cl
  238	).
  239
  240%%%
  241card_path(X, ST, Y) :- @(card_path(X, ST, Y)).
  242%
  243card_path(_, S-S, 1, _) :-!.
  244card_path(X, ST, Y, S) :- open_substate(S),
  245	card_path_xmemo(X, ST, Y, S),
  246	close_substate(S).
  247%
  248card_path_xmemo(I, _, 0, _)	:- I < 2, !.
  249card_path_xmemo(I, ST, C, S)	:- memo(card(I)-C, S),
  250	(	nonvar(C) -> true
  251	;	cofact(I, t(A, L, R), S),
  252		card_path_xmemo(L, ST, Cl, S),
  253		(	A = U-U ->	card_path_xmemo(R, ST, Cr, S)
  254		;	A = ST 	->	card_path_xmemo(R, Cr, S)
  255		; 	Cr = 0
  256		),
  257	C is Cr + Cl
  258	).
  259%
  260card_path_xmemo(I, I, _) :- I<2, !.
  261card_path_xmemo(I, C, S) :- memo(card(I)-C, S),
  262	(	nonvar(C) -> true
  263	;	cofact(I, t(A, L, R), S),
  264		card_path_xmemo(L, Cl, S),
  265		(  	A = U-U ->  card_path_xmemo(R, Cr, S)
  266		;	A = (_-_) ->	Cr = 0
  267		;	card(R, Cr, S)
  268		),
  269		C is Cr + Cl
  270	).
  271
  272% ?- rect_dg(rect(0,1), X, Y).
  273% ?- rect_dg(rect(0,0), X, Y).
  274% ?- rect_dg(rect(1,1), X, Y).
  275rect_dg(rect(W, H), Nodes, Links):-
  276	rect_nodes(W, H, Nodes),
  277	rect_links(W, H, Nodes, Links).
  278
  279% ?- zdd((rect_udg(rect(1,1), X, Y, ST))).
  280% ?- zdd((rect_udg(rect(20,20), X, Y, ST))).
  281% ?- zdd0((rect_udg(rect(1,1), X, Y, ST))).
  282% ?- q_zdd((rect_udg(rect(1,1), X, Y, ST))).
  283
  284rect_udg(A, B, C, ST):- @(rect_udg(A, B, C, ST)).
  285%
  286rect_udg(Rect, Nodes, Links, ST, S):-
  287	rect_dg(Rect, Ns, Ls),
  288	zdd_sort(Ns, Nodes, S),
  289	maplist(pred(S, [U,V]:- normal_pair(U, V, S)), Ls, Ls0),
  290	zdd_sort(Ls0, Links, S),
  291	Rect=rect(W, H),
  292	normal_pair(p(0,0)-p(W,H), ST, S).
  293
  294% ?- zdd((rect_skew(rect(1,1), X, Y, ST))).
  295% ?- zdd0((rect_skew(rect(1,1), X, Y, ST))).
  296% ?- zdd((rect_skew(rect(20,20), X, Y, ST))).
  297rect_skew(A, B, C, D):- @(rect_skew(A, B, C, D)).
  298%
  299rect_skew(Rect, Nodes, Links, ST, S):-
  300	rect_dg_in_skew_axis(Rect, Nodes, Links, S),
  301	Rect=rect(W, H),
  302	convert_skew(p(W, H), P),
  303	normal_pair(p(0,0)-P, ST, S).
  304
  305% ?- rect_htdg(rect(0,0), N, L).
  306% ?- rect_htdg(rect(0,1), N, L).
  307% ?- rect_htdg(rect(1,1), N, L).
  308% ?- rect_htdg(rect(2,2), N, L), maplist(writeln, L).
  309% ?- rect_htdg(rect(3,3), N, L), maplist(writeln, L).
  310% ?- time(rect_htdg(rect(30,30), N, L)).
  311
  312rect_htdg(Rect, Nodes, Sorted_Links):-  Rect = rect(W, H),
  313	rect_dg(Rect, Nodes, Links),
  314	findall(A-B, (	member(A-B, Links),
  315					A @< B
  316				  ),
  317			 Canonical_links),
  318	Max is W+H,
  319	findall(I-L, (	between(0, Max, I),
  320					findall(P-Q, ( member(P-Q, Canonical_links),
  321								   P = p(P1,P2),
  322								   I =:= P1 + P2
  323								 ),
  324							L)
  325				 ),
  326			Sorted_Links).
  327
  328% ?- zdd((q_problem(rect(1,1), L, I, ST))).
  329
  330% ?- zdd((q_problem(rect(1,1), L, I, ST),
  331%		@(elim_links(L, I, M)),
  332%		@(card_hybrid(M, ST, C))
  333% )).
  334
  335q_problem(Rect, Links, ID, p(0,0)-p(W, H)):-
  336	Rect=rect(W, H),
  337	@(rect_udg(Rect, Nodes, Links)),
  338	findall(A-A, member(A, Nodes), ID).
  339
  340% ?- zdd0((skew_problem(rect(1,1), L, I, ST))).
  341% ?- zdd((skew_problem(rect(1,1), L, I, ST))).
  342% ?- zdd0((skew_problem(rect(1,1), L, I, ST))).
  343skew_problem(Rect, Links, ID, ST):- @(skew_problem(Rect, Links, ID, ST)).
  344%
  345skew_problem(Rect, Links, ID, ST, S):-
  346	rect_dg_in_skew_axis(Rect, Nodes, Links, S),
  347	findall(A-A, member(A, Nodes), ID0),
  348	zdd_sort(ID0, ID, S),
  349	Rect=rect(W, H),
  350	convert_skew(p(W, H), P),
  351	set_key(start, P, S),
  352	Level is W + H,
  353	set_key(level, Level, S),
  354	normal_pair(p(0,0)-P, ST, S).
  355
  356%
  357% rect_skew(Rect, Links, ID, ST, S):-
  358% 	rect_dg_in_skew_axis(Rect, Nodes, Links),
  359% 	findall(A-A, member(A, Nodes), ID0),
  360% 	zdd_sort(ID0, ID, S),
  361% 	Rect=rect(W, H),
  362% 	convert_skew(p(W, H), P),
  363% 	normal_pair(p(0,0)-P, ST, S).
  364
  365% ?- rect_nodes(4,5,Ns), length(Ns, L).
  366rect_nodes(W, H, Nodes):-
  367	findall(p(I, J),
  368			(	between(0, W, I),
  369				between(0, H, J)
  370			),
  371			Nodes0),
  372	sort(Nodes0, Nodes).
  373%
  374rect_links(W, H, Ns, Links):-
  375	findall(P-Q,
  376			(	member(P, Ns),
  377				P = p(I, J),
  378				(	Q = p(I, J1),
  379					(	J1 is J-1,
  380						J1 >= 0
  381					;	J1 is J+1,
  382						J1 =< H
  383					)
  384				;   Q = p(I1, J),
  385					(	I1 is I-1,
  386						I1 >= 0
  387					;	I1 is I+1,
  388						I1 =< W
  389					)
  390				)
  391			),
  392			Links0),
  393	sort(Links0, Links).
  394
  395%
  396atmark(X):- functor(X, @, 2).
  397
  398		/*******************************
  399		*     rect_path_count_naive    *
  400		*******************************/
  401% ?- zdd0(rect_path_count_naive(rect(1,0), C)).
  402% ?- zdd0(rect_path_count_naive(rect(2,0), C)).
  403% ?- zdd0(rect_path_count_naive(rect(1,2), C)).
  404% ?- zdd0(rect_path_count_naive(rect(1,3), C)).
  405% ?- zdd0(rect_path_count_naive(rect(3,1), C)).
  406% ?- zdd0(rect_path_count_naive(rect(2,2), C)).
  407% ?- zdd0(rect_path_count_naive(rect(2,2), C)).
  408% ?- zdd0(rect_path_count_naive(rect(2,2), C)).
  409% ?- time(zdd0(rect_path_count_naive(rect(3,2), C))).
  410% ?- time(zdd0(rect_path_count_naive(rect(2,3), C))).
  411% ?- time(zdd0(rect_path_count_naive(rect(3,3), C))).
  412
  413rect_path_count_naive(rect(W, H), C):-
  414	rect_dg(rect(W, H), X, Y),
  415	dg_path_count_naive(dg(X, Y), p(0,0)-p(W, H), C).
  416
  417		/*****************************
  418		*     dg_path_count_naive    *
  419		*****************************/
  420
  421% ?-zdd0(dg_path_count_naive(dg([a, b],[a-b]), a-b, C)).
  422% ?-zdd0(dg_path_count_naive(dg([a, b],[a-b, b-a]), a-b, C)).
  423% ?-zdd0(dg_path_count_naive(dg([a, b, c],[a-b, b-c, a-c]), a-c, C)).
  424% ?-zdd0(dg_path_count_naive(dg([a, b, c],[a-b, b-c, c-b, c-a, a-c]), a-c, C)).
  425dg_path_count_naive(D, ST, C):- @(dg_path_count_naive(D, ST, C)).
  426%
  427dg_path_count_naive(dg(Ns, Es), ST, C, S):-
  428		zdd_sort(Es, Fs, S),
  429		reverse(Fs, Gs),
  430		findall(X-X, member(X, Ns), Id),
  431		zdd_insert_atoms(Id, 1, Initial, S),
  432		repeat_update_mqp(Gs, Initial, Out, S),
  433		card_hybrid(Out, ST, C, S).
  434
  435		/***************************
  436		*     repeat_update_mqp    *
  437		***************************/
  438
  439repeat_update_mqp(Es, X, Y):- @(repeat_update_mqp(Es, X, Y)).
  440%
  441repeat_update_mqp([], X, X, _).
  442repeat_update_mqp([E|Es], X, Y, S):- update_mqp(E, X, X0, S),
  443	zdd_join(X0, X, Y0, S),
  444	repeat_update_mqp(Es, Y0, Y, S).
  445
  446% ?- zdd0((X<<{[a-a, b-b]}, apply_links_on_mqp([a-b], X, Y))).
  447% ?- zdd0((X<<{[a-a, b-b, c-c]},
  448%	apply_links_on_mqp([a-b, b-c, c-a, b-a, a-c], X, Y),
  449%	card_hybrid(Y, a-c, C))).
  450
  451apply_links_on_mqp(Es, X, Y):-@(apply_links_on_mqp(Es, X, Y)).
  452%
  453apply_links_on_mqp(Es, X, Y, S):- zdd_sort(Es, Fs, S),
  454	zdd_eval(pow(Fs), Pow, S),
  455	power_on_mqp(Pow, X, Y, S).
  456%
  457power_on_mqp(0, _, 0, _):-!.
  458power_on_mqp(1, X, X, _):-!.
  459power_on_mqp(_, X, 0, _):- X<2, !.
  460power_on_mqp(P, X, Y, S):- memo(power_on_mqp(P,X)-Y, S),
  461	(	nonvar(Y) -> true,	write(.)
  462	;	cofact(P, t(E, L, R), S),
  463		power_on_mqp(L, X, L0, S),
  464		update_mqp(E, X, EM, S),
  465		power_on_mqp(R, EM, R0, S),
  466		zdd_join(L0, R0, Y, S)
  467	).
  468
  469		/********************
  470		*     update_mqp    *
  471		********************/
  472
  473% ?- zdd0((X<<{[a-a, b-b, c-c]}, psa(X), update_mqp(a-b, X, Y), zdd_join(X, Y, Y0),
  474%	update_mqp(b-c, Y0, Z), zdd_join(Y0, Z, Z0),
  475%	update_mqp(a-c, Z0, U), zdd_join(Z0, U, U0), psa(U0),
  476%	card_hybrid(U0, a-c, C))).
  477
  478% ?- zdd0((X<<{[a-a, b-b, c-c]}, psa(X), update_mqp(a-b, X, Y), zdd_join(X, Y, Y0),
  479%	update_mqp(a-c, Y0, Z), zdd_join(Y0, Z, Z0), psa(Z0),
  480%	update_mqp(b-c, Z0, U), zdd_join(Z0, U, U0), psa(U0),
  481%	card_hybrid(U0, a-c, C))).
  482
  483update_mqp(E, X, Y):- @(update_mqp(E, X, Y)).
  484
  485%
  486update_mqp(_, X, 0, _):- X < 2,!.
  487%
  488update_mqp(E, X, Y, S):- cofact(X, t(P, L, R),  S),
  489	(	arrow_symbol(P) -> Y = 0
  490	;  	update_mqp(E, L, L0, S),
  491		E = (A-B),
  492		P = (C-D),
  493		(	zdd_compare(<, B, C, S) -> R0 = 0	% , write(.)  % Many hits.
  494		;	B = C -> replace_right([A->B], A, D, R, R0, S)
  495		;	A = D -> replace_left([A->B], B, C, R, R0, S)
  496		;	update_mqp(E, R, R1, S),
  497			zdd_insert(P, R1, R0, S)
  498		),
  499		zdd_join(L0, R0, Y, S)
  500	).
  501
  502		/**********************
  503		*     elim_links    *
  504		**********************/
  505
  506% ?- mk_sorted_pair(a, b, U).
  507% ?- mk_sorted_pair(b, a, U).
  508mk_sorted_pair(A, B, A-B):- A@<B, !.
  509mk_sorted_pair(A, B, B-A).
  510%
  511composable_pairs(A-B, A-C, B, C).
  512composable_pairs(A-B, C-A, B, C).
  513composable_pairs(B-A, A-C, B, C).
  514composable_pairs(B-A, C-A, B, C).
  515
  516
  517%
  518normal_pair(P, U):- @(normal_pair(P, U)).
  519%
  520normal_pair(A-B, B-A, S):- zdd_compare(>, A, B, S), !.
  521normal_pair(A->B, B->A, S):- zdd_compare(>, A, B, S), !.
  522normal_pair(P, P, _).
  523%
  524convert_skew_pair(P, Q):-
  525	(	P = (A-B) -> Q = (A0-B0)
  526	;	P = (A->B), Q = (A0->B0)
  527	),
  528	convert_skew(A, A0),
  529	convert_skew(B, B0).
  530% ?- open_state(S), set_compare(compare, S),
  531%	convert_normal_pair(p(1,0)-p(1,1), Q, S).
  532% ?- open_state(S), set_compare(compare, S),
  533%	convert_normal_pair(p(1,0)->p(1,1), Q, S).
  534
  535convert_normal_pair(P, Q, S):- convert_skew_pair(P, Q0),
  536	normal_pair(Q0, Q, S).
  537
  538%
  539normal_arrow(X, Y):- @(normal_arrow(X, Y)).
  540%
  541normal_arrow(A->B, Arr, S):-!,
  542	(	zdd_compare(>, A, B, S) -> Arr = (B->A)
  543	;	Arr = (A->B)
  544	).
  545normal_arrow(A-B, Arr, S):-
  546	(	zdd_compare(>, A, B, S) -> Arr = (B->A)
  547	;	Arr = (A->B)
  548	).
  549
  550%
  551lt_pair(_ - A, B -_, S):- zdd_compare(<, A, B, S).
  552
  553		/*********************************
  554		*     pruning rectangular mqp    *
  555		*********************************/
  556
  557to_be_pruned(X, Y, Z):- @(to_be_pruned(X, Y, Z)).
  558
  559to_be_pruned(Min, A-B, P, S):- A \== B,
  560	(	zdd_compare(<, B, P, S)
  561	;	A \== Min,
  562		zdd_compare(<, A, P, S)
  563	).
  564
  565%
  566prune_for_frontier(_, _, X, 0, _):- X<2, !.
  567prune_for_frontier(F, M, X, Y, S):- cofact(X, t(Ar, L, R), S),
  568		arrow_symbol(Ar, Arrow, P, Q),
  569		(	Arrow = (->)  ->  Y = 0
  570		;
  571		prune_for_frontier(F, M, L, L0, S),
  572		(	on_frontier(F, M, P)
  573		->	(	on_frontier(F, M, Q) ->	prune_for_frontier(F, M, R, R0, S)
  574			;	R0 = R
  575			)
  576		;	(	on_frontier(F, M, Q) ->	R0 = R
  577			;	R0 = 0
  578			)
  579		),
  580		cofact(Y, t(P-Q, L0, R0), S)
  581		).
  582%
  583on_frontier(F, _, p(F, _)).
  584on_frontier(_, M, M).
  585%
  586u_prune(P, X, Y, S):- get_key(prune, F, S), !,
  587	zdd_shift(u_prune(F, P, X, Y, S)).
  588u_prune(_, X, X, _).
  589%
  590u_prune(F, P, X, Y, S, M):- apply_prune(F, P, X, X0, S, M),
  591	zdd_subtr(X, X0, Y, S).
  592%
  593apply_prune(_, _, X, 0, _, _):- X<2, !.
  594apply_prune(F, P, X, Y, S, M):- memo(apply_prune(X)-Y,  M),
  595	(	nonvar(Y) -> true	% , write(/)	% many hits.
  596	;	cofact(X, t(Ar, L, R), S),
  597		apply_prune(F, P, L, L0, S, M),
  598		(	call(F, Ar, P, S) -> R0 = R
  599		;	lt_pair(Ar, P, S) -> R0 = 0
  600		;	apply_prune(F, P, R, R0, S, M)
  601		),
  602		cofact(Y, t(Ar, L0, R0), S)
  603	).
  604
  605%
  606:- meta_predicate udg(:).  607udg(X):- zdd((set_compare(opp_compare), X)).
  608
  609:- meta_predicate q_zdd(:).  610q_zdd(X):- zdd((set_compare(q_compare), X)).
  611% ?- q_zdd(normal_pair(a-b, X)).
  612% ?- q_zdd(normal_pair(1-2, X)).
  613% ?- udg((zdd_sort([p(0,0),p(1,1)], R))).
  614% ?- spy(q_problem).
  615% ?- w_count(rect(1,1), C).
  616w_count(Rect, C):- 	zdd((q_problem(Rect, Links, ID, ST),
  617		  MQP<<set(ID),
  618		  @(elim_links(Links, MQP, MQP1),
  619		  card_hybrid(MQP1, ST, C)))).
  620
  621%%%uuuu
  622% ?- zdd(q_count(rect(0, 1), C)).
  623%@ p(1,0)-p(0,0)
  624%@ C = 1 .
  625% ?- zdd(q_count(rect(1, 0), C)).
  626%@ p(1,1)-p(0,0)
  627%@ C = 1 .
  628% ?- zdd(q_count(rect(1, 1), C)).
  629% ?- zdd(q_count(rect(1, 2), C)).
  630% ?- zdd(q_count(rect(2, 2), C)).
  631% ?- time(zdd(q_count(rect(2, 2), C))).
  632% ?- time(zdd(q_count(rect(3, 3), C))).
  633% ?- time(zdd(q_count(rect(3, 4), C))).
  634% ?- time(zdd0(q_count(rect(4, 4), C))).
  635% ?- time(zdd0(q_count(rect(5, 5), C))).
  636%@ % 12,276,144,277 inferences, 1672.961 CPU in 1693.367 seconds (99% CPU, 7337975 Lips)
  637%@ C = 1262816.
  638
  639q_count(Rect, C):- @(q_count(Rect, C)).
  640%
  641q_count(Rect, C, S):- set_compare(q_compare, S),
  642		(	is_normal_order(S)
  643		->	set_pred(compare_layer, q_compare_layer, S),
  644			set_pred(succ, succ, S)
  645		;	set_pred(compare_layer, q_compare_layer_opp, S),
  646			set_pred(succ, succ_opp, S)
  647		),
  648		skew_problem(Rect, Links, ID, ST, S),
  649		layer_by_level(ID, IDLayers, S),
  650		set_key(idlayers, IDLayers, S),
  651		layer_by_level(Links, Layers, S),
  652		get_key(start, Start, S),
  653		set_pred(prune, to_be_pruned(Start), S),
  654		zdd_ord_insert(ID, 1, MQP, S),
  655		elim_layers(Layers, MQP, MQP1, S),
  656		card_hybrid(MQP1, ST, C, S).
  657%
  658layer_by_level(Links, OutLinks, S):-
  659	get_key(level, MaxLevel, S),
  660	findall(I-G, (	between(0, MaxLevel, I),
  661					findall(Ar, (	member(Ar, Links),
  662									Ar = p(I,_)-_
  663								),
  664							G0),
  665					zdd_sort(G0, G, S)
  666				 ),
  667			Leveled_Links),
  668	get_key(compare_layer, Compare_Layer, S),
  669	predsort(Compare_Layer, Leveled_Links, OutLinks).
  670
  671%
  672elim_layers(X, Y, Z):- @(elim_layers(X, Y, Z)).
  673%
  674elim_layers([], X, X, _).
  675elim_layers([Level-Es | Layers], X, Y, S):-
  676	get_key(start, Min, S),
  677	prune_for_frontier(Level, Min, X, X0, S),
  678	zdd_subtr(X, X0, X1, S),
  679	get_key(succ, SUCC, S),
  680	call(SUCC, Level1, Level),
  681	prune_for_cut_path(Level1, X1, X2, S),
  682	zdd_subtr(X1, X2, X3, S),
  683	elim_links(Es, X3, Z, S),
  684	elim_layers(Layers, Z, Y, S).
  685%
  686prune_for_cut_path(Lev, X, Y, S):-
  687	get_key(idlayers, IDLayers, S),
  688	(	memberchk(Lev-ID, IDLayers)
  689	->  zdd_sub_for_ord_list(ID, X, Y, S)
  690	;	Y = 0
  691	).
  692
  693		/**********************************
  694		*     basic operation on links    *
  695		**********************************/
  696:- meta_predicate q_count_plain(:, :, ?, ?).  697:- meta_predicate q_count_plain(:, :, ?, ?, ?).  698
  699% ?- zdd(q_count_plain(compare, rect_skew, rect(1, 0), C)).
  700% ?- zdd(q_count_plain(compare, rect_skew, rect(1, 2), C)).
  701% ?- zdd(q_count_plain(compare, rect_skew, rect(3, 2), C)).
  702% ?- zdd(q_count_plain(q_compare, rect_udg, rect(2, 2), C)).
  703% ?- zdd(q_count_plain(opp_compare, rect_udg, rect(2, 2), C)).
  704% ?- zdd(q_count_plain(opp_compare, rect_udg, rect(3, 3), C)).
  705% ?- zdd(q_count_plain(compare, rect_udg, rect(1, 0), C)).
  706% ?- zdd(q_count_plain(compare, rect_udg, rect(2, 0), C)).
  707% ?- zdd(q_count_plain(compare, rect_udg, rect(2, 2), C)).
  708
  709q_count_plain(X, Y, Z, U):-@(q_count_plain(X, Y, Z, U)).
  710%
  711q_count_plain(Compare, F, Rect, C, S):-
  712		set_compare(Compare, S),
  713		call(F, Rect, Nodes, Links, ST, S),
  714		ST = Start-_,
  715		set_pred(prune, to_be_pruned(Start), S),
  716		findall(A-A, member(A, Nodes), 	ID),
  717		zdd_insert_atoms(ID, 1, MQP, S),
  718		elim_links(Links, MQP, MQP1, S),
  719		card_hybrid(MQP1, ST, C, S).
  720%
  721elim_links(A, B, C):- @(elim_links(A, B, C)).
  722%
  723elim_links([], X, X, _).
  724elim_links([E|Es], X, Y, S):-
  725	writeln(E),
  726	elim_link(E, X, X0, S),
  727	zdd_join(X, X0, X1, S),
  728	E  = P-_,
  729	u_prune(P, X1, X2, S),
  730	elim_links(Es, X2, Y, S).
  731%
  732elim_link(E, X, Y):- @(elim_link(E, X, Y)).
  733% ?- time(zdd0(q_count(rect(3, 4), C))).
  734
  735elim_link(_, X, 0, _):- X < 2,!.
  736elim_link(E, X, Y, S):-	cofact(X, t(P, L, R),  S),
  737	(	P = (_->_)  ->  Y = 0   %Y = X
  738	;	lt_pair(E, P, S) -> Y = 0
  739	;  	elim_link(E, L, L0, S),
  740		(	composable_pairs(E, P, U, V)
  741		-> 	normal_arrow(E, Arrow, S),
  742			replace_end([Arrow], U, V, R, R0, S)
  743		;	elim_link(E, R, R1, S),
  744			zdd_insert(P, R1, R0, S)
  745		),
  746		zdd_join(L0, R0, Y, S)
  747	).
  748
  749% elim_link with memo
  750elim_link(_, X, 0, _, _):- X < 2,!.
  751elim_link(E, X, Y, S, M):-	cofact(X, t(P, L, R),  S),
  752	(	P = (_->_)  ->  Y = 0   %Y = X
  753	;	lt_pair(E, P, S) -> Y = 0
  754	;  	elim_link(E, L, L0, S, M),
  755		(	composable_pairs(E, P, U, V)
  756		-> 	normal_arrow(E, Arrow, S),
  757			replace_end([Arrow], U, V, R, R0, S, M)
  758		;	elim_link(E, R, R1, S, M),
  759			x_insert(P, R1, R0, S, M)
  760		),
  761		x_join(L0, R0, Y, S, M)
  762	).
  763
  764% Most basic operation.
  765replace_end(_, _, _, X, 0, _):- X < 2, !.
  766replace_end(Es, A, P, X, Y, S):-  	/* replace A with P */
  767	cofact(X, t(U, L, R), S),
  768	arrow_symbol(U, Arrow, Lu, Ru),
  769	(	Arrow = (->) ->	Y = 0
  770	;	replace_end(Es, A, P, L, L0, S),
  771		U = Lu-Ru,
  772		(	zdd_compare(<, A, Lu, S)
  773		->	Y = 0
  774		;	Ru = A
  775		->	normal_pair(Lu-P, V, S),
  776			zdd_ord_insert([V|Es], R, R0, S)
  777		;	Lu = A
  778		->  normal_pair(Ru-P, V, S),
  779			zdd_ord_insert([V|Es], R, R0, S)
  780		;	replace_end(Es, A, P, R, R1, S),
  781			zdd_insert(U, R1, R0, S)
  782		),
  783		zdd_join(L0, R0, Y, S)
  784	).
  785
  786
  787		/********************************
  788		*     u_repeat_update_mqp		*
  789		********************************/
  790
  791u_repeat_update_mqp(Es, X, Y):-
  792	@(u_repeat_update_mqp(Es, X, Y)).
  793%
  794u_repeat_update_mqp([], X, X, _).
  795u_repeat_update_mqp([E|Es], X, Y, S):- u_update_mqp(E, X, X0, S),
  796	zdd_join(X0, X, X1, S),
  797	u_obsolete_mqp(X1, Ob, S),
  798	zdd_subtr(X1, Ob,  Y0, S),
  799	u_repeat_update_mqp(Es, Y0, Y, S).
  800%
  801u_obsolete_mqp(X, Y, S):-
  802	(	get_key(obsolete_checker, F, S)
  803	->	call(F, X, Y, S)
  804	;	Y = 0
  805	).
  806%
  807u_update_mqp_aux(A-B, C-D, U, V):-
  808		(	B = C -> U = A, V = D
  809		;	B = D -> U = A, V = C
  810		;	A = C -> U = B, V = D
  811		;	A = D -> U = B, V = C
  812		).
  813%
  814u_update_mqp(E, X, Y):- @(u_update_mqp(E, X, Y)).
  815%
  816u_update_mqp(_, X, 0, _):- X < 2,!.
  817u_update_mqp(E, X, Y, S):- E = A-B,
  818	cofact(X, t(P, L, R),  S),
  819	(	arrow_symbol(P)  ->  Y = 0
  820	;  	u_update_mqp(E, L, L0, S),
  821		(	u_update_mqp_aux(E, P, U, V)
  822		-> 	u_replace_mqp(A->B, U, V, R, R0, S)
  823		;	u_update_mqp(E, R, R1, S),
  824			zdd_insert(P, R1, R0, S)
  825		),
  826		zdd_join(L0, R0, Y, S)
  827	).
  828
  829%
  830u_replace_mqp(_, _, _, X, 0, _):- X < 2, !.
  831u_replace_mqp(E, A, P, X, Y, S):- cofact(X, t(U, L, R), S),
  832	arrow_symbol(U, Arrow, Lu, Ru),
  833	(	Arrow = (->) ->	Y = 0
  834	;	u_replace_mqp(E, A, P, L, L0, S),
  835		U = Lu-Ru,
  836		(	zdd_compare(<, A, Lu, S),
  837			zdd_compare(<, P, Lu, S)
  838		->	Y = 0
  839		;	Ru = A
  840		->	normal_pair(Lu-P, V, S),
  841			zdd_insert_atoms([V, E], R, R0, S)
  842		;	Lu = A
  843		->  normal_pair(Ru-P, V, S),
  844			zdd_insert_atoms([V, E], R, R0, S)
  845		;	u_replace_mqp(E, A, P, R, R1, S),
  846			zdd_insert(U, R1, R0, S)
  847		),
  848		zdd_join(L0, R0, Y, S)
  849	).
  850
  851
  852
  853% ?- zdd((X<<{[a-a,b-b,c-c]}, update_qp(a-b, X, Y), psa(Y), update_qp(b-c, Y, Z), psa(Z))).
  854% ?- zdd0((X<<{[a-a,b-b,c-c]}, update_qp(a-b, X, Y), psa(Y), update_qp(c-a, Y, Z), psa(Z))).
  855% ?- zdd0((X<<{[a-a,b-b,c-c]}, update_qp(a-b, X, Y), psa(Y), update_qp(b-c, Y, Z), psa(Z), update_qp(b-a, Z, U), psa(U))).
  856
  857update_qp(E, X, Y):- @(update_qp(E, X, Y)).
  858
  859%
  860update_qp(_, X, 0, _):- X < 2,!.
  861update_qp(E, X, Y, S):- cofact0(X, P, R, S),
  862		E = (A-B),
  863		P = (C-D),
  864		(	zdd_compare(<, A, C, S)
  865		->  Y = 0		% , write(.)  % Many hits.
  866		;	B = C -> qp_replace_right(A, D, R, Y, S)
  867		;	A = D -> qp_replace_left(B, C, R, Y, S)
  868		;	update_qp(E, R, R0, S),
  869			zdd_insert_as_list(P, R0, Y, S)
  870		).
  871
  872%  udg: unordered pair   a-b = b-a
  873u_update_qp(E, X, Y):- @(u_update_qp(E, X, Y)).
  874
  875%
  876u_update_qp(_, X, 0, _):- X < 2,!.
  877u_update_qp(E, X, Y, S):- cofact0(X, P, R, S),
  878		E = (A-B),
  879		P = (C-D),
  880		( 	zdd_compare(<, B, C, S)	-> Y = 0 %, write(.)		% Great many hits.
  881		;	B = C -> u_qp_replace(A, D, R, Y, S)
  882		;	B = D -> u_qp_replace(A, C, R, Y, S)
  883		;	A = C -> u_qp_replace(B, D, R, Y, S)
  884		;	A = D -> u_qp_replace(B, C, R, Y, S)
  885		;	u_update_qp(E, R, R0, S),
  886			u_insert(P, R0, Y, S)
  887		).
  888%
  889u_insert(_, 0, 0, _):-!.
  890u_insert(P, 1, Y, S):-!, zdd_singleton(P, Y, S).
  891u_insert(P, X, Y, S):- cofact0(X, Q, R, S),
  892	zdd_compare(C, P, Q, S),
  893	(	C = (<) ->	cofact0(Y, P, X, S)
  894	;	C = (=) ->	Y = X
  895	;	u_insert(P, R, R0, S),
  896		cofact0(Y, Q, R0, S)
  897	).
  898
  899% ?- zdd0((set_key(min, d), X << {[d-e]}, slim_mqp(d, X, Y), psa(Y))).
  900% ?- zdd0((X << {[d-d]}, slim_mqp(d, X, Y), psa(Y))).
  901% ?- zdd0((X << {[]}, slim_mqp(d, X, Y), psa(Y))).
  902% ?- zdd0((X << {[d-e]}, slim_mqp(e, X, Y), psa(Y))).
  903
  904slim_mqp(P, X, Y):- @(slim_mqp(P, X, Y)).
  905%
  906slim_mqp(P, X, Y, S):- get_key(min, Q, S),
  907	obsolete_mqp(P, Q, X, U, S),
  908	zdd_subtr(X, U, Y, S).
  909
  910% ?- spy(obsolete_mqp).
  911% ?- zdd0((X << {[d-d]}, obsolete_mqp(d, d, X, Y), psa(Y))).
  912% ?- zdd0((X << {[d-d]}, obsolete_mqp(e, X, Y), psa(Y))).
  913% ?- zdd0((X << {[d-d]}, obsolete_mqp(a, X, Y), psa(Y))).
  914% ?- zdd0((X << {[d-e]}, obsolete_mqp(d, X, Y), psa(Y))).
  915% ?- zdd0((X << {[x-z, d-e]}, obsolete_mqp(z, X, Y), psa(Y), psa(X))).
  916
  917obsolete_mqp(P, Q, X, Y):- @(obsolete_mqp(P, Q, X, Y)).
  918%
  919obsolete_mqp(_, _, X, 0, _):- X<2, !.
  920obsolete_mqp(P, Q, X, Y, S):- cofact(X, t(E, L, R), S),
  921	arrow_symbol(E, E0, A, B),
  922	(	E0=(-)
  923	->	obsolete_mqp(P, Q, L, L0, S),
  924		zdd_compare(C, A, P, S),
  925		(	C = (<) ->	R0 = R
  926		;	C = (=) ->	R0 = R
  927		;	B = Q	->  obsolete_mqp(P, Q, R, R0, S)
  928		;	B = P	->  R0 = R
  929		),
  930		cofact(Y, t(E, L0, R0), S)
  931	;	Y = 0
  932	).
  933
  934% f(p(I0, J0), p(I, J)):- I0 is I-1, J0 is J-1, I0>=0, J0>=0.
  935% g(p(I0, J0), p(I, J)):-
  936
  937		/*********************
  938		*     update_link    *
  939		*********************/
  940
  941update_links(Es, X, Y):- @(update_links(Es, X, Y)).
  942%
  943update_links([], X, X, _).
  944update_links([E|Es], X, Y, S):- update_link(E, X, X0, S),
  945	zdd_join(X0, X, Y0, S),
  946	update_links(Es, Y0, Y, S).
  947
  948% ?- zdd0((X<<{[a-a, b-b]}, psa(X), update_link(a-b, X, Y), psa(Y))).
  949% ?- zdd0((X<<{[p(0,0)-p(0,0), p(1,0)-p(1,0)]}, psa(X), update_link(p(0,0)-p(1,0), X, Y), psa(Y))).
  950% ?- zdd0((X<<{[p(1,0)-p(1,0), p(0,0)-p(0,0)]}, psa(X), update_link(p(0,0)-p(1,0), X, Y), psa(Y),
  951% ?- zdd0((X<<{[a-a, b-b, c-c]}, psa(X), update_link(a-b, X, Y), psa(Y))).
  952% ?- zdd0((X<<{[c-c, b-b, a-a]}, psa(X), update_link(a-b, X, Y), psa(Y))).
  953% ?- zdd0((X<<{[b-b, a-a]}, psa(X), update_link(a-b, X, Y), psa(Y))).
  954% ?- zdd0((X<<{[a-a, b-b, c-c]}, psa(X), update_link(a-b, X, Y), psa(Y))).
  955% ?- zdd0((X<<{[c-c, b-b, a-a]}, psa(X), update_link(a-b, X, Y), psa(Y))).
  956% ?- zdd0((X<<{[1-2, 3-4, 5-6]}, update_link(3-4, X, Y), psa(Y))).
  957% ?- zdd0((X<<{[4-5]}, psa(X), update_link(2-3, X, Y), psa(Y))).
  958% ?- zdd0((X<<{[4-5,3-3]}, psa(X), update_link(3-4, X, Y), psa(Y))).
  959% ?- zdd0((X<<{[4-5,3-3]}, psa(X), update_link(5-6, X, Y), psa(Y))).
  960update_link(E, X, Y):- @(update_link(E, X, Y)).
  961
  962update_link(_, X, 0, _):- X < 2,!.
  963update_link(E, X, Y, S):- memo(update_link(E, X)-Y, S),
  964	(	nonvar(Y) -> true	% many hits !
  965	;  	cofact(X, t(P, L, R),  S),
  966		update_link(E, L, L0, S),
  967		(	touch(E, P)
  968		->	update_link(P, E, R, R0, S)
  969		;	update_link(E, R, U, S),
  970			zdd_insert(P, U, R0, S)
  971		),
  972		zdd_join(L0, R0, Y, S)
  973	).
  974
  975%
  976update_link(_, _, X, 0, _):- X<2, !.
  977update_link(P, E, X, Y, S):- memo(update_link(P, E, X)-Y, S),
  978	(	nonvar(Y)	-> true		% many hits !
  979	;	cofact(X, t(Q, L, R), S),
  980		update_link(P, E, L, L0, S),
  981		(	touch(E, Q)
  982		->  qp_connect(E, P, Q, U),
  983			change_symbol(E, E0),
  984			zdd_insert_atoms([E0, U], R, R0, S)
  985		;	update_link(P, E, R, U, S),
  986			zdd_insert(Q, U, R0, S)
  987		),
  988		zdd_join(L0, R0, Y, S)
  989	).
  990
  991		/**********************
  992		*     mortal paths    *
  993		**********************/
  994
  995% ?- zdd0((X<<{[3-4]}, mortal_paths(5-2, X, Y))).
  996% ?- zdd0((X<<{[3-4]}, mortal_paths(5-2, X, Y))).
  997% ?- zdd0((X<<{[3-4]}, mortal_paths(2-3, X, Y))).   % Y = 0
  998
  999mortal_paths(E, X, Y):- @(mortal_paths(E, X, Y)).
 1000%
 1001
 1002mortal_paths(_, X, 0, _):- X < 2,!.
 1003mortal_paths(E, X, Y, S):-
 1004	  	cofact(X, t(P, L, R),  S),
 1005		mortal_paths(E, L, L0, S),
 1006		(	arrow_symbol(P, ->) ->	R0 = 0
 1007		;	mortal(E, P) ->	zdd_insert(P, R, R0, S)
 1008		; 	mortal_paths(E, R, U, S),
 1009			zdd_insert(P, U, R0, S)
 1010		),
 1011	zdd_join(L0, R0, Y, S).
 1012
 1013%
 1014mortal(A-_, X-Y):- X\==Y,  A @> Y.   % As are monotone increarsing
 1015
 1016%
 1017update_link_slim(E, X, Y):- @(update_link_slim(E, X, Y)).
 1018%
 1019update_link_slim(E, X, Y, S):- update_link(E, X, X0, S),
 1020	zdd_join(X, X0, X1, S),
 1021	mortal_paths(E, X1, MP, S),
 1022	zdd_subtr(X1, MP, Y, S).
 1023
 1024%
 1025update_links_slim(E, X, Y):- @(update_links_slim(E, X, Y)).
 1026
 1027update_links_slim([], X, X, _).
 1028update_links_slim([E|Es], X, Y, S):-  update_link_slim(E, X, X0, S),
 1029	update_links_slim(Es, X0, Y, S).
 1030
 1031		/*********************
 1032		*     merge_blocks   *
 1033		*********************/
 1034
 1035% ?- zdd0((X<<{[a-a]}, Y<<{[b-b]},
 1036%	merge_blocks([a-b], X, Y, Z),
 1037%	psa(Z))).
 1038
 1039merge_blocks(Es, X, Y, Z):- @(merge_blocks(Es, X, Y, Z)).
 1040%
 1041merge_blocks(Es, X, Y, Z, S):- merge_blocks(Es, X, Y, 0, Z, S).
 1042%
 1043merge_blocks([], X, Y, Z, W, S):- zdd_merge(X, Y, U, S),
 1044	zdd_join(U, Z, W, S).
 1045merge_blocks([E|Es], X, Y, Z0, Z, S):- merge_blocks_step(E, X, Y, U, S),
 1046	update_mqp(E, Z0, V, S),
 1047%	update_link(E, Z0, V, S),
 1048	zdd_join_list([U, V], Z0, Z1, S),
 1049	merge_blocks(Es, X, Y, Z1, Z, S).
 1050
 1051merge_blocks_step(A-B, X, Y, Z, S):-
 1052	(	A @< B
 1053	-> 	link_across_out(A, B, X, Y, Z, S)
 1054%	;	link_across_in(B, A, X, Y, Z, S)
 1055	;	link_across_in(A, B, X, Y, Z, S)
 1056	).
 1057
 1058%
 1059link_across_out(_, _, R, _, 0, _):- R < 2, !.
 1060link_across_out(M, M0, R, R0, Q0, S):- cofact(R, t(A, Left, Right), S),
 1061	arrow_symbol(A, A0, U, V),
 1062	(	A0 = (->)  -> Q0 = 0
 1063	; 	link_across_out(M, M0, Left, R0, Q1, S),
 1064		(	M = V ->
 1065			replace_left([M->M0], M0, U, R0, R1, S),
 1066			zdd_merge(Right, R1, R2, S)
 1067		;	M @> V ->  R2 = 0	% , write(.) % small hits.
 1068		;	link_across_out(M, M0, Right, R0, R1, S),
 1069			zdd_insert(U-V, R1, R2, S)
 1070		),
 1071	zdd_join(Q1, R2, Q0, S)
 1072	).
 1073
 1074link_across_in(_, _, R, _, 0, _):- R < 2, !.
 1075link_across_in(M, M0, R, R0, Q0, S):- cofact(R, t(A, Left, Right), S),
 1076	arrow_symbol(A, A0, U, V),
 1077	(	A0 = (->) -> Q0 = 0
 1078	;  	link_across_in(M, M0, Left, R0, L0, S),
 1079		(	M = U ->
 1080			replace_right([M0->M], M0, V, R0, R1, S),
 1081			zdd_merge(Right, R1, R2, S)
 1082		;	M @> U ->  R2 = 0	% , write(+)  % small hits.
 1083		;	link_across_in(M, M0, Right, R0, R1, S),
 1084			zdd_insert(U-V, R1, R2, S)
 1085		),
 1086		zdd_join(L0, R2, Q0, S)
 1087	).
 1088
 1089
 1090
 1091		/**************************
 1092		*     u_merge_blocks    *
 1093		**************************/
 1094
 1095on_the_same_column(X, Y):- arg(1, X, A), arg(1, Y, A).
 1096%
 1097u_merge_blocks(Es, X, Y, Z):- @(u_merge_blocks(Es, X, Y, Z)).
 1098%
 1099u_merge_blocks(Es, X, Y, Z, S):- u_merge_blocks(Es, X, Y, 0, Z, S).
 1100%
 1101u_merge_blocks([], X, Y, Z, W, S):- zdd_merge(X, Y, U, S),
 1102	zdd_join(U, Z, W, S).
 1103u_merge_blocks([E|Es], X, Y, Z0, Z, S):- u_merge_blocks_step(E, X, Y, U, S),
 1104	u_update_mqp(E, Z0, V, S),
 1105	zdd_join_list([U, V], Z0, Z1, S),
 1106	u_merge_blocks(Es, X, Y, Z1, Z, S).
 1107%
 1108u_merge_blocks_step(_, X, _, 0, _):- X<2, !.
 1109u_merge_blocks_step(E, X, Y, Z, S):- E = A-B,
 1110	cofact(X, t(P, L, R), S),
 1111	(	arrow_symbol(P) -> Z = 0
 1112	;	u_merge_blocks_step(E, L, Y, L0, S),
 1113		(	u_update_mqp_aux(E, P, U, V)
 1114		->  (	on_the_same_column(U, P)
 1115			-> 	u_replace_mqp(U, V, R, R1, S),
 1116				zdd_merge(R1, Y, R0, S)
 1117			;	u_replace_mqp(U, V, Y, Y0, S),
 1118				zdd_merge(R, Y0, R0, S)
 1119			)
 1120		;	u_merge_blocks_step(E, R, Y, R1, S),
 1121			zdd_insert(A->B, R1, R0, S)
 1122		),
 1123		zdd_join(L0, R0, Z, S)
 1124	).
 1125
 1126		/****************************
 1127		*    bridge across blocks   *
 1128		****************************/
 1129
 1130links_across(Es, X, Y, Z):- @(links_across(Es, X, Y, Z)).
 1131%
 1132links_across(Es, X, Y, Z, S):- links_across(Es, X, Y, 0, Z, S).
 1133%
 1134links_across([], X, Y, Z, W, S):- zdd_merge(X, Y, U, S),
 1135	zdd_join(U, Z, W, S).
 1136links_across([E|Es], X, Y, Z0, Z, S):- link_across(E, X, Y, U, S),
 1137	update_link(E, Z0, V, S),
 1138	zdd_join_list([U, V], Z0, Z1, S),
 1139	links_across(Es, X, Y, Z1, Z, S).
 1140%
 1141link_across(_, X, _, 0, _):- X < 2, !.
 1142link_across(E, X, Y, Z, S):- cofact(X, t(A, L, R), S),
 1143	E = LoE - RoE,
 1144	arrow_symbol(A, A0, LoA, RoA),
 1145	(	A0 = (->) ->  Z = 0
 1146	;	link_across(E, L, Y, LY, S),
 1147		(	(LoE = RoA ;  RoE = LoA) ->
 1148			link_across(A, E, R, Y, RY, S)
 1149		;  	link_across(E, R, Y, U, S),
 1150			zdd_insert(A, U, RY, S)
 1151		),
 1152		zdd_join(LY, RY, Z, S)
 1153	).
 1154
 1155link_across(_, _, _, Y, 0, _):- Y<2, !.
 1156link_across(A, E, X, Y, Z, S):- cofact(Y, t(B, L, R), S),
 1157	(	arrow_symbol(B, ->) ->  Z = 0
 1158	;	link_across(A, E, X, L, XL, S),
 1159		(	touch(E, B)
 1160		->	qp_connect(E, A, B, C),
 1161			zdd_merge(X, R, U, S),
 1162			change_symbol(E, E0),
 1163			zdd_insert_atoms([E0, C], U, XR, S)
 1164		;	link_across(A, E, X, R, U, S),
 1165			zdd_insert(B, U, XR, S)
 1166		),
 1167		zdd_join(XL, XR, Z, S)
 1168	).
 1169
 1170		/*****************************
 1171		*     glue-block-frontier    *
 1172		*****************************/
 1173%
 1174glue_block_column(Es, X, Y, Z):- @(glue_block_column(Es, X, Y, Z)).
 1175
 1176glue_block_column(Es, X, Y, Z, S):- glue_block_column(Es, X, Y, 0, Z, S).
 1177%
 1178glue_block_column([], _, _, Z, Z, _).
 1179glue_block_column([E|Es], X, Y, Z0, Z, S):-
 1180	glue_columns(E, X, Y, U, S),
 1181	update_link(E, Z0, V, S),
 1182	zdd_join_list([U, V], Z0, Z1, S),
 1183	glue_block_column(Es, X, Y, Z1, Z, S).
 1184
 1185%
 1186glue_columns(_, X, _, 0, _):- X < 2, !.
 1187glue_columns(E, X, Y, Z, S):- E = U-V,
 1188	cofact(X, t(A, L, R), S),
 1189	arrow_symbol(A, A0, A1, A2),
 1190	(	A0 = (->) -> Z = 0
 1191	;   glue_columns(E, L, Y, L0, S),
 1192		(	U @< V ->
 1193			(	U = A2 ->
 1194				replace_left_column(A1, V, Y, W, S),
 1195				zdd_merge_list([E, R], W, R0, S)
 1196			;	glue_columns(E, R, Y, W, S),
 1197				zdd_insert(A, W, R0, S)
 1198			)
 1199		;	(	V = A1 ->
 1200				replace_right_column(A2, U, Y, W, S),
 1201				zdd_merge_list([E, R], W, R0, S)
 1202			;	V @< A1  ->  R0 = 0
 1203			;	glue_columns(E, R, Y, W, S),
 1204				zdd_insert(A, W, R0, S)
 1205			)
 1206		),
 1207		zdd_join(L0, R0, Z, S)
 1208	).
 1209
 1210%
 1211replace_right_column(_, _, X, 0, _):- X < 2, !.
 1212replace_right_column(A, P, X, Y, S):- cofact(X, t(U, L, R), S),
 1213	arrow_symbol(U, Arrow, Lu, Ru),
 1214	(	Arrow = (->) ->	Y = 0
 1215	;	replace_right_column(A, P, L, L0, S),
 1216		(	Ru = A ->
 1217			cofact(Y, t(Lu - P, L0, R), S)
 1218		;	replace_right_column(A, P, R, R0, S),
 1219			cofact(Y, t(U, L0, R0), S)
 1220		)
 1221	).
 1222
 1223%
 1224replace_left_column(_, _, X, 0, _):- X < 2, !.
 1225replace_left_column(A, P, X, Y, S):- cofact(X, t(U, L, R), S),
 1226	arrow_symbol(U, Arrow, Lu, Ru),
 1227	(	Arrow = (->) -> Y = 0
 1228	;	replace_left_column(A, P, L, L0, S),
 1229		compare(C, A, Lu),
 1230		(	C = (>) ->	R0 = 0
 1231		; 	C = (=)	->
 1232			zdd_insert(P - Ru, R, R0, S)
 1233		;	replace_left_column(A, P, R, W, S),
 1234			zdd_insert(U, W, R0, S)
 1235		),
 1236		zdd_join(L0, R0, Y, S)
 1237	).
 1238
 1239%
 1240slim_block_column(X, 0, _, _):- X<2, !.
 1241slim_block_column(X, Y, K, S):- cofact(X, t(A, L, R), S),
 1242	arrow_symbol(A, A0, A1, A2),
 1243	(	A0 = (->) -> Y = 0
 1244	;	slim_block_column(L, L0, K, S),
 1245		(	A1 = p(K, _) ->
 1246			(	( A2 = p(K, _); A2 = p(0, 0))  ->
 1247				slim_block_column(R, R0, K, S)
 1248			;	R0 = 0
 1249			)
 1250		;	A1 = A2 -> slim_block_column(R, R0, S)
 1251		;	R0 = 0
 1252		),
 1253		cofact(Y, t(A, L0, R0), S)
 1254	).
 1255%
 1256slim_block_column(X, X, _):- X < 2, !.
 1257slim_block_column(X, Y, S):- cofact(X, t(A, L, R), S),
 1258	arrow_symbol(A, A0, A1, A2),
 1259	(	A0 = (->) -> Y = X
 1260	;	slim_block_column(L, L0, S),
 1261		(	A1 = A2 ->
 1262			slim_block_column(R, R0, S)
 1263		;	R0 = 0
 1264		),
 1265		cofact(Y, t(A, L0, R0), S)
 1266	).
 1267%
 1268compare_rev(C, X, Y):- compare(C, Y, X).
 1269
 1270%
 1271replace_right(A, P, X, Y, S):- replace_right([A->P], A, P, X, Y, S).
 1272%
 1273replace_right(_, _, _, X, 0, _):- X < 2, !.
 1274replace_right(Es, A, P, X, Y, S):- cofact(X, t(U, L, R), S),
 1275	arrow_symbol(U, Arrow, Lu, Ru),
 1276	(	Arrow = (->) ->	Y = 0
 1277	;	replace_right(Es, A, P, L, L0, S),
 1278		(	Ru = A ->
 1279			zdd_insert_atoms(Es, R, R0, S),
 1280			cofact(Y, t(Lu - P, L0, R0), S)
 1281		;	replace_right(Es, A, P, R, R0, S),
 1282			cofact(Y, t(U, L0, R0), S)
 1283		)
 1284	).
 1285
 1286%
 1287replace_left(A, P, X, Y, S):- replace_left([P->A], A, P, X, Y, S).
 1288%
 1289replace_left(_, _, _, X, 0, _):- X < 2, !.
 1290replace_left(Es, A, P, X, Y, S):-
 1291	cofact(X, t(U, L, R), S),
 1292	arrow_symbol(U, Arrow, Lu, Ru),
 1293	(	Arrow = (->) -> Y = 0
 1294	;	replace_left(Es, A, P, L, L0, S),
 1295		zdd_compare(C, A, Lu, S),
 1296		(	C = (<) ->	R0 = 0
 1297		; 	C = (=)	->
 1298			zdd_insert_atoms(Es, R, W, S),
 1299			zdd_insert(P - Ru, W, R0, S)
 1300		;	replace_left(Es, A, P, R, W, S),
 1301			zdd_insert(U, W, R0, S)
 1302		),
 1303		zdd_join(L0, R0, Y, S)
 1304	).
 1305
 1306%
 1307qp_replace_right(_, _, X, 0, _):- X < 2, !.
 1308qp_replace_right(A, P, X, Y, S):- cofact0(X, U, R, S),
 1309		U = (Lu-Ru),
 1310		(	Ru = A -> cofact0(Y, Lu - P, R, S)
 1311		;	qp_replace_right(A, P, R, R0, S),
 1312			cofact0(Y, U, R0, S)
 1313		).
 1314%
 1315qp_replace_left(_, _, X, 0, _):- X < 2, !.
 1316qp_replace_left(A, P, X, Y, S):- cofact0(X, U, R, S),
 1317		U = Lu-Ru,
 1318		zdd_compare(C, A, Lu, S),
 1319		(	C = (<) ->	Y = 0
 1320		; 	C = (=)
 1321		->  normal_pair(P-Ru, B, S),
 1322			zdd_insert_as_list(B, R, Y, S)
 1323		;	qp_replace_left(A, P, R, W, S),
 1324			zdd_insert_as_list(U, W, Y, S)
 1325		).
 1326
 1327%
 1328qp_replace(_, _, X, X, _):- X < 2, !.
 1329qp_replace(A, P, X, Y, S):- cofact0(X, U, R, S),
 1330		U = Lu-Ru,
 1331		(	A = Lu
 1332		->  normal_pair(P-Ru, B, S),
 1333			zdd_insert(B, R, Y, S)
 1334		;	A = Ru
 1335		->  normal_pair(P-Lu, B, S),
 1336			zdd_insert(B, R, Y, S)
 1337		;	qp_replace(A, P, R, R0, S),
 1338			cofact0(Y, U, R0, S)
 1339		).
 1340%
 1341u_qp_replace(_, _, X, 0, _):- X < 2, !.
 1342u_qp_replace(A, P, X, Y, S):- cofact0(X, U, R, S),
 1343		U = Lu-Ru,
 1344		(	zdd_compare(<, A, Lu, S),
 1345			zdd_compare(<, P, Lu, S)
 1346		->  Y = 0		%, write(.) % Many hits.
 1347		;	(	A = Lu
 1348			->  normal_pair(P-Ru, B, S),
 1349				u_insert(B, R, Y, S)
 1350			;	A = Ru
 1351			->  normal_pair(P-Lu, B, S),
 1352				u_insert(B, R, Y, S)
 1353			;	u_qp_replace(A, P, R, R0, S),
 1354				u_insert(U, R0, Y, S)
 1355			)
 1356		)