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 11
14arrow_symbol( _ -> _).
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).
21mate_less_than(_ - A, B -_):- A @< B.
22
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).
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 36
38
39subst_node(_, _, _, X, 0, _):- X<2, !.
40subst_node(Es, A, P, X, Y, S):- 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
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
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
97
103
120
139
149
150reverse_successors(X-A, X-B):- reverse(A, B).
151
153rect_mate(Rect, X, S):-rect_mate(Rect, X, [slim(0)], S).
154
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).
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
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
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).
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
216
217add_link(_, X, 0, _):- X<2, !.
218add_link(U, X, Y, S):- 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
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
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).
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.
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 )