1 | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(avl_tools,[avl_height_less_than/2, | |
6 | avl_height_compare/3, | |
7 | avl_height_compare_up_to/5, | |
8 | quick_avl_approximate_size/2, avl_fetch_pair/3, | |
9 | avl_delete_pair/4, | |
10 | avl_apply/5, | |
11 | avl_image_interval/4]). | |
12 | ||
13 | :- use_module(module_information,[module_info/2]). | |
14 | :- module_info(group,kernel). | |
15 | :- module_info(description,'This module provides AVL-tree utilities used by the kernel.'). | |
16 | ||
17 | :- use_module(library(avl)). | |
18 | ||
19 | :- use_module(error_manager). | |
20 | :- use_module(self_check). | |
21 | :- use_module(kernel_waitflags,[add_wd_error_span/4]). | |
22 | ||
23 | % ------------------------------- | |
24 | ||
25 | test_avl_set(node(((int(2),int(3)),int(6)),true,0,node(((int(1),int(2)),int(2)),true,0,empty,empty),node(((int(3),int(4)),int(12)),true,0,empty,empty))). | |
26 | ||
27 | :- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_less_than(A,3) )). | |
28 | :- assert_must_succeed(( avl_tools:avl_height_less_than(empty,1) )). | |
29 | :- assert_must_fail(( avl_tools:test_avl_set(A), avl_tools:avl_height_less_than(A,2) )). | |
30 | :- assert_must_fail(( avl_tools:avl_height_less_than(empty,0) )). | |
31 | ||
32 | % a custom version of avl_height; advantage it will stop when reaching MaxHeight | |
33 | ||
34 | avl_height_less_than(empty, MaxHeight) :- MaxHeight>0. | |
35 | avl_height_less_than(node(_,_,B,L,R), H0) :- H0>1, | |
36 | H1 is H0-1, | |
37 | ( B >= 0 -> avl_height_less_than(R, H1) | |
38 | ; avl_height_less_than(L, H1) | |
39 | ). | |
40 | ||
41 | ||
42 | % efficient way of comparing AVL heights without having to fully traverse larger AVL | |
43 | ||
44 | :- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_compare(A,A,eq) )). | |
45 | :- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_compare(empty,A,lt) )). | |
46 | :- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_compare(A,empty,gt) )). | |
47 | ||
48 | avl_height_compare(A,B,Res) :- avl_height_compare_up_to(A,B,0,0,_,Res). | |
49 | ||
50 | :- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_compare_up_to(empty,A,2,0,lt) )). | |
51 | :- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_compare_up_to(empty,A,3,0,eq) )). | |
52 | ||
53 | % avl_height_compare_up_to(Avl1,Avl2,MaxDiff,ResSz,ResCmp) -> ResSz: Height of smaller AVL, ResCmp = eq,lt,gt | |
54 | avl_height_compare_up_to(Avl1,Avl2,MaxDiff,ResSz,ResCmp) :- | |
55 | avl_height_compare_up_to(Avl1,Avl2,MaxDiff,0,ResSz,ResCmp). | |
56 | ||
57 | avl_height_compare_up_to(empty,empty,_,Sz,Sz,eq). | |
58 | avl_height_compare_up_to(empty,node(_,_,B,L,R),MaxDiff,Sz,Sz,Res) :- | |
59 | (avl_height_less_than(node(_,_,B,L,R),MaxDiff) -> Res=eq ; Res=lt). | |
60 | avl_height_compare_up_to(node(_,_,B,L,R),empty,MaxDiff,Sz,Sz,Res) :- | |
61 | (avl_height_less_than(node(_,_,B,L,R),MaxDiff) -> Res=eq ; Res=gt). | |
62 | avl_height_compare_up_to(node(_,_,B1,L1,R1),node(_,_,B2,L2,R2),MaxDiff,AccSz,ResSz,Res) :- | |
63 | ( B1 >= 0 -> A1=R1 ; A1=L1), | |
64 | ( B2 >= 0 -> A2=R2 ; A2=L2), | |
65 | Acc1 is AccSz+1, | |
66 | avl_height_compare_up_to(A1,A2,MaxDiff,Acc1,ResSz,Res). | |
67 | ||
68 | % ------------------------------- | |
69 | ||
70 | % compute an upper bound for the size of an AVL based on Height (log runtime): | |
71 | quick_avl_approximate_size(AVL,Size) :- avl_height(AVL,Height), Size is integer(2**Height-1). | |
72 | % a lower bound could be computed by =POWER(2,(HEIGHT+0.3277)/1.4405)-2 (page 460, Knuth 3) | |
73 | ||
74 | ||
75 | % ------------------------------- | |
76 | ||
77 | ||
78 | % a version of avl_fetch that looks for a pair in the AVL tree whose | |
79 | % first component is Key; it assumes that the term ordering gives the | |
80 | % first argument higher priority than the second one. | |
81 | % TO DO ?: extend to records: decompose((K,KY),K,KY). decompose(rec([H|T]),H,T). | |
82 | avl_fetch_pair(Key, node((K,KY),_,_,L,R),Res) :- | |
83 | ? | my_compare(O, Key, K), %((O='=',nonvar(Res)) -> print(comp(Res,KY)),nl ; true), % see TODO below |
84 | ? | avl_fetch_pair_1(O, Key, L, R, KY, Res). |
85 | ||
86 | % order of clauses relevant so that safe_avl_member returns elements in order ! | |
87 | avl_fetch_pair_1(<, Key, node((K,KY),_,_,L,R), _, _, Res) :- | |
88 | ? | my_compare(O, Key, K), %((O='=',nonvar(Res)) -> print(comp(Res,KY)),nl ; true), % see TODO below |
89 | ? | avl_fetch_pair_1(O, Key, L, R, KY, Res). |
90 | avl_fetch_pair_1(=, _Key, _L, _R, KY, KY). | |
91 | avl_fetch_pair_1(>, Key, _, node((K,KY),_,_,L,R),_,Res) :- | |
92 | ? | my_compare(O, Key, K), %((O='=',nonvar(Res)) -> print(comp(Res,KY)),nl ; true), % see TODO below |
93 | ? | avl_fetch_pair_1(O, Key, L, R, KY, Res). |
94 | ||
95 | my_compare(O,K1,K2) :- compare(OK,K1,K2), | |
96 | (OK=('=') -> true /* leave O free variable */ | |
97 | % TO DO: think about comparing KY and Res above | |
98 | ; O=OK). | |
99 | ||
100 | :- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_delete_pair((int(3),int(4)),A,true,AA), avl:avl_size(AA,2) )). | |
101 | :- assert_must_fail(( avl_tools:test_avl_set(A), avl_tools:avl_delete_pair((int(1),int(3)),A,true,_) )). | |
102 | :- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_delete_pair((int(1),int(2)),A,true,AA), | |
103 | avl_tools:avl_delete_pair((int(2),int(3)),AA,true,AAA), avl:avl_size(AAA,1) )). | |
104 | ||
105 | % an adaptation of avl_delete which deletes a pair just knowing the first argument of the pair | |
106 | % like avl_fetch_pair it assumes term ordering gives precedence to first argument | |
107 | ||
108 | avl_delete_pair(Key, AVL0, Val, AVL) :- | |
109 | avl_delete_pair5(AVL0, Key, Val, AVL, _). | |
110 | ||
111 | avl_delete_pair5(node(K,V,B,L,R), Key, Val, AVL, Delta) :- | |
112 | K = (KX,_KY), % crucial difference | |
113 | compare(C, Key, KX), | |
114 | avl_delete_pair(C, Key, Val, AVL, Delta, K, V, B, L, R). | |
115 | ||
116 | avl_delete_pair(<, Key, Val, AVL, Delta, K, V, B, L, R) :- | |
117 | avl_delete_pair5(L, Key, Val, L1, D1), | |
118 | B1 is B+D1, | |
119 | avl:avl(B1, K, V, L1, R, AVL), | |
120 | avl:avl_shrinkage(AVL, D1, Delta). | |
121 | avl_delete_pair(=, _, Val, AVL, Delta, _, Val, B, L, R) :- | |
122 | ( L == empty -> AVL = R, Delta = 1 | |
123 | ; R == empty -> AVL = L, Delta = 1 | |
124 | ; avl:avl_del_max(L, K, V, L1, D1), | |
125 | B1 is B+D1, | |
126 | avl:avl(B1, K, V, L1, R, AVL), | |
127 | avl:avl_shrinkage(AVL, D1, Delta) | |
128 | ). | |
129 | avl_delete_pair(>, Key, Val, AVL, Delta, K, V, B, L, R) :- | |
130 | avl_delete_pair5(R, Key, Val, R1, D1), | |
131 | B1 is B-D1, | |
132 | avl:avl(B1, K, V, L, R1, AVL), | |
133 | avl:avl_shrinkage(AVL, D1, Delta). | |
134 | ||
135 | ||
136 | % ------------------------------- | |
137 | ||
138 | ||
139 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
140 | % avl_apply | |
141 | % similar to avl_fetch_pair: but checks whether we have a function | |
142 | % and whether the function is defined for the key | |
143 | :- if(environ(no_wd_checking,true)). | |
144 | /* faster version without WD-checking : */ | |
145 | :- nl,print('DISABLING WD-CHECKING FOR FUNCTION APPLICATION!'),nl,nl. | |
146 | avl_apply(Key, node((K,KY),_,_,L,R),Res,_Span,_WF) :- | |
147 | compare(O, Key, K), | |
148 | avl_apply_1(O, Key, L, R, KY, Res). | |
149 | avl_apply_1(<, Key, node((K,KY),_,_,L,R), _, _, Res) :- | |
150 | compare(O, Key, K), | |
151 | avl_apply_1(O, Key, L, R, KY, Res). | |
152 | avl_apply_1(=, _Key, _Left,_Right, KY, KY). | |
153 | avl_apply_1(>, Key, _, node((K,KY),_,_,L,R),_,Res) :- | |
154 | compare(O, Key, K), | |
155 | avl_apply_1(O, Key, L, R, KY, Res). | |
156 | :- else. | |
157 | /* normal version with WD -checking : */ | |
158 | avl_apply(Key, node((K,KY),_,_,L,R),Res,Span,WF) :- | |
159 | compare(O, Key, K), | |
160 | avl_apply_1(O, Key, L, R, KY, Res,Span,WF). | |
161 | ||
162 | avl_apply_1(<, Key, NODE, _, _, Res,Span,WF) :- | |
163 | (NODE=node((K,KY),_,_,L,R) | |
164 | -> compare(O, Key, K), | |
165 | avl_apply_1(O, Key, L, R, KY, Res,Span,WF) | |
166 | ; add_wd_error_span('function applied outside of domain (#6): ','@fun'(Key,avl_set(NODE)),Span,WF) | |
167 | ). | |
168 | avl_apply_1(>, Key, _, NODE,_,Res,Span,WF) :- | |
169 | (NODE=node((K,KY),_,_,L,R) | |
170 | -> compare(O, Key, K), | |
171 | avl_apply_1(O, Key, L, R, KY, Res,Span,WF) | |
172 | ; add_wd_error_span('function applied outside of domain (#7): ','@fun'(Key,avl_set(NODE)),Span,WF) | |
173 | ). | |
174 | %%avl_apply_1(=, Key, _Left,_Right, KY, KY, _Span,_WF). | |
175 | avl_apply_1(=, Key, Left,Right, KY, Res,Span,WF) :- | |
176 | ((Left = node((Key,KY2),_,_,_,_) ; | |
177 | Right = node((Key,KY2),_,_,_,_)) % this is only a partial quick test; the next & previous elements could be deeper in the tree | |
178 | % TO DO: use optimized version of avl_fetch((Key,KY2),Left) ; avl_fetch((Key,KY2),Right) if preferences:preference(find_abort_values,true), | |
179 | -> add_wd_error_span('function application used for relation: ','@rel'(Key,KY,KY2),Span,WF) | |
180 | % we do not instantiate Res in this case | |
181 | ; Res=KY). | |
182 | ||
183 | :- endif. | |
184 | ||
185 | ||
186 | % ------------------------------- | |
187 | ||
188 | ||
189 | ||
190 | % similar to avl_apply but uses interval as lookup key | |
191 | avl_image_interval(From,To, node((K,KY),_,_,L,R),Res) :- | |
192 | ? | comp_interval(O, From,To, K), |
193 | ? | avl_image_interval_1(O, From,To, L, R, KY, Res). |
194 | avl_image_interval_1(<, From,To, NODE, _, _, Res) :- | |
195 | ? | NODE=node((K,KY),_,_,L,R),comp_interval(O, From,To, K), |
196 | ? | avl_image_interval_1(O, From,To, L, R, KY, Res). |
197 | avl_image_interval_1(=, _From,_To, _Left,_Right, KY, Res) :- Res=KY. | |
198 | avl_image_interval_1(>, From,To, _, NODE,_,Res) :- | |
199 | ? | NODE=node((K,KY),_,_,L,R), |
200 | ? | comp_interval(O, From,To, K), |
201 | ? | avl_image_interval_1(O, From,To, L, R, KY, Res). |
202 | ||
203 | comp_interval(O,From,To,int(Key)) :- | |
204 | ? | ( number(From),Key<From -> O = ('>') % could be minus_inf |
205 | ? | ; number(To), Key>To -> O = ('<') |
206 | ? | ; O = ('<') ; O = ('=') ; O = ('>') |
207 | ). | |
208 | % ------------------------------- |