1:- module(udg_path_count, []).    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
   21%
   22mate_less_than(_ - A, B -_):- A @< B.
   23
   24% One of the most basic helpers.
   25composable_pairs(A-B, A-C, B, C).
   26composable_pairs(A-B, C-A, B, C).
   27composable_pairs(B-A, A-C, B, C).
   28composable_pairs(B-A, C-A, B, C).
   29%
   30normal_pair(A-B, U-V):-!, ( B @< A -> U=B, V=A; U=A, V=B ).
   31normal_pair(A->B, U->V):- ( B @< A -> U=B, V=A; U=A, V=B ).
   32
   33
   34		/****************************************************
   35		*     replace_end/bypass:  Most basic operations.   *
   36		****************************************************/
   37
   38% ?- zdd((X<< +[[c-d]], @(subst_node([a->c], c, a, X, Y)), psa(X), psa(Y))).
   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	;	compare(<, 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		/**********************************
   59		*     simple count path by mate   *
   60		**********************************/
   61
   62% ?- rect_udg(rect(1,1), Ls,  M), udg_path_count_with_sort(Ls, M, C, _).
   63% ?- rect_udg(rect(2,1), Ls,  M), udg_path_count_with_sort(Ls, M, C, _).
   64% ?- rect_udg(rect(3,1), Ls,  M), udg_path_count_with_sort(Ls, M, C, _).
   65% ?- rect_udg(rect(4,1), Ls,  M), udg_path_count_with_sort(Ls, M, C, _).
   66% ?- rect_udg(rect(1,2), Ls,  M), udg_path_count_with_sort(Ls, M, C, _).
   67% ?- rect_udg(rect(1,3), Ls,  M), udg_path_count_with_sort(Ls, M, C, _).
   68% ?- rect_udg(rect(1,4), Ls,  M), udg_path_count_with_sort(Ls, M, C, _).
   69% ?- rect_udg(rect(2,2), Ls,  M), udg_path_count_with_sort(Ls, M, C, _).
   70% ?- time((rect_udg(rect(3,3), Ls,  M), udg_path_count_with_sort(Ls, M, C, _))).
   71% ?- rect_udg(rect(4,4), Ls,  M),
   72%	call_with_time_limit(600, udg_path_count_with_sort(Ls, M, C, _)).
   73% ?- rect_udg(rect(5,5), Ls,  M),
   74%	call_with_time_limit(100, udg_path_count_with_sort(Ls, M, C, _)).
   75% ?- bfs_rect_path_count(rect(1,1), C, _).
   76% ?- bfs_rect_path_count(rect(2,2), C, _).
   77% ?- bfs_rect_path_count(rect(3,3), C, _).
   78% ?- bfs_rect_path_count(rect(4,4), C, _).
   79
   80bfs_rect_path_count(R, C, Opts):- % Links is used as it is.
   81	rect_udg(R, Ls,  M),
   82	bfs_path_count(Ls, M, C, Opts).
   83
   84% ?- bfs_path_count([a-b, b-c,  a-c], a-c, C, _).
   85% ?- bfs_path_count([a-b, a-c, b-d, c-d, c-e, e-f, d-f, a-f], a-f, C, _).
   86bfs_path_count(Links, A-B, C, Opts):- % Links is used as it is.
   87	memberchk(state(S), Opts),
   88	memberchk(path(Y), Opts),
   89	memberchk(mate(X), Opts),
   90	open_state(S),
   91	findall(W, (member(M, Links), (M = (W-_); M=(_-W))), Ps),
   92	sort([A,B|Ps], Qs),
   93	sort([A,B], [N0, N1]),
   94	set_key(final, N0-N1, S),
   95	findall(U-U, member(U, Qs), M),
   96	sort(M, M0),
   97	zdd_insert_atoms(M0, 1, Mates, S),
   98	sort(Links, Links0),
   99	bfs_path_count(Links0, Mates, X, 0, Y, S),
  100	card(Y, C, S).
  101
  102%
  103bfs_path_count([], X, X, Y, Y, _).
  104bfs_path_count([L|Ls], X, X0, Y, Y0, S):-
  105	bfs_path_count(Ls, X, X1, Y, Y1, S),
  106	add_links([L], X1, X0, Y1, Y0, S).
  107
  108% sort give links, and pass it.
  109% ?- rect_udg(rect(1, 3), Ls,  M),
  110%	call_with_time_limit(100, udg_path_count_with_sort(Ls, M, C, _)).
  111%@ C = 8.
  112% ?- rect_udg(rect(2,2), Ls,  M),
  113%	call_with_time_limit(100, udg_path_count_with_sort(Ls, M, C, _)).
  114% ?- rect_udg(rect(2,2), Ls,  M),
  115% ?- rect_udg(rect(3,3), Ls,  M),
  116%	call_with_time_limit(100, udg_path_count_with_sort(Ls, M, C, _)).
  117% ?- rect_udg(rect(4,4), Ls,  M),
  118%	call_with_time_limit(100, udg_path_count_with_sort(Ls, M, C, _)).
  119% ?- rect_udg(rect(2,2), X, Y), udg_path_count(X, Y, C, _).
  120
  121% sort give links, and pass it.
  122udg_path_count_with_sort(Links, Final, C, Opts):-
  123	sort(Links, Links0),
  124	reverse(Links0, Links1),
  125	udg_path_count(Links1, Final, C, Opts).
  126%
  127udg_path_count(Links, A-B, C, Opts):- % Links is used as it is.
  128	memberchk(state(S), Opts),
  129	memberchk(path(Y), Opts),
  130	memberchk(mate(X), Opts),
  131	open_state(S),
  132	findall(W, (member(M, Links), (M = (W-_); M=(_-W))), Ps),
  133	sort([A,B|Ps], Qs),
  134	sort([A,B], [N0, N1]),
  135	set_key(final, N0-N1, S),
  136	findall(U-U, member(U, Qs), M),
  137	sort(M, M0),
  138	zdd_insert_atoms(M0, 1, Mates, S),
  139	bfs_sort_links([N1], Links, [], L_links),
  140	reverse(L_links, L_links_r),
  141	add_layered_links(L_links_r, Mates, X, 0, Y, S),
  142	card(Y, C, S).
  143%
  144add_layered_links([], X, X, Y, Y, _).
  145add_layered_links([L|Ls], X, X0, Y, Y0, S):-
  146	add_links(L, X, X1, Y, Y1, S),
  147	add_layered_links(Ls, X1, X0, Y1, Y0, S).
  148
  149% ?- zdd X<<{[a-a, b-b]}, set_key(final, a-b), add_links([a-b], X, X0, 0, Y), psa(Y).
  150
  151% ?- zdd set_key(final, c-d), X<<{[a-a, b-b]}, add_links([a-b], X, X0, 0, Y), psa(X0).
  152
  153% ?-rect_udg(rect(3,3), Ls, E), findall(U-U, (member(D, Ls), (D=(U-_); D=(_-U))), M), sort(M, M0),
  154% zdd((X<<{M0}, set_key(final,E), @(add_links(Ls, X, X0, 0, Y)), card(Y, Card))).
  155%@ Ls = [p(0, 0)-p(0, 1), p(0, 0)-p(1, 0), p(0, 1)-p(0, 2), p(0, 1)-p(1, 1), p(0, 2)-p(0, 3), p(0, 2)-p(1, 2), p(0, 3)-p(1, 3), p(..., ...)-p(..., ...), ... - ...|...],
  156%@ E = p(0, 0)-p(3, 3),
  157%@ M = [p(0, 0)-p(0, 0), p(0, 1)-p(0, 1), p(0, 0)-p(0, 0), p(1, 0)-p(1, 0), p(0, 1)-p(0, 1), p(0, 2)-p(0, 2), p(0, 1)-p(0, 1), p(..., ...)-p(..., ...), ... - ...|...],
  158%@ M0 = [p(0, 0)-p(0, 0), p(0, 1)-p(0, 1), p(0, 2)-p(0, 2), p(0, 3)-p(0, 3), p(1, 0)-p(1, 0), p(1, 1)-p(1, 1), p(1, 2)-p(1, 2), p(..., ...)-p(..., ...), ... - ...|...],
  159%@ X = 17,
  160%@ X0 = 15726402,
  161%@ Y = 14297372,
  162%@ Card = 184.
  163
  164add_links([], X, X, C, C, _).
  165add_links([L|Ls], X, X0, C, C0, S):-
  166	add_link(L, X, X1, S),
  167	get_key(final, E, S),
  168	separate_finals(X1, Finals, X2, E, S),   % experimental
  169	zdd_join(C, Finals, C1, S),
  170	zdd_join(X, X2, X3, S),
  171	add_links(Ls, X3, X0, C1, C0, S).
  172
  173
  174% ?- zdd X << +[*[a-a, b-b, c-c]],
  175%	simple_add_links([a-b,a-c,b-c], X, X0), psa(X0).
  176
  177simple_add_links([], X, X, _).
  178simple_add_links([L|Ls], X, X0, S):-
  179	add_link(L, X, X1, S),
  180	zdd_join(X, X1, X2, S),
  181	simple_add_links(Ls, X2, X0, S).
  182
  183
  184% ?- zdd X<<{[a-b, c-d]}, psa(X), add_link(b-c, X, Y), psa(Y).
  185% ?- zdd X<< +[*[a-b, c-d], *[e-f]], psa(X), add_link(b-c, X, Y), psa(Y).
  186% ?- zdd X<< +[*[a-b, c-d], *[a-a, b-b], *[e-f]], psa(X), add_link(b-c, X, Y), psa(Y).
  187% ?- zdd X<< +[*[a-a, b-b, c-c]], psa(X), add_link(b-c, X, Y), psa(Y).
  188
  189add_link(_, X, 0, _):- X<2, !.
  190add_link(U, X, Y, S):- % memo is useless here
  191	cofact(X, t(A, L, R), S),
  192	(	A = (_->_) -> Y = 0
  193	;	add_link(U, L, L0, S),
  194		U = Ul-Ur,
  195		(	mate_less_than(U, A) -> R0 = 0
  196		; 	A = U -> R0 = 0
  197		; 	composable_pairs(U, A, U0, V0) ->
  198			subst_node([Ul->Ur], U0, V0, R, R0, S)
  199		;	add_link(U, R, R1, S),
  200			zdd_insert(A, R1, R0, S)
  201		),
  202		zdd_join(L0, R0, Y, S)
  203	).
  204
  205% ?- zdd X<<{[a-b, c-c, x->y]}, separate_finals(X, Y, Z, a-b), psa(X), psa(Z), psa(Y).
  206% ?- zdd X<<{[a-b, c-c, x->y], [c-d, a->b], [a-b, c-d], [a-b, d-d]},
  207%	separate_finals(X, Y, Z, a-b), psa(X), psa(Z), psa(Y).
  208
  209separate_finals(X, Fin, Z, E, S):- zdd_divisible_by_list(X, [E], X0, S),
  210	separate_non_finals(X0, Non, E, S),
  211	zdd_subtr(X0, Non, Fin, S),
  212	zdd_subtr(X, X0, Z, S).
  213%
  214separate_non_finals(X, 0, _, _):- X<2, !.
  215separate_non_finals(X, Y, E, S):- cofact(X, t(A, L, R), S),
  216	separate_non_finals(L, L0, E, S),
  217	(	A = (U-V) ->
  218		(	(A = E; U=V) -> separate_non_finals(R, R0, E, S)
  219		;	R0 = R
  220		)
  221	;	R0 = 0
  222	),
  223	cofact(Y, t(A, L0, R0), S).
  224
  225%
  226collect_closed_mate(X, 0, _, _):- X<2, !.
  227collect_closed_mate(X, Y, E, S):- cofact(X, t(A, L, R), S),
  228	(	A = (_->_)	-> Y = 0
  229	;	A = E ->
  230		collect_mate_free(R, R0, S),
  231		cofact(Y, t(A, 0, R0), S)
  232	; 	collect_closed_mate(L, L0, E, S),
  233		(	A = (U-U) ->
  234			collect_closed_mate(R, R0, E, S)
  235		;	R0 = 0
  236		),
  237		cofact(Y, t(A, L0, R0), S)
  238	).
  239%
  240collect_mate_free(X, Y, _):- X<2, !, Y=X.
  241collect_mate_free(X, Y, S):- cofact(X, t(A, L, R), S),
  242	(	A = (_->_) -> Y = X
  243	;	collect_mate_free(L, L0, S),
  244		(	A = (U-U) ->
  245			collect_mate_free(R, R0, S)
  246		;	R0 = 0
  247		),
  248		cofact(Y, t(A, L0, R0), S)
  249	).
  250
  251		/***********************
  252		*     layered links    *
  253		***********************/
  254
  255% ?- bfs_sort_links([a], [a-b, b-c, d-e, a-c], [],  Out).
  256% ?- time((rect_udg(rect(1,1), Ls, A-B), bfs_sort_links([B], Ls, [], Y))).
  257% ?- time((rect_udg(rect(100,100), Ls, A-B),
  258%	bfs_sort_links([B], Ls, [], Y))), length(Y, Len).
  259%
  260add_new(X, Y, Y):- memberchk(X, Y), !.
  261add_new(X, Y, [X|Y]).
  262
  263bfs_sort_links([], _, Y, Y).
  264bfs_sort_links(X, M, Y, Z):-
  265	bfs_layer_list(X, [], L, [], K, M, M0),
  266	bfs_sort_links(K, M0, [L|Y], Z).
  267
  268% ?- bfs_layer_list([a], [], L0, [], K0, [a-b], M0).
  269% ?- bfs_layer_list([a, b], [], L0, [], K0, [a-b, b-c, a-c], M0).
  270% ?- bfs_layer_list([a, b], [], L0, [], K0, [a-b, b-c, d-e, a-c], M0).
  271%
  272bfs_layer_list([], L, L, K, K, M, M).
  273bfs_layer_list([N|Ns], L, L0, K, K0, M, M0):-
  274	bfs_layer(N, L, L1, K, K1, M, M1),
  275	bfs_layer_list(Ns, L1, L0, K1, K0, M1, M0).
  276%
  277bfs_layer(N, L, L0, K, K0, M, M0):-
  278	select(X, M, M1),
  279	(X = (P-N); X = (N-P)),
  280	!,
  281	add_new(X, L, L1),
  282	add_new(P, K, K1),
  283	bfs_layer(N, L1, L0, K1, K0, M1, M0).
  284bfs_layer(_, L, L, K, K, M, M).
  285
  286		/*************************
  287		*     linear grid udg    *
  288		*************************/
  289
  290% ?- zdd rect_col_bridge(rect(0,0), Cols, Brs).
  291% ?- zdd rect_col_bridge(rect(0,1), Cols, Brs).
  292% ?- zdd rect_col_bridge(rect(1,1), Cols, Brs).
  293% ?- time((zdd rect_col_bridge(rect(20,20), Cols, Brs))).
  294%@ % 4,157,825,846 inferences, 452.733 CPU in 468.459 seconds (97% CPU, 9183838 Lips)
  295
  296% ?- time( (zdd rect_col_bridge(rect(20,20), Cols, fBrs))).
  297%@ % 4,157,825,846 inferences, 551.569 CPU in 559.546 seconds (99% CPU, 7538185 Lips)
  298
  299rect_col_bridge(Rect, Cols, Brs, S):-
  300	rect_col_list(Rect, Cols, S),
  301	rect_bridge(Rect, Brs).
  302%
  303rect_bridge(rect(W, H), Brs):-
  304	(	W > 0 ->
  305		W0 is W-1,
  306		mk_bridge_list(0-W0, 0-H, Brs)
  307	;	Brs = []
  308	).
  309
  310
  311% ?- zdd rect_col_list(rect(1,1), Vs), s_map(psa, Vs).
  312
  313% ?- time((zdd rect_col_list(rect(15,15), Vs))).
  314
  315rect_col_list(rect(W, H), Vs, S):-
  316	mk_column_list(rect(p(0,0), p(W, H)), Cols),
  317	s_map(linear_grid_udg, Cols, Vs, S).
  318
  319% ?- mk_column_list(rect(p(0,0), p(1,1)), Cols).
  320mk_column_list(rect(p(J0, K0), p(J1, K1)), Cols):-
  321	numlist(J0, J1, Js),
  322	numlist(K0, K1, Ks),
  323	maplist(mk_column(Ks), Js, Cols).
  324%
  325mk_column(Ks, J, Col):- findall(p(J, K), member(K, Ks), Col).
  326
  327% ?- zdd linear_grid_udg([a], X), psa(X).
  328% ?- zdd linear_grid_udg([a,b], X), psa(X).
  329% ?- zdd linear_grid_udg([a,b,c,d], X), psa(X).
  330
  331linear_grid_udg([], 1, _).
  332linear_grid_udg([J|Js], X, S):- linear_grid_udg(Js, X0, S),
  333	add_node_grid_udg(J, Js, X0, X, S).
  334%
  335add_node_grid_udg(J, Js, X, Y, S):- zdd_insert(J-J, X, Y0, S),
  336	add_links_grid_udg(J, Js, X, 0, Y1, S),
  337	zdd_join(Y0, Y1, Y, S).
  338%
  339add_links_grid_udg(_, [], _, Y, Y, _):-!.
  340add_links_grid_udg(J, [K|_], X, Y, Y0, S):-add_link_grid_udg(J-K, X, Y1, S),
  341	zdd_join(Y, Y1, Y0, S).
  342
  343%
  344add_link_grid_udg(_, 0, 0, _):-!.
  345add_link_grid_udg(J-K, 1, Y, S):-!, zdd_ord_insert([J-K, J->K], 1, Y, S).
  346add_link_grid_udg(J-K, X, Y, S):- % memo is useless here.
  347	cofact(X, t(U, L, R), S),
  348	U=A-B,
  349	add_link_grid_udg(J-K, L, L0, S),
  350	(	K = A ->
  351		zdd_ord_insert([J-B, J->K], R, R0, S)
  352	;   throw(unexpected_link)
  353	),
  354	zdd_join(L0, R0, Y, S).
  355
  356% ?- mk_bridge(2, 0-3, Bridge).
  357mk_bridge(I, J-K, Bridge):- findall(p(I,B)-p(I0,B), ( between(J, K, B), succ(I, I0) ), Bridge).
  358
  359% ?- mk_bridge_list(0-1, 0-3, Bs), maplist(writeln, Bs).
  360%@ [p(0,0)-p(1,0),p(0,1)-p(1,1),p(0,2)-p(1,2),p(0,3)-p(1,3)]
  361%@ [p(1,0)-p(2,0),p(1,1)-p(2,1),p(1,2)-p(2,2),p(1,3)-p(2,3)]
  362mk_bridge_list(Min-Max, J-K, Bs):-
  363	findall(B, (between(Min, Max, I), mk_bridge(I, J-K, B)), Bs).
  364
  365
  366% ?- test(rect(0,0), X, S), psa(X, S).
  367% ?- test(rect(1,0), X, S), psa(X, S).
  368% ?- test(rect(2,0), X, S), psa(X, S).
  369% ?- test(rect(30,0), X, S), psa(X, S).
  370% ?- test(rect(1,1), X, S), psa(X, S).
  371% ?- test(rect(1,1), X, S), card(X, C, S).
  372% ?- test(rect(2,2), X, S), card(X, C, S).
  373% ?- test(rect(3,3), X, S), card(X, C, S).
  374% ?- test(rect(4,4), X, S), card(X, C, S).
  375% ?- time((test(rect(5,5), X, S), card(X, C, S))).
  376%@ % 513,644,743 inferences, 71.589 CPU in 72.633 seconds (99% CPU, 7174907 Lips)
  377
  378test(rect(W, H), X, S):- open_state(S),
  379	set_key(max_node, p(W, H), S),
  380	W0 is W-1,
  381	set_key(bridge_id, W0, S),
  382	rect_col_bridge(rect(W, H), Cols, Brs, S),
  383	reverse(Cols, RCols),
  384	maplist(reverse, Brs, Brs0),
  385	reverse(Brs0, RBrs),
  386	RCols=[Col|Cols0],
  387	fold_columns(RBrs, Cols0, Col, X0, S),
  388	prune_final(p(0, 0), p(W, H), X0, X, S).
  389
  390%
  391fold_columns([], [], X, X, _).
  392fold_columns([B|Bs], [C|Cs], X, Y, S):-
  393	bridge_prune(B, C, X, X0, S),
  394	get_key(bridge_id, K, S),
  395	K0 is K-1,
  396	set_key(bridge_id, K0, S),
  397	fold_columns(Bs, Cs, X0, Y, S).
  398
  399
  400% ?- path_count(rect(0,0), X, S), psa(X, S), get_compare(F, S).
  401% ?- path_count(rect(1,0), X, S), card(X, C, S).
  402% ?- path_count(rect(2,0), X, S), card(X, C, S).
  403% ?- path_count(rect(30,0), X, S), card(X, C, S).
  404% ?- path_count(rect(1,1), X, S), card(X, C, S).
  405% ?- path_count(rect(2,2), X, S), card(X, C, S).
  406% ?- path_count(rect(3,3), X, S), card(X, C, S).
  407% ?- time((path_count(rect(4,4), X, S), card(X, C, S))).
  408% ?- time((path_count(rect(5,5), X, S), card(X, C, S))).
  409%@ % 659,736,449 inferences, 56.014 CPU in 56.567 seconds (99% CPU, 11778141 Lips)
  410%@ % 659,736,449 inferences, 78.308 CPU in 78.596 seconds (100% CPU, 8424911
  411%@ % 659,704,102 inferences, 61.864 CPU in 62.239 seconds (99% CPU, 10663748 Lips)
  412%@ C = 1262816.
  413
  414path_count(rect(W, H), X, S):- open_state(S),
  415	set_key(max_node, p(W, H), S),
  416	set_key(bridge_id, W, S),
  417	rect_bridge(rect(W, H), Brs),
  418	maplist(reverse, Brs, Brs0),
  419	reverse(Brs0, RBrs),
  420	next_column(Col, S),
  421	fold_columns(RBrs, Col, X0, S),
  422	prune_final(p(0, 0), p(W, H), X0, X, S).
  423
  424% ?- open_state(S), set_key(bridge_id, 2, S), set_key(max_node, p(4,4), S), next_column(X, S), psa(X, S).
  425next_column(X, S):- get_key(bridge_id, I, S),
  426	get_key(max_node, N, S),
  427	N = p(_, H),
  428	next_column(I, H, X, S).
  429%
  430next_column(I, H, X, S):- findall(p(I, J), between(0, H, J), Ps),
  431	linear_grid_udg(Ps, X, S).
  432
  433%
  434fold_columns([], X, X, _).
  435fold_columns([B|Bs], In, Y, S):-
  436	zdd_slim(In, X, S),
  437	get_key(bridge_id, K, S),
  438	K0 is K-1,
  439	set_key(bridge_id, K0, S),
  440	next_column(C, S),
  441	bridge_prune(B, C, X, X0, S),
  442	fold_columns(Bs, X0, Y, S).
  443
  444%
  445bridge_prune(Bs, X, Y, Z, S):- bridge(Bs, X, Y, 0, Z0, S),
  446	get_key(max_node, P, S),
  447	get_key(bridge_id, I, S),
  448	prune(I, P, Z0, Z1, S),
  449	zdd_join(X, Z1, Z, S).
  450
  451% ?- zdd X << +[*[a-b]], Y<< +[*[x-y]], bridge([a-x], X, Y, 0, Z), psa(Z).
  452
  453% ?- zdd X<< +[*[a-b],*[a-c]], Y<< +[*[x-y], *[x-z]], bridge([a-x], X, Y, 0, Z), psa(Z).
  454% ?- zdd X<< +[*[a-b],*[a-c]], Y<< +[*[x-y], *[x-z]], bridge([a-x, b-y], X, Y, 0, Z), psa(Z).
  455bridge([], _, _, Z, Z, _):-!.
  456bridge([U|Us], X, Y, Z, Z0, S):-
  457	add_link(U, Z, Z1, S),
  458	bridge(U, X, Y, W, S),
  459	zdd_join_list([W, Z1, Z], Z2, S),
  460	bridge(Us, X, Y, Z2, Z0, S).
  461
  462% ?- zdd X<< +[*[a-b]], Y<< +[*[x-y]], bridge(a-x, X, Y, Z), psa(Z).
  463% ?- zdd X<< +[*[a-b], *[a-c]], Y<< +[*[x-y]],  bridge(a-x, X, Y, Z), psa(Z).
  464% ?- zdd X<< +[*[a-b], *[a-c]], Y<< +[*[x-y], *[x-u]],  bridge(a-x, X, Y, Z), psa(Z).
  465
  466bridge(_, X, Y, 0, _):- (X<2; Y<2), !.
  467bridge(U, X, Y, Z, S):- cofact(X, t(A, L, R), S),
  468		(	A = (_->_) -> Z = 0
  469		;	A = A0-A1,
  470			U = J-K,
  471			bridge(U, L, Y, L0, S),
  472			(	J @< A0 ->  R0 = 0
  473			;	J = A0 ->
  474				subst_node([J->K], K, A1, Y, Y1, S),
  475				zdd_merge(Y1, R, R0, S)
  476			;	J = A1 ->
  477				subst_node([J->K], K, A0, Y, Y1, S),
  478				zdd_merge(Y1, R, R0, S)
  479			;	bridge(U, R, Y, Y0, S),
  480				zdd_insert(A, Y0, R0, S)
  481			),
  482			zdd_join(L0, R0, Z, S)
  483		).
  484
  485% ?- zdd X<< *[*[p(1, 0)-p(2,2)]], prune(1, p(2,2), X, Y), psa(Y).
  486% ?- zdd X<< +[*[p(1, 0)-p(2,1)], *[p(1,1)-p(1,2), p(1,0)-p(2,2)],
  487%	*[p(1,1)-p(2,2)]], psa(X), prune(1, p(2,2), X, Y), psa(Y).
  488
  489prune(_, _, X, X, _):-X<2, !.
  490prune(I, P, X, Y, S):-cofact(X, t(A, L, R), S),
  491	(	A = (_->_) -> Y = X
  492	;	prune(I, P, L, L0, S),
  493		A = A0-A1,
  494		A0 = p(J, _),
  495		A1 = p(K, _),
  496		(	J = I ->
  497			(	( K = I; A1 = P) ->
  498				prune(I, P, R, R1, S),
  499				zdd_insert(A, R1, R0, S)
  500			;	R0 = 0
  501			)
  502		;	A0 \== A1 -> R0 = 0
  503		;	prune(I, P, R, R0, S)
  504		),
  505		zdd_join(L0, R0, Y, S)
  506	).
  507
  508% ?- zdd X<< +[*[a-b, a->b]], prune_final(a, b, X, Y), psa(Y).
  509
  510prune_final(_, _, X, X, _):- X<2, !.
  511prune_final(P, Q, X, Y, S):- cofact(X, t(A, L, R), S),
  512	(	A = (_->_) -> Y = X
  513	;	prune_final(P, Q, L, L0, S),
  514		A = A1-A2,
  515		(	 A1 = P ->
  516			 (	A2 = Q
  517			 -> prune_final(P, Q, R, R0, S)
  518			 ;	R0 = 0
  519			 )
  520		;	A1 = A2 ->
  521			prune_final(P, Q, R, R0, S)
  522		;	R0 = 0
  523		),
  524		zdd_join(L0, R0, Y, S)
  525	)