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(state_packing,[reset_stored_values/0, | |
6 | precompile_state_packing/0, % to be called after b_global_sets precompiled | |
7 | pack_state/2, unpack_state/2, | |
8 | unpack_state_top_level/2, | |
9 | incremental_pack_state/4, | |
10 | pack_values/2, unpack_values/2, | |
11 | pack_value/2, unpack_value/2, | |
12 | ||
13 | pack_bind_list/3, % pack a list of bind/2 terms and skeleton returning list of values | |
14 | unpack_bind_list/3, | |
15 | ||
16 | get_packed_b_state_with_uncompressed_lists/2, | |
17 | print_stored_values/1, set_next_value_id/1, | |
18 | retract_stored_values_with_statistics/0, | |
19 | print_state_packing_profile/0]). | |
20 | ||
21 | % a module to pack/compress states before asserting them in state_space | |
22 | :- use_module(specfile,[ csp_mode/0]). % b_or_z_mode/0, | |
23 | :- use_module(tools). | |
24 | :- use_module(b_global_sets). | |
25 | :- use_module(error_manager). | |
26 | :- use_module(debug,[debug_mode/1]). | |
27 | ||
28 | :- use_module(module_information). | |
29 | :- module_info(group,state_space). | |
30 | :- module_info(description,'This module packs and upacks states and values.'). | |
31 | ||
32 | :- dynamic bind_skeleton/2. % stores the list of variable names | |
33 | % we assume they are always in the same order; otherwise there is a problem | |
34 | % there is a separate skeleton for const_and_vars list of variables only and for full states with constants/variables (as generated by CBC checking) | |
35 | ||
36 | %pack_state(S,R) :- print('pack '), tools_printing:print_term_summary(S),nl,fail. | |
37 | pack_state(root,R) :- !, R=root. | |
38 | pack_state(const_and_vars(ID,S),R) :- % b_or_z_mode, % here for efficiency we assume that we are in B mode; any plug-in should not use this state constructor !! | |
39 | !, | |
40 | R='$cst_vars'(ID,PCS), | |
41 | % debug:time(state_packing:pack_bind_list(S,PS)). | |
42 | (bind_skeleton(const_and_vars,Skel) -> pack_bind_list(S,Skel,PS) | |
43 | ; pack_bind_list(S,Skel,PS), %print(vskel(Skel)),nl, | |
44 | (bind_skeleton(const_and_vars,OtherList) | |
45 | -> add_internal_error('Multiple bind skeletons for const_and_vars:',OtherList:Skel) ; true), | |
46 | assertz(bind_skeleton(const_and_vars,Skel))), | |
47 | compress_list(PS,PCS). | |
48 | pack_state(concrete_constants(S),R) :- preference(use_state_packing,full), | |
49 | !, | |
50 | % leads to further reduction in memory consumption, but to a slowdown | |
51 | R = '$cst'(PCS), | |
52 | (bind_skeleton(concrete_constants,Skel) -> pack_bind_list(S,Skel,PS) | |
53 | ; pack_bind_list(S,Skel,PS), %print(vskel(Skel)),nl, | |
54 | assertz(bind_skeleton(concrete_constants,Skel))), | |
55 | compress_list(PS,PCS). | |
56 | pack_state([bind(V,Val)|T],R) :- % b_or_z_mode, % again, for effiency we do not check whether we are in B mode here | |
57 | !, | |
58 | R='$bind_lst'(PV1,PCT), | |
59 | pack_value(Val,PV), | |
60 | (bind_skeleton(list,[V|Skel]) | |
61 | -> PV1=PV,pack_bind_list(T,Skel,PT1) | |
62 | ; pack_bind_list(T,Skel,PT), | |
63 | (bind_skeleton(list,OtherList) | |
64 | -> add_warning(pack_state,'Multiple bind skeletons:',OtherList:[V|Skel]), | |
65 | reorder(OtherList,[V|Skel],[PV|PT],[PV1|PT1]) %,print(reordered(PT1)),nl | |
66 | ; assertz(bind_skeleton(list,[V|Skel])), PT=PT1,PV=PV1 | |
67 | ) | |
68 | ), | |
69 | compress_list(PT1,PCT). | |
70 | pack_state([],R) :- !, R=[]. | |
71 | pack_state(csp_and_b(CSP,B),R) :- !, R=csp_and_b(PCSP,PB), | |
72 | pack_state(CSP,PCSP), | |
73 | pack_state(B,PB). | |
74 | pack_state(expanded_const_and_vars(C,V,_,_),R) :- !, | |
75 | pack_state(const_and_vars(C,V),R). | |
76 | pack_state(expanded_vars(V,_),R) :- !, | |
77 | pack_state(V,R). | |
78 | pack_state(CSP,R) :- | |
79 | \+ preference(use_state_packing,false),csp_mode,!, | |
80 | pack_csp_expression(CSP,PCSP), R=PCSP. | |
81 | pack_state(V,V). | |
82 | ||
83 | :- use_module(library(lists),[nth1/3]). | |
84 | reorder([],_,_,[]). | |
85 | reorder([ID|T1],Skel,Vals,[V2|T2]) :- nth1(Nr,Skel,ID), nth1(Nr,Vals,V2),!, | |
86 | reorder(T1,Skel,Vals,T2). | |
87 | reorder([ID|T1],Skel,Vals,Res) :- add_internal_error('Cannot find identifier:',ID), | |
88 | reorder(T1,Skel,Vals,Res). | |
89 | ||
90 | %compress_list([A,B,C,D|T],l4(A,B,C,D,CT)) :- !, compress_list(T,CT). | |
91 | %compress_list(List,'$bitvector'(Val,Len,CT)) :- compress_bv(List,Val,Len,T), !, compress_list(T,CT). | |
92 | compress_list([A,B,C|T],l3(A,B,C,CT)) :- !, compress_list(T,CT). | |
93 | %compress_list([A,B,C|T],l3c(ID,CT)) :- !, store_value((A,B,C),ID),compress_list(T,CT). % TO DO: use this when preferences:preference(use_state_packing,true) ? | |
94 | compress_list(T,T). | |
95 | ||
96 | %uncompress_list(l2(A,B,CT),[A,B|T]) :- uncompress_list(CT,T). | |
97 | uncompress_list(l3(A,B,C,CT),[A,B,C|T]) :- !, uncompress_list(CT,T). | |
98 | %uncompress_list('$bitvector'(Val,Len,CT),Res) :- !, uncompress_bv(Val,Len,T,Res), uncompress_list(CT,T). | |
99 | %uncompress_list(l3c(ID,CT),[A,B,C|T]) :- stored_value(ID,(A,B,C)),!,uncompress_list(CT,T). | |
100 | %uncompress_list(l4(A,B,C,D,CT),[A,B,C,D|T]) :- uncompress_list(CT,T). | |
101 | uncompress_list(T,T). | |
102 | ||
103 | ||
104 | %pack_bind_list(Store,ValueList) :- pack_bind_list(Store,_,ValueList). | |
105 | ||
106 | :- use_module(error_manager,[add_internal_error/2]). | |
107 | pack_bind_list([],[],R) :- !,R=[]. | |
108 | pack_bind_list([bind(V,Val)|T],[V|VT],R) :- !,R=[PV|PT], | |
109 | %atom_concat(pack_,V,PackV),runtime_profiler:profile_single_call(PackV,state_packing:pack_value(Val,PV)), | |
110 | pack_value(Val,PV), | |
111 | pack_bind_list(T,VT,PT). | |
112 | pack_bind_list(V,VT,R) :- | |
113 | add_internal_error('Illegal call, probably illegal order of variables: ',pack_bind_list(V,VT,R)), | |
114 | R=V. | |
115 | ||
116 | ||
117 | % just unpack top-level constructor for matching against | |
118 | % WARNING: do not use state for any processing apart from checking top-level constructor and constants id | |
119 | % it can be used for something like state_corresponds_to_initialised_b_machine, state_corresponds_to_set_up_constants | |
120 | unpack_state_top_level(root,State) :- !, State=root. | |
121 | unpack_state_top_level(concrete_constants(C),State) :- !, State=concrete_constants(C). | |
122 | unpack_state_top_level(const_and_vars(ID,CS),R) :- !, R=const_and_vars(ID,CS). | |
123 | unpack_state_top_level('$cst'(CS),R) :- !, R=concrete_constants(CS). | |
124 | unpack_state_top_level('$cst_vars'(ID,CS),R) :- !, R=const_and_vars(ID,CS). | |
125 | unpack_state_top_level('$bind_lst'(Val,_),R) :- !, R=[bind(unknown,Val)]. | |
126 | unpack_state_top_level(csp_and_b(CSP,B),csp_and_b(UPCSP,UPB)) :- !, unpack_state_top_level(CSP,UPCSP), | |
127 | unpack_state_top_level(B,UPB). | |
128 | unpack_state_top_level(X,X). | |
129 | ||
130 | ||
131 | :- use_module(library(avl)). | |
132 | unpack_state(root,State) :- !, State=root. | |
133 | unpack_state(concrete_constants(C),State) :- !, State=concrete_constants(C). % comment out in case concrete_constants are packed after all | |
134 | unpack_state(PackedState,State) :- %empty_avl(E), %tools_printing:print_term_summary(unpack(PackedState,State)),nl, | |
135 | %tools_printing:print_term_summary(unpack_state(PackedState)), | |
136 | unpack_state2(PackedState,State). | |
137 | ||
138 | %unpack_state(concrete_constants(S),R) --> {b_or_z_mode},!, {R=concrete_constants(UPS)}, unpack_state(S,UPS). % leads to further reduction | |
139 | unpack_state2(const_and_vars(ID,CS),R) :- !, | |
140 | R=const_and_vars(ID,UPS), | |
141 | unpack_state2(CS,UPS). | |
142 | unpack_state2('$cst'(CS),R) :- !, | |
143 | R=concrete_constants(UPS), | |
144 | uncompress_list(CS,S),get_bind_skeleton(concrete_constants,Skel), | |
145 | unpack_bind_list(S,Skel,UPS). | |
146 | unpack_state2('$cst_vars'(ID,CS),R) :- % {b_or_z_mode}, we assume const_and_vars is only used in B or Z mode or is compatible | |
147 | !, | |
148 | R=const_and_vars(ID,UPS), | |
149 | uncompress_list(CS,S),get_bind_skeleton(const_and_vars,Skel), | |
150 | unpack_bind_list(S,Skel,UPS). | |
151 | unpack_state2('$bind_lst'(Val,CT),R) :- % {b_or_z_mode}, we assume $bind_lst not used by any plug-in | |
152 | !, | |
153 | uncompress_list(CT,T),get_bind_skeleton(list,[Var|Skel]),R=[bind(Var,UPV)|RT], | |
154 | %atom_concat(unpack_,Var,PackV),runtime_profiler:profile_single_call(PackV,state_packing:unpack_value(Val,UPV)), | |
155 | unpack_value(Val,UPV), %!, | |
156 | unpack_bind_list(T,Skel,RT). | |
157 | unpack_state2([],R) :- !, R=[]. | |
158 | unpack_state2(csp_and_b(CSP,B),csp_and_b(UPCSP,UPB)) :- !, unpack_state2(CSP,UPCSP), | |
159 | unpack_state2(B,UPB). | |
160 | unpack_state2(PCSP,R) :- | |
161 | csp_mode, \+ preference(use_state_packing,false),!, | |
162 | unpack_csp_expression(PCSP,R). | |
163 | unpack_state2(R,R). | |
164 | ||
165 | unpack_bind_list([],[],[]). | |
166 | unpack_bind_list([Val|T],[Var|VT],R) :- R=[bind(Var,UPV)|UPT], | |
167 | %atom_concat(unpack_,Var,PackV),runtime_profiler:profile_single_call(PackV,state_packing:unpack_value(Val,UPV)), | |
168 | unpack_value(Val,UPV), %!, | |
169 | unpack_bind_list(T,VT,UPT). | |
170 | %unpack_bind_list('$bind_lst'(Var,Val,_),_) --> {add_internal_error('Unpacking value failed: ',Var/Val),fail}. | |
171 | ||
172 | ||
173 | get_bind_skeleton(Category,X) :- | |
174 | (bind_skeleton(Category,X) -> true | |
175 | ; add_internal_error('No bind skeleton stored for: ',get_bind_skeleton(Category,X)),fail). | |
176 | ||
177 | % a simpler version for list of bind-pairs; does not require bind_skeleton to be set up / stored | |
178 | pack_values([],[]) :- !. | |
179 | pack_values([bind(V,Val)|T],R) :- !,R=[Bind|PT], | |
180 | pack_bind(Val,V,Bind), | |
181 | pack_values(T,PT). | |
182 | pack_values(V,R) :- add_internal_error('Illegal value: ',pack_values(V,R)),R=V. | |
183 | ||
184 | pack_bind([],V,R) :- !, R='$bind_empty_set'(V). | |
185 | pack_bind(pred_false,V,R) :- !, R='$bind_false'(V). % bind boolean values | |
186 | pack_bind(pred_true,V,R) :- !, R='$bind_true'(V). | |
187 | pack_bind(Val,V,'$bind'(V,PV)) :- pack_value(Val,PV). | |
188 | ||
189 | unpack_bind('$bind_empty_set'(V),V,[]). | |
190 | unpack_bind('$bind_false'(V),V,pred_false). | |
191 | unpack_bind('$bind_true'(V),V,pred_true). | |
192 | unpack_bind('$bind'(V,PV),V,Val) :- unpack_value(PV,Val). | |
193 | ||
194 | unpack_values([],[]) :- !. | |
195 | unpack_values([PBind|T],R) :- unpack_bind(PBind,V,Val),!, | |
196 | R=[bind(V,Val)|UPT], | |
197 | unpack_values(T,UPT). | |
198 | unpack_values(V,R) :- | |
199 | add_internal_error('Illegal value: ',unpack_values(V,R)),R=V. | |
200 | ||
201 | ||
202 | :- use_module(library(avl)). | |
203 | :- use_module(preferences,[preference/2]). | |
204 | :- use_module(custom_explicit_sets,[is_interval_closure/5, construct_interval_closure/3]). | |
205 | ||
206 | pack_value(Var,R) :- var(Var),!, | |
207 | add_internal_error('Illegal variable value: ', pack_value(Var,R)), | |
208 | R='$variable'(Var). | |
209 | pack_value(avl_set(A),R) :- !, pack_avl_set(A,R). | |
210 | pack_value((A,B),(PA,PB)) :- !, pack_value(A,PA), pack_value(B,PB). | |
211 | pack_value(fd(Nr,T),R) :- pack_basic_fd_value(T,Nr,Atom),!,Atom=R. | |
212 | pack_value(int(Nr),R) :- !, R=Nr. | |
213 | pack_value(closure(P,T,Body),R) :- pack_closure(P,T,Body,PC),!, R=PC. | |
214 | pack_value(rec(Fields),PFields) :- !, pack_fields(Fields,PFields). | |
215 | pack_value(freeval(ID,Case,Val),freeval(ID,Case,PVal)) :- !, pack_value(Val,PVal). | |
216 | pack_value(term(floating(Nr)),R) :- !, R=Nr. | |
217 | %pack_value(V,_) :- V \= [], V \= pred_true, V \= pred_false, V \= string(_), functor(V,F,N), write(cannot_pack(F,N)),nl,fail. | |
218 | pack_value(V,V). | |
219 | ||
220 | /* not worth it : compute avl_domain and apply pack_value in one go: | |
221 | avl_packed_domain(empty, Domain, Domain). | |
222 | avl_packed_domain(node(Key,_,_,L,R), Domain0, Domain) :- | |
223 | pack_value(Key,PKey), avl_packed_domain(L, Domain0, [PKey|Domain1]), | |
224 | avl_packed_domain(R, Domain1, Domain). | |
225 | */ | |
226 | ||
227 | :- use_module(bsyntaxtree,[transform_bexpr/3]). | |
228 | ||
229 | pack_closure(P,T,Body,R) :- is_interval_closure(P,T,Body,Low,Up),!, | |
230 | %print(pack_interval(Low,Up,B)),nl, | |
231 | R='$interval'(Low,Up). | |
232 | %pack_value(closure(P,T,B),R) :- is_cartesian_product_closure(CPA,A1,A2),!, | |
233 | % R='$cartesian_product'(PA1,PA2), | |
234 | % pack_value(A1,PA1), pack_value(A2,PA2). | |
235 | pack_closure(P,T,Body,R) :- | |
236 | (preference(use_state_packing,full) -> true ; preference(force_state_packing_for_closures,true)), | |
237 | R = '$closure'(P,T,PBody), | |
238 | %add_message(state_packing,'Packing closure: ',Body,Body), | |
239 | transform_bexpr(state_packing:pack_bexpr,Body,PBody). | |
240 | ||
241 | pack_fields([],[]). | |
242 | pack_fields([field(F,H)|T],'$field'(F,PH,PT)) :- pack_value(H,PH), pack_fields(T,PT). | |
243 | ||
244 | l_pack_value([],[]). | |
245 | l_pack_value([H|T],[PH|PT]) :- pack_value(H,PH), l_pack_value(T,PT). | |
246 | ||
247 | pack_bexpr(b(value(Val),T,I),b(value(PVal),T,I)) :- | |
248 | pack_value(Val,PVal). | |
249 | ||
250 | % -------------------- | |
251 | ||
252 | ||
253 | pack_avl_set(Avl,R) :- preference(use_state_packing,Pref), pack_avl_set_aux(Avl,Pref,R). | |
254 | ||
255 | pack_avl_set_aux(A,full,R) :- | |
256 | avl_top_val2(A,(_,Bool)), (Bool=pred_false ; Bool=pred_true), % we have a relation/function to BOOL | |
257 | !, | |
258 | pack_relation(A,DomSkel,RangeVals), | |
259 | compress_bv(RangeVals,BVVal,BVLen,[]), !, % Store function/relation skeleton separately and compress bv | |
260 | %print(rel_packed(Val,Len,Rest)),nl, | |
261 | R='$stored_avl_rel_bv_packed'(ID1,BVVal), | |
262 | store_value((BVLen,DomSkel),ID1). | |
263 | pack_avl_set_aux(A,full,R) :- %R\==[], | |
264 | avl_domain(A,AD), | |
265 | (pack_fd_set(AD,Type,PackedInteger) | |
266 | -> !, | |
267 | R = '$avl_bv'(PackedInteger,Type) % avl bit vector | |
268 | ; AD = [_,_|_], % at least two elements | |
269 | !, | |
270 | l_pack_value(AD,ADL), | |
271 | R='$stored_avl_exp'(ID), | |
272 | store_value(ADL,ID) | |
273 | ). | |
274 | pack_avl_set_aux(A,_,R) :- A = node(fd(_,Type),_,_,_,_), | |
275 | % maybe we want to disable this for Pref=false ? TODO: benchmark (for nota.mch pack_fd_set seems slightly better) | |
276 | fd_type_can_be_packed_to_bv(Type), | |
277 | avl_domain(A,AD), | |
278 | pack_fd_set(AD,Type,PackedInteger),!, | |
279 | R = '$avl_bv'(PackedInteger,Type). | |
280 | pack_avl_set_aux(A,Pref,R) :- !, | |
281 | %avl_height(A,Height), format('Packing avl with height ~w (pref: ~w)~n',[Height,Pref]), | |
282 | pack_avl(A,PA), | |
283 | (try_store_avl(Pref,A,PA) | |
284 | -> R='$stored_avl_packed'(ID), store_value(PA,ID) | |
285 | ; PA = packed_leaf(AP) -> R='$avl_singleton'(AP) | |
286 | ; R='$avl_packed'(PA) | |
287 | ). | |
288 | ||
289 | :- use_module(probsrc(avl_tools),[avl_height_less_than/2]). | |
290 | try_store_avl(true,_A,PA) :- | |
291 | %\+ avl_height_less_than(A,5), % if the set is large enough, store it separately; TODO: provide preference? | |
292 | store_packed_avl(PA). | |
293 | ||
294 | store_packed_avl(packed_leaf(Val)) :- | |
295 | compound(Val). % no use storing simple singleton sets; maybe singleton sets in general? | |
296 | store_packed_avl(packed_node(_,_,_,_)). | |
297 | ||
298 | %avl_top_val(node(Val,_,_,_,_),Val). | |
299 | avl_top_val2(node(Val,_,_,L,R),Val) :- L \= empty, R\=empty. | |
300 | ||
301 | unpack_avl_expanded(AD,R) :- | |
302 | l_unpack_value(AD,ADT), | |
303 | custom_explicit_sets:ord_list_to_avlset_direct(ADT,R,unpack_value). | |
304 | ||
305 | % try to pack an AVL tree in-place without expanding to list first: | |
306 | pack_avl(empty, empty). | |
307 | pack_avl(node(Val,_,0,empty,empty), R) :- !, | |
308 | R= packed_leaf(PackedVal), | |
309 | pack_value(Val,PackedVal). | |
310 | pack_avl(node(Val,true,B,L0,R0), packed_node(PackedVal,B,L1,R1)) :- | |
311 | pack_value(Val,PackedVal), | |
312 | pack_avl(L0, L1), % TODO: we could store L, R separately | |
313 | pack_avl(R0, R1). | |
314 | ||
315 | unpack_avl(empty,empty). | |
316 | unpack_avl(packed_leaf(PackedVal), node(Val,true,0,empty,empty)) :- unpack_value(PackedVal,Val). | |
317 | unpack_avl(packed_node(PackedVal,B,L0,R0), node(Val,true,B,L1,R1)) :- | |
318 | unpack_value(PackedVal,Val), | |
319 | unpack_avl(L0, L1), | |
320 | unpack_avl(R0, R1). | |
321 | ||
322 | % pack relation: skeleton of relation and range values separately | |
323 | pack_relation(AVL,DomSkeleton,RangeValueList) :- pack_relation(AVL,DomSkeleton,RangeValueList,[]). | |
324 | pack_relation(empty, empty) --> []. | |
325 | pack_relation(node((DomVal,RanVal),true,B,L0,R0), packed_rel_node(PackedVal,B,L1,R1)) --> | |
326 | {pack_value(DomVal,PackedVal), | |
327 | RanVal=RanPackedVal %pack_value(RanVal,RanPackedVal) | |
328 | }, % enable compress_bv | |
329 | [RanPackedVal], | |
330 | pack_relation(L0, L1), | |
331 | pack_relation(R0, R1). | |
332 | ||
333 | unpack_relation(DomSkeleton,RangeValueList,AVL) :- unpack_relation(DomSkeleton,AVL,RangeValueList,[]). | |
334 | unpack_relation(empty, empty) --> []. | |
335 | unpack_relation(packed_rel_node(PackedVal,B,L1,R1), node((DomVal,RanVal),true,B,L0,R0)) --> | |
336 | {unpack_value(PackedVal,DomVal)}, | |
337 | [RanPackedVal], | |
338 | {RanPackedVal=RanVal}, %{unpack_value(RanPackedVal,RanVal)}, | |
339 | unpack_relation(L1, L0), | |
340 | unpack_relation(R1, R0). | |
341 | ||
342 | % avl_height but for packed AVLs | |
343 | packed_avl_height(AVL, Height) :- | |
344 | packed_avl_height(AVL, 0, Height). | |
345 | ||
346 | packed_avl_height(empty, H, H). | |
347 | packed_avl_height(packed_leaf(_), H0, H1) :- H1 is H0+1. | |
348 | packed_avl_height(packed_node(_,B,L,R), H0, H) :- | |
349 | H1 is H0+1, | |
350 | ( B >= 0 -> packed_avl_height(R, H1, H) | |
351 | ; packed_avl_height(L, H1, H) | |
352 | ). | |
353 | packed_avl_height(packed_rel_node(_,_,B,L,R), H0, H) :- | |
354 | H1 is H0+1, | |
355 | ( B >= 0 -> packed_avl_height(R, H1, H) | |
356 | ; packed_avl_height(L, H1, H) | |
357 | ). | |
358 | ||
359 | % -------------------- | |
360 | ||
361 | % TO DO or [(fd,fd) as bit-vectors if <xx bits | |
362 | ||
363 | % Pack set of FD values as bit-vector representation | |
364 | pack_fd_set([fd(X,Type)|T],Type,Result) :- | |
365 | fd_type_can_be_packed_to_bv(Type), | |
366 | Acc is 1<<X, | |
367 | pack_fd_set_aux(T,Acc,Result). | |
368 | ||
369 | :- use_module(tools_platform, [max_tagged_pow2/1]). | |
370 | fd_type_can_be_packed_to_bv(Type) :- | |
371 | b_get_fd_type_bounds(Type,1,UpBound), integer(UpBound), | |
372 | max_tagged_pow2(MaxBound), | |
373 | UpBound < MaxBound. | |
374 | ||
375 | pack_fd_set_aux([],A,A). | |
376 | pack_fd_set_aux([fd(X,_)|T],Acc,Res) :- | |
377 | NewAcc is Acc \/ (1<<X), | |
378 | pack_fd_set_aux(T,NewAcc,Res). | |
379 | ||
380 | % unpack a bit-vector set representation | |
381 | unpack_fd_set(PackedInteger,Type,Value) :- | |
382 | unpack_fd_set_aux(PackedInteger,0,Type,ResList), %print(unpacked(PackedInteger,ResList)),nl, | |
383 | custom_explicit_sets:ord_list_to_avlset_direct(ResList,Value,unpack_fd_set). | |
384 | ||
385 | unpack_fd_set_aux(0,_,_,Res) :- !, Res=[]. | |
386 | unpack_fd_set_aux(Nr,X,Type,Res) :- | |
387 | (Nr mod 2 =:= 1 -> Res = [fd(X,Type)-true|T] ; Res=T), | |
388 | X1 is X+1, Nr1 is (Nr>>1), | |
389 | unpack_fd_set_aux(Nr1,X1,Type,T). | |
390 | ||
391 | % first rough attempt at packing CSP expressions | |
392 | pack_csp_expression(esharing(Set,B,C,Span),'$esharing'(PSet,PB,PC,PSpan)) :- !, | |
393 | pack_csp_expression(Set,PSet), pack_csp_expression(B,PB), | |
394 | pack_csp_expression(C,PC), pack_csp_expression(Span,PSpan). | |
395 | pack_csp_expression('|||'(A,B,Span),'|||'(PA,PB,PSpan)) :- !, | |
396 | pack_csp_expression(A,PA), pack_csp_expression(B,PB), pack_csp_expression(Span,PSpan). | |
397 | %pack_csp_expression('&'(A,B),'&'(PA,PB)) :- !, | |
398 | % pack_csp_expression(A,PA), pack_csp_expression(B,PB). | |
399 | pack_csp_expression('[]'(A,B,Span),'[]'(PA,PB,PSpan)) :- !, | |
400 | pack_csp_expression(A,PA), pack_csp_expression(B,PB), pack_csp_expression(Span,PSpan). | |
401 | pack_csp_expression(eaParallel(C,A,D,B,Span),eaParallel(PC,PA,PD,PB,PSpan)) :- !, | |
402 | pack_csp_expression(A,PA), pack_csp_expression(B,PB), pack_csp_expression(C,PC), | |
403 | pack_csp_expression(D,PD), pack_csp_expression(Span,PSpan). | |
404 | %pack_csp_expression(prefix(C,A,D,B,Span),prefix(PC,PA,PD,PB,PSpan)) :- !, | |
405 | % pack_csp_expression(A,PA), pack_csp_expression(B,PB), pack_csp_expression(C,PC), | |
406 | % pack_csp_expression(D,PD), pack_csp_expression(Span,PSpan). | |
407 | %pack_csp_expression(ifte(C,A,D,B,Span,S3),ifte(PC,PA,PD,PB,PSpan,S3)) :- !, | |
408 | % pack_csp_expression(A,PA), pack_csp_expression(B,PB), pack_csp_expression(C,PC), | |
409 | % pack_csp_expression(D,PD), pack_csp_expression(Span,PSpan). | |
410 | %pack_csp_expression(V,'$stored_csp'(ID)) :- store_value(V,ID). | |
411 | pack_csp_expression(V,ID) :- store_value(V,ID). | |
412 | ||
413 | unpack_csp_expression('$esharing'(PSet,PB,PC,PSpan),esharing(Set,B,C,Span)) :- !, | |
414 | unpack_csp_expression(PSet,Set), unpack_csp_expression(PB,B), | |
415 | unpack_csp_expression(PC,C), unpack_csp_expression(PSpan,Span). | |
416 | unpack_csp_expression('|||'(A,B,Span),'|||'(PA,PB,PSpan)) :- !, | |
417 | unpack_csp_expression(A,PA), unpack_csp_expression(B,PB), unpack_csp_expression(Span,PSpan). | |
418 | %unpack_csp_expression('&'(A,B),'&'(PA,PB)) :- !, | |
419 | % unpack_csp_expression(A,PA), unpack_csp_expression(B,PB). | |
420 | unpack_csp_expression('[]'(A,B,Span),'[]'(PA,PB,PSpan)) :- !, | |
421 | unpack_csp_expression(A,PA), unpack_csp_expression(B,PB), unpack_csp_expression(Span,PSpan). | |
422 | unpack_csp_expression(eaParallel(C,A,D,B,Span),eaParallel(PC,PA,PD,PB,PSpan)) :- !, | |
423 | unpack_csp_expression(A,PA), unpack_csp_expression(B,PB), unpack_csp_expression(C,PC), | |
424 | unpack_csp_expression(D,PD), unpack_csp_expression(Span,PSpan). | |
425 | %unpack_csp_expression(prefix(C,A,D,B,Span),prefix(PC,PA,PD,PB,PSpan)) :- !, | |
426 | % unpack_csp_expression(A,PA), unpack_csp_expression(B,PB), unpack_csp_expression(C,PC), | |
427 | % unpack_csp_expression(D,PD), unpack_csp_expression(Span,PSpan). | |
428 | %unpack_csp_expression(ifte(C,A,D,B,Span,S3),ifte(PC,PA,PD,PB,PSpan,S3)) :- !, | |
429 | % unpack_csp_expression(A,PA), unpack_csp_expression(B,PB), unpack_csp_expression(C,PC), | |
430 | % unpack_csp_expression(D,PD), unpack_csp_expression(Span,PSpan). | |
431 | %unpack_csp_expression('$stored_csp'(ID),V) :- !, stored_value(ID,V). | |
432 | unpack_csp_expression(ID,V) :- !, stored_value(ID,V). | |
433 | unpack_csp_expression(V,V). | |
434 | ||
435 | %unpack_value(Val,UPVal) :- unpack_value(Val,UPVal,empty,_). | |
436 | ||
437 | unpack_value(V,R) :- var(V),!, | |
438 | add_internal_error('Illegal variable value: ', unpack_value(V,R)), R=V. | |
439 | unpack_value('$avl_packed'(AP),R) :- !, R=avl_set(A),unpack_avl(AP,A). | |
440 | unpack_value('$avl_singleton'(AP),R) :- !, R=avl_set(node(A,true,0,empty,empty)),unpack_value(AP,A). | |
441 | unpack_value('$avl_exp'(AD),R) :- !, unpack_avl_expanded(AD,R). | |
442 | unpack_value('$stored_avl_packed'(ID),R) :- !, | |
443 | (stored_value(ID,Val) -> R = avl_set(A), unpack_avl(Val,A) | |
444 | ; add_internal_error('No stored AVL: ',ID),fail). | |
445 | unpack_value('$stored_avl_exp'(ID),R) :- !, | |
446 | (stored_value(ID,Val) -> unpack_avl_expanded(Val,R) | |
447 | ; add_internal_error('No stored AVL: ',ID),fail). | |
448 | unpack_value('$stored_avl_rel_bv_packed'(ID1,Val),R) :- !, | |
449 | (stored_value(ID1,(Len,DomVal)) | |
450 | -> R = avl_set(A), | |
451 | uncompress_bv(Val,Len,[],RanVals), | |
452 | unpack_relation(DomVal,RanVals,A) | |
453 | ; add_internal_error('No stored length and Domain AVL / Range Value: ',ID1),fail). | |
454 | unpack_value('$avl_bv'(PackedInteger,Type),R) :- !, unpack_fd_set(PackedInteger,Type,R). | |
455 | /* comment in and re-add DCG to try and re-construct sharing; does seem to increase memory usage for vital_gradient_values | |
456 | unpack_value('$stored_avl'(ID),R,InEnv,OutEnv) :- !, | |
457 | (avl_fetch(ID,InEnv,ER) %(expanded(ID,ER),InEnv) | |
458 | -> R = ER, OutEnv=InEnv % reuse the already expanded value: will also decrease memory consumption due to sharing | |
459 | ; stored_value(ID,Val), | |
460 | avl_store(ID,InEnv,R,InEnv2), % OutEnv=[expanded(ID,R)|OutEnv2], % note: ID cannot occur inside Val | |
461 | unpack_avl_expanded(Val,R,InEnv2,OutEnv)). | |
462 | */ | |
463 | %unpack_value('$cartesian_product'(A,B),R) :- unpack_value(A,PA), unpack_value(B,PB), | |
464 | % construct_cartesian_product_closure(PA,PB,R). | |
465 | unpack_value((A,B),(PA,PB)) :- !, unpack_value(A,PA), unpack_value(B,PB). | |
466 | unpack_value('$interval'(A,B),R) :- !, construct_interval_closure(A,B,R). | |
467 | unpack_value('$closure'(P,T,PB),closure(P,T,B)) :- !, transform_bexpr(state_packing:unpack_bexpr,PB,B). | |
468 | unpack_value('$field'(Field,PH,PT),rec(F)) :- !, | |
469 | unpack_fields('$field'(Field,PH,PT),F). | |
470 | unpack_value(freeval(ID,Case,PVal),freeval(ID,Case,Val)) :- !, unpack_value(PVal,Val). | |
471 | unpack_value(Nr,R) :- integer(Nr),!, R=int(Nr). | |
472 | unpack_value(Nr,R) :- float(Nr),!, R=term(floating(Nr)). | |
473 | unpack_value(V,UPV) :- unpack_basic_fd_value(V,FD),!,UPV=FD. | |
474 | unpack_value(V,V). | |
475 | ||
476 | unpack_fields([],[]). | |
477 | unpack_fields('$field'(F,PH,PT),[field(F,H)|T]) :- unpack_value(PH,H), unpack_fields(PT,T). | |
478 | ||
479 | l_unpack_value([],[]). | |
480 | l_unpack_value([H|T],[PH-true|PT]) :- unpack_value(H,PH), l_unpack_value(T,PT). | |
481 | ||
482 | unpack_bexpr(b(value(PVal),T,I),b(value(Val),T,I)) :- | |
483 | unpack_value(PVal,Val). | |
484 | ||
485 | % ------------------------- | |
486 | ||
487 | % a version of pack_state which makes use of a previously packed state and a ordered list of Unchanged variables | |
488 | % incremental_pack_state(State,PrevPackedState,UnchangedVariables,PackedState) | |
489 | % The idea is to re-use the packed values from the previous state if possible | |
490 | ||
491 | % the packed state needs to be processed by get_packed_b_state_with_uncompressed_lists first | |
492 | ||
493 | % Note: bind_skeleton does not need to be stored as these clauses only apply when previous state of same type exists | |
494 | incremental_pack_state(const_and_vars(ID,T),const_and_vars(ID,PrevCT),Unchanged,'$cst_vars'(ID,PCT)) :- !, | |
495 | uncompress_list(PrevCT,PrevT), | |
496 | incr_pack_bind_list(T,PrevT,Unchanged,PT), | |
497 | compress_list(PT,PCT). | |
498 | incremental_pack_state([bind(V,Val)|T],[bind(V,PrevV)|PrevCT],Unchanged,'$bind_lst'(PV,PCT)) :- !, | |
499 | uncompress_list(PrevCT,PrevT), | |
500 | incremental_pack_value(Val,V,PrevV,Unchanged,PV,U2), | |
501 | incr_pack_bind_list(T,PrevT,U2,PT), | |
502 | compress_list(PT,PCT). | |
503 | incremental_pack_state(State,Prev,UC,PackedState) :- | |
504 | tools_printing:print_term_summary(non_incremental_pack_state(State,Prev,UC,PackedState)),nl, | |
505 | pack_state(State,PackedState). | |
506 | ||
507 | %ord_delete_existing_element(List,El,ResList) :- % ord_del_element also succeeds if El is not in the list ! | |
508 | % ord_intersection([El],List,[El],ResList). | |
509 | %:- use_module(library(ordsets),[ord_intersection/4]). | |
510 | ||
511 | incremental_pack_value(_,Var,PrevPackVal,[Var|U2],PackedValue,U2) :- % copy previously packed value | |
512 | !, PackedValue=PrevPackVal. | |
513 | incremental_pack_value(Val,_Var,_Prev,Unchanged,PackedValue,Unchanged) :- | |
514 | pack_value(Val,PackedValue). | |
515 | ||
516 | %not_packed(pred_false). | |
517 | %not_packed(pred_true). | |
518 | %not_packed(string(_)). | |
519 | ||
520 | incr_pack_bind_list([],_,Unchanged,[]) :- | |
521 | (Unchanged=[] -> true ; add_internal_error('Did not encounter these unchanged vars:',Unchanged)). | |
522 | incr_pack_bind_list([bind(V,Val)|T],[bind(V,PrevV)|PrevT],Unchanged,[PackedValue|PT]) :- | |
523 | incremental_pack_value(Val,V,PrevV,Unchanged,PackedValue,U2), | |
524 | incr_pack_bind_list(T,PrevT,U2,PT). | |
525 | ||
526 | % ------------------------- | |
527 | ||
528 | :- use_module(library(terms),[term_hash/2]). | |
529 | :- use_module(debug,[debug_format/3]). | |
530 | :- dynamic pack_basic_fd_value4/4, unpack_basic_fd_value/2. | |
531 | % associate precompiled atoms with all enumerated & deferred set elements; TO DO: only do for "smaller" SETS | |
532 | precompile_state_packing :- | |
533 | retractall(pack_basic_fd_value4(_,_,_,_)), | |
534 | retractall(unpack_basic_fd_value(_,_)), | |
535 | ? | b_global_set(T), |
536 | b_fd_card(T,Card), | |
537 | (integer(Card), Card < 1000 -> true | |
538 | ; debug_format(19,'Not precompiling state packing for ~w (size ~w)~n',[T,Card]),fail), | |
539 | ? | enum_global_type_limited(fd(Nr,T),_), % limits infinite deferred sets, which we don't precompile anyway |
540 | gen_fd_atom(Nr,T,NewAtom), | |
541 | %debug:debug_println(9,pack(T,Nr,NewAtom)), | |
542 | term_hash((T,Nr),Hash), % we could number the Types and use something like TypeNr*MaxSize + Nr | |
543 | assertz(pack_basic_fd_value4(Hash,T,Nr,NewAtom)), | |
544 | assertz(unpack_basic_fd_value(NewAtom,fd(Nr,T))),fail. | |
545 | precompile_state_packing. | |
546 | ||
547 | gen_fd_atom(Nr,T,NewAtom) :- | |
548 | atom_codes(T,TC), | |
549 | number_codes(Nr,NrC), | |
550 | append(TC,NrC,TNrC), | |
551 | atom_codes(NewAtom,[36,102,100,95|TNrC]). % generates '$fd_TNr atom | |
552 | ||
553 | % use term_hash in case we have very large enumerated/deferred sets | |
554 | pack_basic_fd_value(T,Nr,NewAtom) :- term_hash((T,Nr),Hash), | |
555 | pack_basic_fd_value4(Hash,T,Nr,NewAtom). | |
556 | ||
557 | % ------------------------ | |
558 | ||
559 | :- dynamic stored_value/2, stored_value_hash_to_id/2. | |
560 | ||
561 | reset_stored_values :- | |
562 | %(retract(stored_value(ID,_)), print(remove_stored_value(ID)),nl,fail ; true), | |
563 | retractall(bind_skeleton(_,_)), | |
564 | retractall(stored_value(_,_)), | |
565 | retractall(stored_value_hash_to_id(_,_)), | |
566 | bb_put(next_value_id,0). | |
567 | ||
568 | :- if(current_prolog_flag(dialect, sicstus)). | |
569 | :- use_module(library(terms),[term_hash/3]). | |
570 | store_value(Value,ID) :- | |
571 | term_hash(Value,[range(smallint),algorithm(sdbm), depth(infinite),if_var(ignore)],Hash), | |
572 | % instead of infinite we could use a lower bound, collisions are taken care of below | |
573 | store_value_aux(Value,Hash,ID). | |
574 | :- else. | |
575 | :- use_module(hashing,[my_term_hash/2]). | |
576 | store_value(Value,ID) :- | |
577 | my_term_hash(Value,Hash), | |
578 | store_value_aux(Value,Hash,ID). | |
579 | :- endif. | |
580 | ||
581 | store_value_aux(Value,Hash,ID) :- | |
582 | stored_value_hash_to_id(Hash,ID), | |
583 | stored_value(ID,Stored_Value), | |
584 | Value=Stored_Value, % check that we have the exact value, could be expensive but collisions are possible | |
585 | !. % we have already stored the value | |
586 | store_value_aux(Value,Hash,ID) :- | |
587 | (bb_get(next_value_id,NID) -> true ; NID=0), | |
588 | NID1 is NID+1, | |
589 | bb_put(next_value_id,NID1), | |
590 | assertz(stored_value(NID,Value)), | |
591 | assertz(stored_value_hash_to_id(Hash,NID)), | |
592 | ID=NID. | |
593 | ||
594 | :- use_module(tools_printing, [print_dynamic_pred/4]). | |
595 | % state_packing:print_stored_values(user_output) | |
596 | print_stored_values(Stream) :- % for saving state_space to file | |
597 | print_dynamic_pred(Stream,state_packing,bind_skeleton,2), | |
598 | print_dynamic_pred(Stream,state_packing,stored_value,2), | |
599 | print_dynamic_pred(Stream,state_packing,stored_value_hash_to_id,2), | |
600 | (bb_get(next_value_id,NID) -> true ; NID=0), format(Stream,'~n:- dynamic next_value_id/1.~nnext_value_id(~w).~n~n',[NID]). | |
601 | ||
602 | % when loading state space from file | |
603 | set_next_value_id(ID) :- bb_put(next_value_id,ID). | |
604 | ||
605 | retract_stored_values_with_statistics :- | |
606 | ? | retract_with_statistics(state_packing,[stored_value(_,_), |
607 | stored_value_hash_to_id(_,_)]), | |
608 | reset_stored_values. | |
609 | ||
610 | % portray state packing infos | |
611 | print_state_packing_profile :- | |
612 | (bb_get(next_value_id,Nr) -> true ; Nr=0), | |
613 | format('Stored ~w AVL sets for state compression~n',[Nr]), | |
614 | (debug_mode(on) -> portray_stored_values ; true). | |
615 | ||
616 | portray_stored_values :- bind_skeleton(Kind,Skel), | |
617 | format('Binding skeleton for ~w:~n ~w~n',[Kind,Skel]), | |
618 | fail. | |
619 | portray_stored_values :- | |
620 | stored_value(NID,Value), functor(Value,F,N), | |
621 | (packed_avl_height(Value,Size) -> true ; length(Value,Size) -> true ; Size='?'), | |
622 | format('Value ~w : ~w/~w : size: ~w~n',[NID,F,N,Size]), | |
623 | fail. | |
624 | portray_stored_values. | |
625 | ||
626 | % ------------------------------------- | |
627 | ||
628 | % utility to translate boolean variables into bit-vector integers (not used yet; degrades performance) | |
629 | ||
630 | :- use_module(self_check). | |
631 | :- assert_must_succeed((Input=[pred_false,pred_true,pred_false,1],state_packing:compress_bv(Input,Val,Len,Rest), state_packing:uncompress_bv(Val,Len,Rest,Res), Res=Input)). | |
632 | :- assert_must_succeed((Input=[pred_false,pred_false],state_packing:compress_bv(Input,Val,Len,Rest), state_packing:uncompress_bv(Val,Len,Rest,Res), Res=Input)). | |
633 | :- assert_must_succeed((Input=[pred_true,pred_true],state_packing:compress_bv(Input,Val,Len,Rest), state_packing:uncompress_bv(Val,Len,Rest,Res), Res=Input)). | |
634 | ||
635 | % compress successive boolean values (at least 2) | |
636 | compress_bv([P|T],Val,Len,Rest) :- get_bool_bv(P,Acc), compress_bv2(T,Acc,Val,Len,Rest). | |
637 | get_bool_bv(pred_true,1). | |
638 | get_bool_bv(pred_false,0). | |
639 | compress_bv2([P|T],Acc,Val,Len,Rest) :- get_bool_bv(P,BoolVal),!, | |
640 | Acc2 is Acc + BoolVal*2, % BoolVal+(Acc << 1), | |
641 | compress_bv3(T,Acc2,Val,2,Len,Rest). | |
642 | compress_bv3([P|T],Acc,Val,AccLen,Len,Rest) :- %get_bool_bv(P,BoolVal),!, | |
643 | (P=pred_true -> Acc2 is Acc + (1 << AccLen) ; P=pred_false -> Acc2 = Acc), !, | |
644 | %Acc2 is Acc + BoolVal*(2^AccLen), | |
645 | AccLen2 is AccLen+1, compress_bv3(T,Acc2,Val,AccLen2,Len,Rest). | |
646 | compress_bv3(Rest,Acc,Acc,AccLen,AccLen,Rest). % we have a non BOOL value | |
647 | ||
648 | % uncompress bitvector Val of Len bits into list of pred_true, pred_false elements | |
649 | uncompress_bv(_,Len,Rest,Res) :- Len =< 0, !, Res=Rest. | |
650 | uncompress_bv(Val,Len,Rest,[BV|TRes]) :- | |
651 | (Val mod 2 =:= 1 -> BV = pred_true ; BV=pred_false), | |
652 | Val2 is Val >> 1, Len1 is Len-1, | |
653 | uncompress_bv(Val2,Len1,Rest,TRes). | |
654 | ||
655 | % ------------------------------------- | |
656 | ||
657 | % a utility to get a state as List or const_and_vars(ID,List) with list of packed values with bind/2 terms | |
658 | ||
659 | get_packed_b_state_with_uncompressed_lists(csp_and_b(_,B),Res) :- !, | |
660 | get_packed_b_state_with_uncompressed_lists(B,Res). | |
661 | get_packed_b_state_with_uncompressed_lists(const_and_vars(ID,List),const_and_vars(ID,Res)) :- | |
662 | get_packed_b_state_with_uncompressed_lists(List,Res). | |
663 | get_packed_b_state_with_uncompressed_lists('$cst_vars'(ID,CS),const_and_vars(ID,Res)) :- | |
664 | uncompress_list(CS,List), | |
665 | get_bind_skeleton(const_and_vars,Skel), | |
666 | gen_packed_bind_list(List,Skel,Res). | |
667 | get_packed_b_state_with_uncompressed_lists('$bind_lst'(Val,CT),[bind(Var1,Val)|Res]) :- uncompress_list(CT,List), | |
668 | get_bind_skeleton(list,[Var1|Skel]), | |
669 | gen_packed_bind_list(List,Skel,Res). | |
670 | ||
671 | ||
672 | gen_packed_bind_list([],[],[]). | |
673 | gen_packed_bind_list([Val|T],[Var|VT],R) :- R=[bind(Var,Val)|UPT], | |
674 | gen_packed_bind_list(T,VT,UPT). | |
675 | ||
676 | ||
677 | % ------------------------------------- | |
678 | ||
679 | ||
680 |