1 % (c) 2009-2024 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(kernel_z, [compaction/3,bag_items/3]).
6 % The module for Z specific kernel operations
7
8 :- use_module(library(avl)).
9
10 %:- use_module(debug).
11 :- use_module(self_check).
12 %:- use_module(tools).
13 %:- use_module(error_manager).
14 :- use_module(kernel_objects).
15 :- use_module(kernel_waitflags,[add_wd_error/3,assert_must_abort_wf/2]).
16 :- use_module(custom_explicit_sets,[expand_custom_set_to_list_wf/5, sorted_ground_normalised_list_to_avlset/3]).
17
18 :- use_module(module_information,[module_info/2]).
19 :- module_info(group,proz).
20 :- module_info(description,'This module provides operations that are special to the Z notation (sequence compaction, items of a bag).').
21
22
23 /* The compaction of a set integer -> X is the sequence where the "gaps are filled up".
24 E.g. compaction of {(1,a),(4,b),(8,c)} is {(1,a),(2,b),(3,c)}. */
25
26 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_z:compaction([(int(1),int(11)), (int(4),int(44))],[(int(1),int(11)), (int(2),int(44))],WF),WF)).
27 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_z:compaction([(int(33),int(333)), (int(4),int(2222)), (int(0),int(0))],[(int(1),int(0)), (int(2),int(2222)), (int(3),int(333))],WF),WF)).
28 :- assert_must_succeed(kernel_z:compaction([(int(1),int(11)), (int(4),int(44))],[(int(2),int(44)), (int(1),int(11))],_)).
29 :- assert_must_succeed((kernel_z:compaction(S,R,_),
30 S=[(int(5),int(55)),(int(1),int(11)), (int(4),int(44))], kernel_objects:equal_object(R,[(int(3),int(55)),(int(1),int(11)), (int(2),int(44))]))).
31 :- assert_must_abort_wf(kernel_z:compaction([(int(1),int(11)), (int(4),int(44)), (int(1),int(22))],_,WF),WF).
32
33 :- block compaction(-,?,?).
34 compaction(avl_set(A),Value,WF) :- !,
35 compaction_avl_set(A,Value,WF).
36 compaction(Sequence,Value,WF) :-
37 % TO DO: same cardinality of Sequence and Value
38 % TO DO: provide optimized version for avl_set?
39 expand_custom_set_to_list_wf(Sequence,ESeq,Done,compaction,WF),
40 compaction2(ESeq,Done,Value,WF).
41
42 % >>> f=%i.(i:2..90000|i+1) & r=SQUASH(SQUASH(SQUASH(f))) walltime reduced from 985 ms to 448 ms by using this version
43 compaction_avl_set(AVL,Sequence,WF) :- avl_domain(AVL,List),
44 List = [(int(FirstIdx),Val1)|RestList],
45 compaction_avl_list(RestList,FirstIdx,2,RestCompacted,WF),
46 % TODO: we could check if any change was made
47 CompactedList = [(int(1),Val1)|RestCompacted],
48 sorted_ground_normalised_list_to_avlset(CompactedList,SeqAVL,compaction_avl_set),
49 equal_object_wf(SeqAVL,Sequence,WF).
50
51 % compact an expanded AVL tree
52 compaction_avl_list([],_,_,[],_).
53 compaction_avl_list([(int(Idx),Val)|T],LastIdx,NextSeqIdx,Res,WF) :-
54 (Idx>LastIdx
55 -> Res = [(int(NextSeqIdx),Val)|TRes],
56 N1 is NextSeqIdx+1,
57 compaction_avl_list(T,Idx,N1,TRes,WF)
58 ;
59 add_wd_error('Input for squash is not a function for index:', b(integer(Idx),integer,[]),WF),
60 compaction_avl_list(T,Idx,NextSeqIdx,Res,WF)
61 ).
62
63 :- block compaction2(?,-,?,?).
64 compaction2(Relation,_,Sequence,WF) :-
65 empty_avl(Empty),
66 collect_sorted_values(Relation,Empty,SortedValues,WF),
67 create_sequence(SortedValues,Sequence1),
68 equal_object_optimized_wf(Sequence1,Sequence,compaction,WF).
69
70 :- block collect_sorted_values(-,?,?,?).
71 collect_sorted_values([],Avl,Avl,_WF).
72 collect_sorted_values([(int(Pos),Element)|Rest],In,Out,WF) :-
73 add_value(Pos,Element,Rest,In,Out,WF).
74
75 :- use_module(probsrc(preferences),[get_preference/2]).
76 :- block add_value(-,?,?,?,?,?).
77 add_value(Pos,Element,Rest,In,Out,WF) :-
78 ( avl_fetch(Pos,In,Old) ->
79 not_equal_object_wf(Old,Element,WF),
80 add_wd_error('Input for squash is not a function',
81 b(value([(int(Pos),Old),(int(Pos),Element)]),seq(any),[]),WF),
82 (get_preference(find_abort_values,false)
83 -> collect_sorted_values(Rest,In,Out,WF) % we have added error above; construct a solution nonetheless; will avoid enumeration warnings/ virtual timeouts but may hide a WD error due to failure
84 ; Out=failure
85 )
86 ;
87 avl_store(Pos,In,Element,Inter),
88 collect_sorted_values(Rest,Inter,Out,WF)).
89
90 :- block create_sequence(-,?).
91 create_sequence(failure,_Sequence) :- !.
92 create_sequence(SortedValues,Sequence) :-
93 create_sequence2(SortedValues,1,Sequence1),
94 equal_object(Sequence1,Sequence).
95 create_sequence2(SortedValues,Pos,Sequence) :-
96 ( avl_del_min(SortedValues, _Min, Element, Rest) ->
97 Sequence = [(int(Pos),Element)|RestSequence],
98 NextPos is Pos+1,
99 create_sequence2(Rest,NextPos,RestSequence)
100 ;
101 Sequence = []).
102
103 :- assert_must_succeed(exhaustive_kernel_check_wfdet(kernel_z:bag_items([(int(1),int(11)), (int(2),int(22)), (int(3),int(11))],[(int(11),int(2)), (int(22),int(1))],WF),WF)).
104 :- assert_must_abort_wf(bag_items([(int(1),int(11)), (int(2),int(22)), (int(4),int(11))],_,WF),WF).
105 :- assert_must_abort_wf(bag_items([(int(1),int(11)), (int(2),int(22)), (int(1),int(11))],_,WF),WF).
106
107 % This predicate computes the effect of the items function in Z.
108 % It is written for basic bag (multiset) support without performance in mind.
109 :- block bag_items(-,?,?).
110 bag_items(Sequence,Bag,WF) :-
111 expand_custom_set_to_list_wf(Sequence,ESequence,_Done,bag_items,WF),
112 empty_avl(Empty),
113 bag_items2(ESequence,[],Bag,Empty,WF).
114
115 :- block bag_items2(-,?,?,?,?), bag_items2(?,-,?,?,?), bag_items2(?,?,?,-,?).
116 bag_items2([],InBag,OutBag,Cnt,WF) :-
117 ( check_count(Cnt) ->
118 equal_object_wf(InBag,OutBag,WF)
119 ;
120 add_wd_error('Input for bag_times is not a sequence',[],WF)).
121 bag_items2([(int(Pos),Elem)|Rest],InBag,OutBag,InCnt,WF) :-
122 bag_items3(Pos,Elem,InBag,InterBag,InCnt,OutCnt,WF),
123 bag_items2(Rest,InterBag,OutBag,OutCnt,WF).
124 :- block bag_items3(-,?,?,?,?,?,?).
125 bag_items3(Pos,Elem,InBag,OutBag,InCnt,OutCnt,WF) :-
126 ( avl_fetch(Pos,InCnt) ->
127 add_wd_error('Input for bag_times is not a function',[],WF)
128 ;
129 avl_store(Pos,InCnt,true,OutCnt),
130 OldEntry = (Elem,int(OldCount)),
131 ( exact_element_of(OldEntry, InBag) ->
132 remove_element_wf( OldEntry, InBag, InterBag,WF),!,
133 NewCount is OldCount+1
134 ;
135 InterBag = InBag,
136 NewCount = 1),
137 add_element_wf( (Elem,int(NewCount)), InterBag, OutBag,WF)).
138
139 check_count(Cnt) :-
140 avl_domain(Cnt,Domain),
141 check_count2(Domain,1).
142 check_count2([],_).
143 check_count2([H|T],H) :- I is H+1,check_count2(T,I).