1		% (c) 2009-2023 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_approximate_size_from_height/2,
9		avl_min_pair/3, avl_max_pair/3,
10		avl_fetch_pair/3,
11		avl_delete_pair/4,
12		avl_fetch_with_index/3, decompose_index/3,
13		avl_fetch_bin/4,
14		avl_apply/5,
15		avl_image_interval/4,
16		ord_domain_list_to_avl/2,
17		check_is_non_empty_avl/1]).
18
19		:- use_module(module_information,[module_info/2]).
20		:- module_info(group,kernel).
21		:- module_info(description,'This module provides AVL-tree utilities used by the kernel.').
22
23		:- use_module(library(avl)).
24
25		:- use_module(error_manager).
26		:- use_module(self_check).
27		:- use_module(kernel_waitflags,[add_wd_error_span/4]).
28
29		% -------------------------------
30
31		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))).
32
33		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_less_than(A,3) )).
34		:- assert_must_succeed(( avl_tools:avl_height_less_than(empty,1) )).
35		:- assert_must_fail(( avl_tools:test_avl_set(A), avl_tools:avl_height_less_than(A,2) )).
36		:- assert_must_fail(( avl_tools:avl_height_less_than(empty,0) )).
37
38		% a custom version of avl_height; advantage it will stop when reaching MaxHeight
39
40		avl_height_less_than(empty, MaxHeight) :- MaxHeight>0.
41		avl_height_less_than(node(_,_,B,L,R), H0) :- H0>1,
42		H1 is H0-1,
43		( B >= 0 -> avl_height_less_than(R, H1)
44		; avl_height_less_than(L, H1)
45		).
46
47
48		% efficient way of comparing AVL heights without having to fully traverse larger AVL
49
50		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_compare(A,A,eq) )).
51		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_compare(empty,A,lt) )).
52		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_compare(A,empty,gt) )).
53
54	?	avl_height_compare(A,B,Res) :- avl_height_compare_up_to(A,B,0,0,_,Res).
55
56		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_compare_up_to(empty,A,2,0,lt) )).
57		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_height_compare_up_to(empty,A,3,0,eq) )).
58
59		% avl_height_compare_up_to(Avl1,Avl2,MaxDiff,ResSz,ResCmp) -> ResSz: Height of smaller AVL, ResCmp = eq,lt,gt
60		avl_height_compare_up_to(Avl1,Avl2,MaxDiff,ResSz,ResCmp) :-
61		avl_height_compare_up_to(Avl1,Avl2,MaxDiff,0,ResSz,ResCmp).
62
63		avl_height_compare_up_to(empty,empty,_,Sz,Sz,eq).
64		avl_height_compare_up_to(empty,node(_,_,B,L,R),MaxDiff,Sz,Sz,Res) :-
65		(avl_height_less_than(node(_,_,B,L,R),MaxDiff) -> Res=eq ; Res=lt).
66		avl_height_compare_up_to(node(_,_,B,L,R),empty,MaxDiff,Sz,Sz,Res) :-
67		(avl_height_less_than(node(_,_,B,L,R),MaxDiff) -> Res=eq ; Res=gt).
68		avl_height_compare_up_to(node(_,_,B1,L1,R1),node(_,_,B2,L2,R2),MaxDiff,AccSz,ResSz,Res) :-
69		( B1 >= 0 -> A1=R1 ; A1=L1),
70		( B2 >= 0 -> A2=R2 ; A2=L2),
71		Acc1 is AccSz+1,
72	?	avl_height_compare_up_to(A1,A2,MaxDiff,Acc1,ResSz,Res).
73
74		% -------------------------------
75
76		% compute an upper bound for the size of an AVL based on Height (log runtime):
77		quick_avl_approximate_size(AVL,Size) :- avl_height(AVL,Height), Size is floor(2**Height)-1.
78		% a lower bound could be computed by =POWER(2,(HEIGHT+0.3277)/1.4405)-2 (page 460, Knuth 3)
79		avl_approximate_size_from_height(Height,Size) :- Size is floor(2**Height)-1.
80
81
82		% -------------------------------
83
84
85		avl_min_pair(AVLFun,FFrom,FTo) :-
86		(avl_min(AVLFun,(FFrom,FTo)) -> true
87		; add_error_fail(avl_min_pair,'Could not extract minimum pair of AVL set',AVLFun)).
88		avl_max_pair(AVLFun,FFrom,FTo) :-
89		(avl_max(AVLFun,(FFrom,FTo)) -> true
90		; add_error_fail(avl_max_pair,'Could not extract maximum pair of AVL set',AVLFun)).
91
92		% -------------------------------
93
94
95		% a version of avl_fetch that looks for a pair in the AVL tree whose
96		% first component is Key; it assumes that the term ordering gives the
97		% first argument higher priority than the second one.
98
99		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_pair((int(2),int(3)),A,R), R==int(6) )).
100		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_pair((int(1),int(2)),A,R), R==int(2) )).
101		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_pair((int(3),int(4)),A,R), R==int(12) )).
102		:- assert_must_fail(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_pair((int(1),int(4)),A,_) )).
103
104		avl_fetch_pair(Key, node((K,KY),_,_,L,R),Res) :-
105		my_compare(O, Key, K), %((O='=',nonvar(Res)) -> print(comp(Res,KY)),nl ; true), % see TODO below
106	?	avl_fetch_pair_1(O, Key, L, R, KY, Res).
107
108		% order of clauses relevant so that safe_avl_member returns elements in order !
109		avl_fetch_pair_1(<, Key, node((K,KY),_,_,L,R), _, _, Res) :-
110		my_compare(O, Key, K), %((O='=',nonvar(Res)) -> print(comp(Res,KY)),nl ; true), % see TODO below
111	?	avl_fetch_pair_1(O, Key, L, R, KY, Res).
112		avl_fetch_pair_1(=, _Key, _L, _R, KY, KY).
113		avl_fetch_pair_1(>, Key, _, node((K,KY),_,_,L,R),_,Res) :-
114		my_compare(O, Key, K), %((O='=',nonvar(Res)) -> print(comp(Res,KY)),nl ; true), % see TODO below
115	?	avl_fetch_pair_1(O, Key, L, R, KY, Res).
116
117		my_compare(O,K1,K2) :- compare(OK,K1,K2),
118		(OK=('=') -> true /* leave O free variable */
119		% TO DO: think about comparing KY and Res above
120		; O=OK).
121
122
123		% now a more generic version; which also works with records and later maybe freetypes, ...
124		% TODO: check if performance difference with avl_fetch_pair can be noticed
125
126		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_with_index((int(2),int(3)),A,R), R==int(6) )).
127		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_with_index((int(1),int(2)),A,R), R==int(2) )).
128		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_with_index((int(3),int(4)),A,R), R==int(12) )).
129		:- assert_must_fail(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_with_index((int(1),int(4)),A,_) )).
130
131		avl_fetch_with_index(Key, node(Value,_,_,L,R),Res) :- decompose_index(Value,K,KY),
132		my_compare(O, Key, K), %((O='=',nonvar(Res)) -> print(comp(Res,KY)),nl ; true), % see TODO below
133	?	avl_fetch_idx_1(O, Key, L, R, KY, Res).
134
135		% decompose a value into the index and the rest
136		decompose_index((K,KY),K,KY).
137		decompose_index(rec([field(F,FH)|T]),field(F,FH),rec(T)) :- T\==[]. % we could just use FH as key; assuming typechecker would catch if names mismatch
138		% TODO: freeval(ID,Case,Val1),
139		% avl_set(node(TopVal,_,_,L,R)) --> no use in decomposing: avl_set is fully known already
140
141		% order of clauses relevant so that safe_avl_member returns elements in order !
142		avl_fetch_idx_1(<, Key, node(Value,_,_,L,R), _, _, Res) :-
143		decompose_index(Value,K,KY),
144		my_compare(O, Key, K), %((O='=',nonvar(Res)) -> print(comp(Res,KY)),nl ; true), % see TODO below
145	?	avl_fetch_idx_1(O, Key, L, R, KY, Res).
146		avl_fetch_idx_1(=, _Key, _L, _R, KY, KY).
147		avl_fetch_idx_1(>, Key, _, node(Value,_,_,L,R),_,Res) :-
148		decompose_index(Value,K,KY),
149		my_compare(O, Key, K), %((O='=',nonvar(Res)) -> print(comp(Res,KY)),nl ; true), % see TODO below
150	?	avl_fetch_idx_1(O, Key, L, R, KY, Res).
151
152
153
154		% -------------------------------
155
156		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_bin((int(2),int(3)),',',A,R), R==int(6) )).
157		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_bin((int(1),int(2)),',',A,R), R==int(2) )).
158		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_bin((int(3),int(4)),',',A,R), R==int(12) )).
159		:- assert_must_fail(( avl_tools:test_avl_set(A), avl_tools:avl_fetch_bin((int(1),int(4)),',',A,_) )).
160
161		% fetch binary constructs with first argument known, e.g. member(Key,Res) or equal(Key,Res) or ...construct
162		avl_fetch_bin(Key, BinFunctor, AVL, Res) :- (AVL=empty ; AVL=node(_,_,_,_,_)),!,
163	?	avl_fetch_bin0(Key, BinFunctor, AVL, Res).
164		avl_fetch_bin(Key, BinFunctor, AVL, Res) :-
165		add_internal_error('Illegal AVL tree: ',avl_fetch_bin(Key, BinFunctor, AVL, Res)),fail.
166
167		avl_fetch_bin0(Key, BinFunctor, node(Expr,_,_,L,R),Res) :-
168		my_compare_bin(Expr,BinFunctor, O, Key, KY),
169	?	avl_fetch_bin_1(O, Key, BinFunctor, L, R, KY, Res).
170
171		% order of clauses relevant so that safe_avl_member returns elements in order !
172		avl_fetch_bin_1(<, Key, BinFunctor, node(Expr,_,_,L,R), _, _, Res) :-
173		my_compare_bin(Expr,BinFunctor, O, Key, KY),
174	?	avl_fetch_bin_1(O, Key,BinFunctor, L, R, KY, Res).
175		avl_fetch_bin_1(=, _Key, _, _L, _R, KY, KY).
176		avl_fetch_bin_1(>, Key, BinFunctor, _, node(Expr,_,_,L,R),_,Res) :-
177		my_compare_bin(Expr,BinFunctor, O, Key, KY),
178	?	avl_fetch_bin_1(O, Key,BinFunctor, L, R, KY, Res).
179
180		my_compare_bin(Expr,BinFunctor, O,Key,KY) :- functor(Expr,BinFunctor,2),!,
181		arg(1,Expr,K), arg(2,Expr,KY),
182		my_compare(O,Key,K).
183		my_compare_bin(Other,BinFunctor, O,_Key,'$none') :-
184		functor(Search,BinFunctor,2), % TODO: pass term with Key?
185		compare(O,Search,Other).
186
187
188
189		% -------------------------------
190
191
192		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_delete_pair((int(3),int(4)),A,true,AA), avl_size(AA,2) )).
193		:- assert_must_fail(( avl_tools:test_avl_set(A), avl_tools:avl_delete_pair((int(1),int(3)),A,true,_) )).
194		:- assert_must_succeed(( avl_tools:test_avl_set(A), avl_tools:avl_delete_pair((int(1),int(2)),A,true,AA),
195		avl_tools:avl_delete_pair((int(2),int(3)),AA,true,AAA), avl_size(AAA,1) )).
196
197		% an adaptation of avl_delete which deletes a pair just knowing the first argument of the pair
198		% like avl_fetch_pair it assumes term ordering gives precedence to first argument
199
200		avl_delete_pair(Key, AVL0, Val, AVL) :-
201		avl_delete_pair5(AVL0, Key, Val, AVL, _).
202
203		avl_delete_pair5(node(K,V,B,L,R), Key, Val, AVL, Delta) :-
204		K = (KX,_KY), % crucial difference
205		compare(C, Key, KX),
206		avl_delete_pair(C, Key, Val, AVL, Delta, K, V, B, L, R).
207
208		% If library(avl) has been replaced with avl_custom,
209		% also adjust the module prefixes here.
210		:- if(predicate_property(empty_avl(_), imported_from(avl_custom))).
211
212		avl_delete_pair(<, Key, Val, AVL, Delta, K, V, B, L, R) :-
213		avl_delete_pair5(L, Key, Val, L1, D1),
214		B1 is B+D1,
215		avl_custom:avl(B1, K, V, L1, R, AVL),
216		avl_custom:avl_shrinkage(AVL, D1, Delta).
217		avl_delete_pair(=, _, Val, AVL, Delta, _, Val, B, L, R) :-
218		( L == empty -> AVL = R, Delta = 1
219		; R == empty -> AVL = L, Delta = 1
220		; avl_custom:avl_del_max(L, K, V, L1, D1),
221		B1 is B+D1,
222		avl_custom:avl(B1, K, V, L1, R, AVL),
223		avl_custom:avl_shrinkage(AVL, D1, Delta)
224		).
225		avl_delete_pair(>, Key, Val, AVL, Delta, K, V, B, L, R) :-
226		avl_delete_pair5(R, Key, Val, R1, D1),
227		B1 is B-D1,
228		avl_custom:avl(B1, K, V, L, R1, AVL),
229		avl_custom:avl_shrinkage(AVL, D1, Delta).
230
231		:- else.
232
233		avl_delete_pair(<, Key, Val, AVL, Delta, K, V, B, L, R) :-
234		avl_delete_pair5(L, Key, Val, L1, D1),
235		B1 is B+D1,
236		avl:avl(B1, K, V, L1, R, AVL),
237		avl:avl_shrinkage(AVL, D1, Delta).
238		avl_delete_pair(=, _, Val, AVL, Delta, _, Val, B, L, R) :-
239		( L == empty -> AVL = R, Delta = 1
240		; R == empty -> AVL = L, Delta = 1
241		; avl:avl_del_max(L, K, V, L1, D1),
242		B1 is B+D1,
243		avl:avl(B1, K, V, L1, R, AVL),
244		avl:avl_shrinkage(AVL, D1, Delta)
245		).
246		avl_delete_pair(>, Key, Val, AVL, Delta, K, V, B, L, R) :-
247		avl_delete_pair5(R, Key, Val, R1, D1),
248		B1 is B-D1,
249		avl:avl(B1, K, V, L, R1, AVL),
250		avl:avl_shrinkage(AVL, D1, Delta).
251
252		:- endif.
253
254
255		% -------------------------------
256
257
258		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
259		% avl_apply
260		% similar to avl_fetch_pair: but checks whether we have a function
261		% and whether the function is defined for the key
262		:- if(environ(no_wd_checking,true)).
263		/* faster version without WD-checking : */
264		:- nl,print('DISABLING WD-CHECKING FOR FUNCTION APPLICATION!'),nl,nl.
265		avl_apply(Key, node((K,KY),_,_,L,R),Res,_Span,_WF) :-
266		compare(O, Key, K),
267		avl_apply_1(O, Key, L, R, KY, Res).
268		avl_apply_1(<, Key, node((K,KY),_,_,L,R), _, _, Res) :-
269		compare(O, Key, K),
270		avl_apply_1(O, Key, L, R, KY, Res).
271		avl_apply_1(=, _Key, _Left,_Right, KY, KY).
272		avl_apply_1(>, Key, _, node((K,KY),_,_,L,R),_,Res) :-
273		compare(O, Key, K),
274		avl_apply_1(O, Key, L, R, KY, Res).
275		:- else.
276		/* normal version with WD -checking : */
277		avl_apply(Key, node((K,KY),_,_,L,R),Res,Span,WF) :-
278		compare(O, Key, K),
279		avl_apply_1(O, Key, L, R, KY, Res,Span,WF).
280
281		avl_apply_1(<, Key, NODE, _, _, Res,Span,WF) :-
282		(NODE=node((K,KY),_,_,L,R)
283		-> compare(O, Key, K),
284		avl_apply_1(O, Key, L, R, KY, Res,Span,WF)
285		; add_wd_error_span('function applied outside of domain (#6): ','@fun'(Key,[]),Span,WF)
286		).
287		avl_apply_1(>, Key, _, NODE,_,Res,Span,WF) :-
288		(NODE=node((K,KY),_,_,L,R)
289		-> compare(O, Key, K),
290		avl_apply_1(O, Key, L, R, KY, Res,Span,WF)
291		; add_wd_error_span('function applied outside of domain (#7): ','@fun'(Key,[]),Span,WF)
292		).
293		%%avl_apply_1(=, Key, _Left,_Right, KY, KY, _Span,_WF).
294		avl_apply_1(=, Key, Left,Right, KY, Res,Span,WF) :-
295		((Left = node((Key,KY2),_,_,_,_) ;
296		Right = node((Key,KY2),_,_,_,_)) % this is only a partial quick test; the next & previous elements could be deeper in the tree
297		% TO DO: use optimized version of avl_fetch((Key,KY2),Left) ; avl_fetch((Key,KY2),Right) if preferences:preference(find_abort_values,true),
298		-> add_wd_error_span('function application used for relation: ','@rel'(Key,KY,KY2),Span,WF)
299		% we do not instantiate Res in this case
300		; Res=KY).
301
302		:- endif.
303
304		% -------------------------------
305
306
307		% similar to avl_apply but uses interval as lookup key
308		avl_image_interval(From,To, node((K,KY),_,_,L,R),Res) :-
309	?	comp_interval(O, From,To, K),
310	?	avl_image_interval_1(O, From,To, L, R, KY, Res).
311		avl_image_interval_1(<, From,To, NODE, _, _, Res) :-
312	?	NODE=node((K,KY),_,_,L,R),comp_interval(O, From,To, K),
313	?	avl_image_interval_1(O, From,To, L, R, KY, Res).
314		avl_image_interval_1(=, _From,_To, _Left,_Right, KY, Res) :- Res=KY.
315		avl_image_interval_1(>, From,To, _, NODE,_,Res) :-
316		NODE=node((K,KY),_,_,L,R),
317	?	comp_interval(O, From,To, K),
318	?	avl_image_interval_1(O, From,To, L, R, KY, Res).
319
320		comp_interval(O,From,To,int(Key)) :-
321		( number(From),Key<From -> O = ('>') % could be minus_inf
322		; number(To), Key>To -> O = ('<')
323		; O = ('<') ; O = ('=') ; O = ('>')
324		).
325		% -------------------------------
326
327		% like ord_list_to_avl but does not require list of Dom-Range pairs, adds true automatically
328		:- assert_must_succeed(( avl_tools:ord_domain_list_to_avl([1,2,3],A), avl_fetch(2,A))).
329
330		add_true_to_list([],[]).
331		add_true_to_list([H|T],[H-true|TT]) :- add_true_to_list(T,TT).
332
333		ord_domain_list_to_avl(List,Res) :-
334		add_true_to_list(List,LT),
335		ord_list_to_avl(LT,Res).
336
337		% -------------------------------
338
339		check_is_non_empty_avl(V) :- var(V),!, add_internal_error('Variable AVL tree:',check_is_non_empty_avl(V)).
340		check_is_non_empty_avl(empty) :- !, add_internal_error('Empty AVL tree:',check_is_non_empty_avl(empty)).
341		check_is_non_empty_avl(node(_,_,_,_,_)) :- !.
342		check_is_non_empty_avl(V) :- add_internal_error('Illegal AVL tree:',check_is_non_empty_avl(V)).
343
344