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