1:- module(orth, []). 2
3:- use_module(zdd('zdd-array')). 4:- use_module(zdd(zdd)). 5:- use_module(pac(op)). 6
7 10
13setup_ctrl_opt(X, ctrl(GC, S, T, Rect)):-
14 memberchk(rect(W, H), X),
15 Rect = rect(W, H),
16 ( memberchk(gc(GC), X) -> true
17 ; GC = 0
18 ),
19 ( memberchk(S-T, X) -> true
20 ; S = p(0,0),
21 T = p(W, H)
22 ).
23
25get_ctrl(X, end, Y) :-!, arg(3, X, Y).
26get_ctrl(X, gc, Y) :-!, arg(1, X, Y).
27get_ctrl(X, start, Y):-!, arg(2, X, Y).
28get_ctrl(X, rect, Y):- arg(4, X, Y).
29
32arrow_symbol( _ -> _).
34arrow_symbol(A, A0):- functor(A, A0, 2).
35arrow_symbol(A, A0, A1, A2):- functor(A, A0, 2),
36 arg(1, A, A1),
37 arg(2, A, A2).
38
40composable_pairs(A-B, A-C, B, C).
41composable_pairs(A-B, C-A, B, C).
42composable_pairs(B-A, A-C, B, C).
43composable_pairs(B-A, C-A, B, C).
45normal_pair(A-B, U-V):-!, ( B @< A -> U=B, V=A; U=A, V=B ).
46normal_pair(A->B, U->V):- ( B @< A -> U=B, V=A; U=A, V=B ).
47
52
54frontier_node(_-[_, P], P):-!.
55frontier_node(p(_, J)-[p(K, J)], p(K, J)):-!.
56frontier_node(p(I, J)-[p(I, _)], p(K, J)):-!, K is I+1.
57frontier_node(p(I, J)-[], p(K, J)):- K is I + 1.
58
61rect_nodes(rect(W, H), Ns):-
62 findall(p(I,J),
63 ( between(0, W, I),
64 between(0, H, J)
65 ),
66 Ns).
67
70rect_udg(rect(W, H), UDG):-
71 findall( p(I,J)-Suc,
72 ( between(0, W, I),
73 between(0, H, J),
74 findall( p(K,L),
75 ( L=J, K is I + 1, K =< W
76 ; K=I, L is J + 1, L =< H
77 ),
78 Suc0),
79 sort(Suc0, Suc)
80 ),
81 UDG).
82
83
84 108
123
129
136
138
141
144
146
147 151rect_mate(Rect, X):- udg_mate([gc(0), Rect], X).
153rect_mate(Rect, Opts, X):- udg_mate([Rect|Opts], X).
155udg_mate(Opts, X):-
156 setup_ctrl_opt(Opts, Ctrl),
157 get_ctrl(Ctrl, rect, Rect),
158 rect_udg(Rect, Dg0),
159 reverse(Dg0, Dg),
160 udg_mate(Ctrl, Dg, 1, X0),
161 get_ctrl(Ctrl, start, Start),
162 get_ctrl(Ctrl, end, End),
163 prune_final(Start, End, X0, X).
165udg_mate(_, [], X, X).
166udg_mate(Ctrl, [N-Ps|UDG], X, Y):-
167 get_ctrl(Ctrl, end, End),
168 frontier_node(N-Ps, F),
169 add_node(F-End, N, Ps, X, X0),
170 prune_by_classify_link(F, End, X0, X1),
171 ctrl_gc(Ctrl, N, X1, X2),
172 udg_mate(Ctrl, UDG, X2, Y).
173
174 177
178add_node(_, N, [], X, Y):-!, zdd_insert(N-N, X, Y).
179add_node(FE, p(0,0), [P], X, Y):-!, N=p(0,0),
180 subst_node(FE, [N->P], P, N, X, Y).
181add_node(FE, N, [P], X, Y):-!,
182 subst_node(FE, [N->P], P, N, X, X0),
183 zdd_insert(N-N, X, X1),
184 zdd_join(X0, X1, Y).
185add_node(FE, p(0,0), [P, Q], X, Y):-!, N=p(0,0),
186 subst_node(FE, [N->P], P, N, X, X0),
187 subst_node(FE, [N->Q], Q, N, X, X1),
188 zdd_join(X0, X1, Y).
189add_node(FE, N, [P, Q], X, Y):-
190 subst_node(FE, [N->P], P, N, X, X0),
191 subst_node(FE, [N->Q], Q, N, X, X1),
192 bypass(FE, [N->P, N->Q], P-Q, X, X2),
193 zdd_insert(N-N, X, X3),
194 zdd_join_list([X0, X1, X2, X3], Y).
195
199subst_node(_, _, _, _, X, 0):- X < 2, !.
200subst_node(FE, Es, A, P, X, Y):- FE = Fr-End, 201 cofact(X, t(U, L, R)),
202 subst_node(FE, Es, A, P, L, L0),
203 classify_link(on_frontier_for_subst, Fr, End, U, Case),
204 arrow_symbol(U, _, Lu, Ru),
205 ( ( Case = 0 ; Case = arrow ) -> R0 = 0
206 ; Case = ignore ->
207 subst_node(FE, Es, A, P, R, R0)
208 ; ( Ru = A ->
209 normal_pair(Lu-P, V),
210 zdd_ord_insert([V|Es], R, R0)
211 ; Lu = A ->
212 normal_pair(P-Ru, V),
213 zdd_ord_insert([V|Es], R, R0)
214 ; subst_node(FE, Es, A, P, R, R1),
215 zdd_insert(U, R1, R0)
216 )
217 ),
218 zdd_join(L0, R0, Y).
220bypass(_, _, _, X, 0):- X<2, !.
221bypass(FE, Bypass, U, X, Y):- FE = Fr-E,
222 cofact(X, t(A, L, R)),
223 bypass(FE, Bypass, U, L, L0),
224 classify_link(on_frontier, Fr, E, A, Case),
225 ( ( Case = 0; Case = arrow ) -> R0 = 0 226 ; Case = ignore -> bypass(FE, Bypass, U, R, R0) 227 ; ( A = U -> R0 = 0 228 ; composable_pairs(U, A, U0, V0) ->
229 subst_node(FE, Bypass, U0, V0, R, R0)
230 ; bypass(FE, Bypass, U, R, R1),
231 zdd_insert(A, R1, R0)
232 )
233 ),
234 zdd_join(L0, R0, Y).
235
237add_link(_, _, X, 0):- X<2, !.
238add_link(FE, U, X, Y):- FE = F-E,
239 cofact(X, t(A, L, R)),
240 add_link(FE, U, L, L0),
241 classify_link(on_frontier, F, E, A, Case),
242 ( ( Case = 0; Case = arrow ) -> R0 = 0 243 ; Case = ignore -> add_link(FE, U, R, R0) 244 ; U = Ul-Ur,
245 ( A = U -> R0 = 0 246 ; composable_pairs(U, A, U0, V0) ->
247 subst_node(FE, [Ul->Ur], U0, V0, R, R0)
248 ; add_link(FE, U, R, R1),
249 zdd_insert(A, R1, R0)
250 )
251 ),
252 zdd_join(L0, R0, Y).
253
254 257
259prune_final(_, _, X, 0):- X<2, !.
260prune_final(P, Q, X, Y):- cofact(X, t(A, L, R)),
261 prune_final(P, Q, L, L0),
262 ( A = (_->_) -> R0 = 0
263 ; A = P-Q -> prune_final0(R, R0)
264 ; A = U-U -> prune_final(R, R0)
265 ; R0 = 0
266 ),
267 zdd_join(L0, R0, Y).
269prune_final0(X, X):- X<2, !.
270prune_final0(X, Y):- cofact(X, t(A, L, R)),
271 prune_final0(L, L0),
272 ( A = (_->_) -> zdd_insert(A, R, R0)
273 ; A = (B-B) -> prune_final0(R, R0)
274 ; R0 = 0
275 ),
276 zdd_join(L0, R0, Y).
278ctrl_gc(Ctrl, P, X, Y):- get_ctrl(Ctrl, gc, GC),
279 ctrl_gc_case(GC, P, X, Y).
281ctrl_gc_case(all, P, X, Y):-!,
282 writeln(all),
283 format("GC at ~w \n", [P]),
284 slim_gc(X, Y). 286
287ctrl_gc_case(K, P, X, Y):- integer(K), !,
288 P = p(_, J),
289 ( J = K ->
290 format("GC at ~w \n", [P]),
292 slim_gc(X, Y) 293 ; Y=X
294 ).
295ctrl_gc_case(_, _, X, X).
296
297 300
302
305
307on_frontier(P, p(1, K)):-!, 308 ( P = p(1,J) -> J < K
309 ; P = p(0,J),
310 J =< K+1
311 ).
318on_frontier(P, F):- P @< F.
320on_frontier_for_subst(P, p(1, K)):-!, 321 ( P=p(1,J) -> J =< K
322 ; P=p(0,J), J =< K+1
323 ).
324on_frontier_for_subst(P, F):- P @=< F.
325
326:- meta_predicate classify_link(2, ?, ?, ?, ?). 327classify_link(_, _, _, _->_, arrow):-!.
328classify_link(Pred, F, End, A-B, Case):- call(Pred, A, F), !,
329 ( call(Pred, B, F) -> Case = keep
330 ; B = End -> Case = keep
331 ; Case = 0
332 ).
333classify_link(_, _, E, E-E, 0):-!. 334classify_link(_, _, _, A-A, ignore):-!.
335classify_link(_, _, _, _, 0).
336
341classify_link_for_bypass(F, E, A, Case):- classify_link(on_frontier, F, E, A, Case).
343classify_link_for_subst(X, Y, Z, U):- classify_link(on_frontier_for_subst, X, Y, Z, U).
344
346prune_by_classify_link(_, _, X, X):- X<2, !.
347prune_by_classify_link(F, End, X, Y):- cofact(X, t(A, L, R)),
348 prune_by_classify_link(F, End, L, L0),
349 classify_link(on_frontier, F, End, A, Case), 350 ( Case = arrow -> zdd_insert(A, R, R0)
351 ; Case = keep -> 352 prune_by_classify_link(F, End, R, R1),
353 zdd_insert(A, R1, R0)
354 ; Case = ignore -> 355 prune_by_classify_link(F, End, R, R0)
356 ; R0 = 0 357 ),
358 zdd_join(L0, R0, Y)