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). |