1 | % (c) 2009-2019 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 | incremental_pack_state/4, | |
9 | pack_values/2, unpack_values/2, | |
10 | pack_value/2, unpack_value/2, | |
11 | print_stored_values/0, retract_stored_values_with_statistics/0]). | |
12 | ||
13 | % a module to pack/compress states before asserting them in state_space | |
14 | :- use_module(specfile,[ csp_mode/0]). % b_or_z_mode/0, | |
15 | :- use_module(tools). | |
16 | :- use_module(b_global_sets). | |
17 | :- use_module(error_manager). | |
18 | ||
19 | :- use_module(module_information). | |
20 | :- module_info(group,animator). | |
21 | :- module_info(description,'This module packs and upacks states and values.'). | |
22 | ||
23 | :- dynamic bind_skeleton/2. % stores the list of variable names | |
24 | % we assume they are always in the same order; otherwise there is a problem | |
25 | % 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) | |
26 | ||
27 | %pack_state(S,R) :- tools_printing:print_term_summary(S),nl,fail. | |
28 | pack_state(root,R) :- !, R=root. | |
29 | 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 !! | |
30 | !, | |
31 | R='$cst_vars'(ID,PCS), | |
32 | % debug:time(state_packing:pack_bind_list(S,PS)). | |
33 | (bind_skeleton(const_and_vars,Skel) -> pack_bind_list(S,Skel,PS) | |
34 | ; pack_bind_list(S,Skel,PS), %print(vskel(Skel)),nl, | |
35 | (bind_skeleton(const_and_vars,OtherList) | |
36 | -> add_internal_error('Multiple bind skeletons:',OtherList:Skel) ; true), | |
37 | assert(bind_skeleton(const_and_vars,Skel))), | |
38 | compress_list(PS,PCS). | |
39 | %pack_state(concrete_constants(S),R) :- !, . % leads to further reduction in memory consumption, but to a slowdown | |
40 | % R = '$cst'(PCS), | |
41 | % (bind_skeleton(concrete_constants,Skel) -> pack_bind_list(S,Skel,PS) | |
42 | % ; pack_bind_list(S,Skel,PS), %print(vskel(Skel)),nl, | |
43 | % assert(bind_skeleton(concrete_constants,Skel))), | |
44 | % compress_list(PS,PCS). | |
45 | 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 | |
46 | !, | |
47 | R='$bind_lst'(PV1,PCT), | |
48 | pack_value(Val,PV), | |
49 | (bind_skeleton(list,[V|Skel]) | |
50 | -> PV1=PV,pack_bind_list(T,Skel,PT1) | |
51 | ; pack_bind_list(T,Skel,PT), | |
52 | (bind_skeleton(list,OtherList) | |
53 | -> add_warning(pack_state,'Multiple bind skeletons:',OtherList:[V|Skel]), | |
54 | reorder(OtherList,[V|Skel],[PV|PT],[PV1|PT1]), print(reordered(PT1)),nl | |
55 | ; assert(bind_skeleton(list,[V|Skel])), PT=PT1,PV=PV1 | |
56 | ) | |
57 | ), | |
58 | compress_list(PT1,PCT). | |
59 | pack_state(csp_and_b(CSP,B),R) :- !, R=csp_and_b(PCSP,PB), | |
60 | pack_state(CSP,PCSP), | |
61 | pack_state(B,PB). | |
62 | pack_state(CSP,R) :- | |
63 | preference(use_state_packing,true),csp_mode,!, | |
64 | pack_csp_expression(CSP,PCSP), R=PCSP. | |
65 | pack_state(V,V). | |
66 | ||
67 | :- use_module(library(lists),[nth1/3]). | |
68 | reorder([],_,_,[]). | |
69 | reorder([ID|T1],Skel,Vals,[V2|T2]) :- nth1(Nr,Skel,ID), nth1(Nr,Vals,V2),!, | |
70 | reorder(T1,Skel,Vals,T2). | |
71 | reorder([ID|T1],Skel,Vals,Res) :- add_internal_error('Cannot find identifier:',ID), | |
72 | reorder(T1,Skel,Vals,Res). | |
73 | ||
74 | %compress_list([A,B,C,D|T],l4(A,B,C,D,CT)) :- !, compress_list(T,CT). | |
75 | %compress_list(List,'$bitvector'(Val,Len,CT)) :- compress_bv(List,Val,Len,T), !, compress_list(T,CT). | |
76 | compress_list([A,B,C|T],l3(A,B,C,CT)) :- !, compress_list(T,CT). | |
77 | %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) ? | |
78 | compress_list(T,T). | |
79 | ||
80 | %uncompress_list(l2(A,B,CT),[A,B|T]) :- uncompress_list(CT,T). | |
81 | uncompress_list(l3(A,B,C,CT),[A,B,C|T]) :- !, uncompress_list(CT,T). | |
82 | %uncompress_list('$bitvector'(Val,Len,CT),Res) :- !, uncompress_bv(Val,Len,T,Res), uncompress_list(CT,T). | |
83 | %uncompress_list(l3c(ID,CT),[A,B,C|T]) :- stored_value(ID,(A,B,C)),!,uncompress_list(CT,T). | |
84 | %uncompress_list(l4(A,B,C,D,CT),[A,B,C,D|T]) :- uncompress_list(CT,T). | |
85 | uncompress_list(T,T). | |
86 | ||
87 | ||
88 | :- use_module(error_manager,[add_internal_error/2]). | |
89 | pack_bind_list([],[],R) :- !,R=[]. | |
90 | pack_bind_list([bind(V,Val)|T],[V|VT],R) :- !,R=[PV|PT], | |
91 | pack_value(Val,PV), | |
92 | pack_bind_list(T,VT,PT). | |
93 | pack_bind_list(V,VT,R) :- | |
94 | add_internal_error('Illegal value: ',pack_bind_list(V,VT,R)),R=V. | |
95 | ||
96 | ||
97 | :- use_module(library(avl)). | |
98 | unpack_state(root,State) :- !, State=root. | |
99 | unpack_state(concrete_constants(C),State) :- !, State=concrete_constants(C). % comment out in case concrete_constants are packed after all | |
100 | unpack_state(PackedState,State) :- %empty_avl(E), %tools_printing:print_term_summary(unpack(PackedState,State)),nl, % trace, | |
101 | %tools_printing:print_term_summary(unpack_state(PackedState)), | |
102 | unpack_state2(PackedState,State). | |
103 | ||
104 | %unpack_state(concrete_constants(S),R) --> {b_or_z_mode},!, {R=concrete_constants(UPS)}, unpack_state(S,UPS). % leads to further reduction | |
105 | unpack_state2(const_and_vars(ID,CS),R) :- !, | |
106 | R=const_and_vars(ID,UPS), | |
107 | unpack_state2(CS,UPS). | |
108 | %unpack_state2('$cst'(CS),R) :- !, | |
109 | % R=concrete_constants(UPS), | |
110 | % uncompress_list(CS,S),get_bind_skeleton(concrete_constants,Skel), | |
111 | % unpack_bind_list(S,Skel,UPS). | |
112 | 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 | |
113 | !, | |
114 | R=const_and_vars(ID,UPS), | |
115 | uncompress_list(CS,S),get_bind_skeleton(const_and_vars,Skel), | |
116 | unpack_bind_list(S,Skel,UPS). | |
117 | unpack_state2('$bind_lst'(Val,CT),R) :- % {b_or_z_mode}, we assume $bind_lst not used by any plug-in | |
118 | !, | |
119 | uncompress_list(CT,T),get_bind_skeleton(list,[Var|Skel]),R=[bind(Var,UPV)|RT], | |
120 | unpack_value(Val,UPV), %!, | |
121 | unpack_bind_list(T,Skel,RT). | |
122 | unpack_state2(csp_and_b(CSP,B),csp_and_b(UPCSP,UPB)) :- !, unpack_state2(CSP,UPCSP), | |
123 | unpack_state2(B,UPB). | |
124 | unpack_state2(PCSP,R) :- | |
125 | csp_mode,preference(use_state_packing,true),!, | |
126 | unpack_csp_expression(PCSP,R). | |
127 | unpack_state2(R,R). | |
128 | ||
129 | unpack_bind_list([],[],[]). | |
130 | unpack_bind_list([Val|T],[Var|VT],R) :- R=[bind(Var,UPV)|UPT], | |
131 | unpack_value(Val,UPV), %!, | |
132 | unpack_bind_list(T,VT,UPT). | |
133 | %unpack_bind_list('$bind_lst'(Var,Val,_),_) --> {add_internal_error('Unpacking value failed: ',Var/Val),fail}. | |
134 | ||
135 | ||
136 | get_bind_skeleton(Category,X) :- | |
137 | (bind_skeleton(Category,X) -> true | |
138 | ; add_internal_error('No bind skeleton stored for: ',get_bind_skeleton(Category,X)),fail). | |
139 | ||
140 | % a simpler version for list of bind-pairs; does not require bind_skeleton to be set up / stored | |
141 | pack_values([],[]) :- !. | |
142 | pack_values([bind(V,Val)|T],R) :- !,R=[Bind|PT], | |
143 | pack_bind(Val,V,Bind), | |
144 | pack_values(T,PT). | |
145 | pack_values(V,R) :- add_internal_error('Illegal value: ',pack_values(V,R)),R=V. | |
146 | ||
147 | pack_bind([],V,R) :- !, R='$bind_empty_set'(V). | |
148 | pack_bind(pred_false,V,R) :- !, R='$bind_false'(V). % bind boolean values | |
149 | pack_bind(pred_true,V,R) :- !, R='$bind_true'(V). | |
150 | pack_bind(Val,V,'$bind'(V,PV)) :- pack_value(Val,PV). | |
151 | ||
152 | unpack_bind('$bind_empty_set'(V),V,[]). | |
153 | unpack_bind('$bind_false'(V),V,pred_false). | |
154 | unpack_bind('$bind_true'(V),V,pred_true). | |
155 | unpack_bind('$bind'(V,PV),V,Val) :- unpack_value(PV,Val). | |
156 | ||
157 | unpack_values([],[]) :- !. | |
158 | unpack_values([PBind|T],R) :- unpack_bind(PBind,V,Val),!, | |
159 | R=[bind(V,Val)|UPT], | |
160 | unpack_values(T,UPT). | |
161 | unpack_values(V,R) :- add_internal_error('Illegal value: ',unpack_values(V,R)),R=V. | |
162 | ||
163 | ||
164 | :- use_module(library(avl)). | |
165 | :- use_module(preferences,[preference/2]). | |
166 | :- use_module(custom_explicit_sets,[is_interval_closure/5, construct_interval_closure/3]). | |
167 | ||
168 | pack_value(Var,R) :- var(Var),!, | |
169 | add_internal_error('Illegal variable value: ', pack_value(Var,R)), | |
170 | R='$variable'(Var). | |
171 | pack_value(avl_set(A),R) :- !, %R\==[], | |
172 | avl_domain(A,AD), | |
173 | %avl_packed_domain(A,ADL,[]), | |
174 | (pack_fd_set(AD,Type,PackedInteger) -> R = '$avl_bv'(PackedInteger,Type) % avl bit vector %, print(packed(PackedInteger,AD)),nl | |
175 | ; l_pack_value(AD,ADL), | |
176 | (preferences:preference(use_state_packing,true) %ADL=[_,_|_] | |
177 | -> R='$stored_avl'(ID),store_value(ADL,ID) | |
178 | % , print(stored(ID,ADL)),nl | |
179 | ; R='$avl_exp'(ADL)) % ,print(packed(A,R)),nl | |
180 | ). | |
181 | pack_value((A,B),(PA,PB)) :- !, pack_value(A,PA), pack_value(B,PB). | |
182 | pack_value(fd(Nr,T),R) :- pack_basic_fd_value(T,Nr,Atom),!,Atom=R. | |
183 | pack_value(int(Nr),R) :- !, R=Nr. | |
184 | pack_value(closure(P,T,B),R) :- is_interval_closure(P,T,B,Low,Up),!, | |
185 | %print(pack_interval(Low,Up,B)),nl, | |
186 | R='$interval'(Low,Up). | |
187 | %pack_value(closure(P,T,B),R) :- is_cartesian_product_closure(CPA,A1,A2),!, | |
188 | % R='$cartesian_product'(PA1,PA2), | |
189 | % pack_value(A1,PA1), pack_value(A2,PA2). | |
190 | pack_value(V,V). | |
191 | % to do: records + maybe closures (interval-closures,... ?) | |
192 | ||
193 | /* not worth it : | |
194 | % compute avl_domain and apply pack_value in one go: | |
195 | avl_packed_domain(empty, Domain, Domain). | |
196 | avl_packed_domain(node(Key,_,_,L,R), Domain0, Domain) :- | |
197 | pack_value(Key,PKey), | |
198 | avl_packed_domain(L, Domain0, [PKey|Domain1]), | |
199 | avl_packed_domain(R, Domain1, Domain). | |
200 | */ | |
201 | ||
202 | l_pack_value([],[]). | |
203 | l_pack_value([H|T],[PH|PT]) :- pack_value(H,PH), l_pack_value(T,PT). | |
204 | ||
205 | % TO DO or [(fd,fd) as bit-vectors if <xx bits | |
206 | ||
207 | % Pack set of FD values as bit-vector representation | |
208 | pack_fd_set([fd(X,Type)|T],Type,Result) :- | |
209 | b_global_sets:b_get_fd_type_bounds(Type,1,UpBound), | |
210 | (UpBound < 28 -> true /* we are ok on 32-bit systems */ | |
211 | ; UpBound < 60, platform_is_64_bit), /* prolog_flag(max_tagged_integer,X), Y is 1<<59, Y<X. */ | |
212 | Acc is 1<<X, | |
213 | pack_fd_set_aux(T,Acc,Result). | |
214 | ||
215 | pack_fd_set_aux([],A,A). | |
216 | pack_fd_set_aux([fd(X,_)|T],Acc,Res) :- | |
217 | NewAcc is Acc \/ (1<<X), | |
218 | pack_fd_set_aux(T,NewAcc,Res). | |
219 | ||
220 | % unpack a bit-vector set representation | |
221 | unpack_fd_set(PackedInteger,Type,Value) :- | |
222 | unpack_fd_set_aux(PackedInteger,0,Type,ResList), %print(unpacked(PackedInteger,ResList)),nl, | |
223 | custom_explicit_sets:ord_list_to_avlset_direct(ResList,Value,unpack_fd_set). | |
224 | ||
225 | unpack_fd_set_aux(0,_,_,Res) :- !, Res=[]. | |
226 | unpack_fd_set_aux(Nr,X,Type,Res) :- | |
227 | (Nr mod 2 =:= 1 -> Res = [fd(X,Type)-true|T] ; Res=T), | |
228 | X1 is X+1, Nr1 is (Nr>>1), | |
229 | unpack_fd_set_aux(Nr1,X1,Type,T). | |
230 | ||
231 | % first rough attempt at packing CSP expressions | |
232 | pack_csp_expression(esharing(Set,B,C,Span),'$esharing'(PSet,PB,PC,PSpan)) :- !, | |
233 | pack_csp_expression(Set,PSet), pack_csp_expression(B,PB), | |
234 | pack_csp_expression(C,PC), pack_csp_expression(Span,PSpan). | |
235 | pack_csp_expression('|||'(A,B,Span),'|||'(PA,PB,PSpan)) :- !, | |
236 | pack_csp_expression(A,PA), pack_csp_expression(B,PB), pack_csp_expression(Span,PSpan). | |
237 | %pack_csp_expression('&'(A,B),'&'(PA,PB)) :- !, | |
238 | % pack_csp_expression(A,PA), pack_csp_expression(B,PB). | |
239 | pack_csp_expression('[]'(A,B,Span),'[]'(PA,PB,PSpan)) :- !, | |
240 | pack_csp_expression(A,PA), pack_csp_expression(B,PB), pack_csp_expression(Span,PSpan). | |
241 | pack_csp_expression(eaParallel(C,A,D,B,Span),eaParallel(PC,PA,PD,PB,PSpan)) :- !, | |
242 | pack_csp_expression(A,PA), pack_csp_expression(B,PB), pack_csp_expression(C,PC), | |
243 | pack_csp_expression(D,PD), pack_csp_expression(Span,PSpan). | |
244 | %pack_csp_expression(prefix(C,A,D,B,Span),prefix(PC,PA,PD,PB,PSpan)) :- !, | |
245 | % pack_csp_expression(A,PA), pack_csp_expression(B,PB), pack_csp_expression(C,PC), | |
246 | % pack_csp_expression(D,PD), pack_csp_expression(Span,PSpan). | |
247 | %pack_csp_expression(ifte(C,A,D,B,Span,S3),ifte(PC,PA,PD,PB,PSpan,S3)) :- !, | |
248 | % pack_csp_expression(A,PA), pack_csp_expression(B,PB), pack_csp_expression(C,PC), | |
249 | % pack_csp_expression(D,PD), pack_csp_expression(Span,PSpan). | |
250 | %pack_csp_expression(V,'$stored_csp'(ID)) :- store_value(V,ID). | |
251 | pack_csp_expression(V,ID) :- store_value(V,ID). | |
252 | ||
253 | unpack_csp_expression('$esharing'(PSet,PB,PC,PSpan),esharing(Set,B,C,Span)) :- !, | |
254 | unpack_csp_expression(PSet,Set), unpack_csp_expression(PB,B), | |
255 | unpack_csp_expression(PC,C), unpack_csp_expression(PSpan,Span). | |
256 | unpack_csp_expression('|||'(A,B,Span),'|||'(PA,PB,PSpan)) :- !, | |
257 | unpack_csp_expression(A,PA), unpack_csp_expression(B,PB), unpack_csp_expression(Span,PSpan). | |
258 | %unpack_csp_expression('&'(A,B),'&'(PA,PB)) :- !, | |
259 | % unpack_csp_expression(A,PA), unpack_csp_expression(B,PB). | |
260 | unpack_csp_expression('[]'(A,B,Span),'[]'(PA,PB,PSpan)) :- !, | |
261 | unpack_csp_expression(A,PA), unpack_csp_expression(B,PB), unpack_csp_expression(Span,PSpan). | |
262 | unpack_csp_expression(eaParallel(C,A,D,B,Span),eaParallel(PC,PA,PD,PB,PSpan)) :- !, | |
263 | unpack_csp_expression(A,PA), unpack_csp_expression(B,PB), unpack_csp_expression(C,PC), | |
264 | unpack_csp_expression(D,PD), unpack_csp_expression(Span,PSpan). | |
265 | %unpack_csp_expression(prefix(C,A,D,B,Span),prefix(PC,PA,PD,PB,PSpan)) :- !, | |
266 | % unpack_csp_expression(A,PA), unpack_csp_expression(B,PB), unpack_csp_expression(C,PC), | |
267 | % unpack_csp_expression(D,PD), unpack_csp_expression(Span,PSpan). | |
268 | %unpack_csp_expression(ifte(C,A,D,B,Span,S3),ifte(PC,PA,PD,PB,PSpan,S3)) :- !, | |
269 | % unpack_csp_expression(A,PA), unpack_csp_expression(B,PB), unpack_csp_expression(C,PC), | |
270 | % unpack_csp_expression(D,PD), unpack_csp_expression(Span,PSpan). | |
271 | %unpack_csp_expression('$stored_csp'(ID),V) :- !, stored_value(ID,V). | |
272 | unpack_csp_expression(ID,V) :- !, stored_value(ID,V). | |
273 | unpack_csp_expression(V,V). | |
274 | ||
275 | %unpack_value(Val,UPVal) :- unpack_value(Val,UPVal,empty,_). | |
276 | ||
277 | unpack_value(V,R) :- var(V),!, | |
278 | add_internal_error('Illegal variable value: ', unpack_value(V,R)), R=V. | |
279 | unpack_value('$avl_exp'(AD),R) :- !, unpack_avl_expanded(AD,R). | |
280 | unpack_value('$stored_avl'(ID),R) :- !, | |
281 | (stored_value(ID,Val) -> true ; add_internal_error('No stored AVL: ',ID),fail), | |
282 | unpack_avl_expanded(Val,R). | |
283 | unpack_value('$avl_bv'(PackedInteger,Type),R) :- !, unpack_fd_set(PackedInteger,Type,R). | |
284 | /* comment in and re-add DCG to try and re-construct sharing; does seem to increase memory usage for vital_gradient_values | |
285 | unpack_value('$stored_avl'(ID),R,InEnv,OutEnv) :- !, | |
286 | (avl_fetch(ID,InEnv,ER) %(expanded(ID,ER),InEnv) | |
287 | -> R = ER, OutEnv=InEnv % reuse the already expanded value: will also decrease memory consumption due to sharing | |
288 | ; stored_value(ID,Val), | |
289 | avl_store(ID,InEnv,R,InEnv2), % OutEnv=[expanded(ID,R)|OutEnv2], % note: ID cannot occur inside Val | |
290 | unpack_avl_expanded(Val,R,InEnv2,OutEnv)). | |
291 | */ | |
292 | %unpack_value('$cartesian_product'(A,B),R) :- unpack_value(A,PA), unpack_value(B,PB), | |
293 | % construct_cartesian_product_closure(PA,PB,R). | |
294 | unpack_value('$interval'(A,B),R) :- !, construct_interval_closure(A,B,R). | |
295 | unpack_value((A,B),(PA,PB)) :- !, unpack_value(A,PA), unpack_value(B,PB). | |
296 | unpack_value(Nr,R) :- number(Nr),!, R=int(Nr). | |
297 | unpack_value(V,UPV) :- unpack_basic_fd_value(V,FD),!,UPV=FD. | |
298 | unpack_value(V,V). | |
299 | ||
300 | unpack_avl_expanded(AD,R) :- | |
301 | l_unpack_value(AD,ADT), | |
302 | custom_explicit_sets:ord_list_to_avlset_direct(ADT,R,unpack_value). | |
303 | ||
304 | l_unpack_value([],[]). | |
305 | l_unpack_value([H|T],[PH-true|PT]) :- unpack_value(H,PH), l_unpack_value(T,PT). | |
306 | ||
307 | % ------------------------- | |
308 | ||
309 | % a version of pack_state which makes use of a previously packed state and a ordered list of written variables | |
310 | % incremental_pack_state(State,PrevPackedState,WrittenVariables,PackedState) | |
311 | % The idea is to re-use the packed values from the previous state if possible | |
312 | ||
313 | % Note: bind_skeleton does not need to be stored as these clauses only apply when previous state of same type exists | |
314 | incremental_pack_state(const_and_vars(ID,T),'$cst_vars'(ID,PrevCT),Written,'$cst_vars'(ID,PCT)) :- !, | |
315 | uncompress_list(PrevCT,PrevT), | |
316 | incr_pack_bind_list(T,PrevT,Written,PT), | |
317 | compress_list(PT,PCT). | |
318 | incremental_pack_state([bind(V,Val)|T],'$bind_lst'(PrevV,PrevCT),Written,'$bind_lst'(PV,PCT)) :- !, | |
319 | uncompress_list(PrevCT,PrevT), | |
320 | incremental_pack_value(Val,V,PrevV,Written,PV), | |
321 | incr_pack_bind_list(T,PrevT,Written,PT), | |
322 | compress_list(PT,PCT). | |
323 | incremental_pack_state(State,_,_,PackedState) :- pack_state(State,PackedState). | |
324 | ||
325 | :- use_module(library(ordsets),[ord_member/2]). | |
326 | incremental_pack_value(int(Nr),_,_,_W,R) :- !, R=Nr. | |
327 | incremental_pack_value(Val,_,_,_W,R) :- not_packed(Val),!, R=Val. | |
328 | incremental_pack_value(Val,Var,_Prev,Written,PackedValue) :- ord_member(Var,Written), !, | |
329 | pack_value(Val,PackedValue). | |
330 | incremental_pack_value(_,_,PrevPackVal,_W,PrevPackVal). % copy previously packed value | |
331 | ||
332 | not_packed(pred_false). | |
333 | not_packed(pred_true). | |
334 | not_packed(string(_)). | |
335 | ||
336 | incr_pack_bind_list([],_,_,[]). | |
337 | incr_pack_bind_list([bind(V,Val)|T],[PrevV|PrevT],Written,[PackedValue|PT]) :- | |
338 | incremental_pack_value(Val,V,PrevV,Written,PackedValue), | |
339 | incr_pack_bind_list(T,PrevT,Written,PT). | |
340 | ||
341 | % ------------------------- | |
342 | ||
343 | :- dynamic pack_basic_fd_value/3, unpack_basic_fd_value/2. | |
344 | % associate precompiled atoms with all enumerated & deferred set elements; TO DO: only do for "smaller" SETS | |
345 | precompile_state_packing :- | |
346 | retractall(pack_basic_fd_value(_,_,_)), | |
347 | retractall(unpack_basic_fd_value(_,_)), | |
348 | ? | b_global_sets:enum_global_type(fd(Nr,T),_), |
349 | string_concatenate('$fd_',T,FDT), | |
350 | string_concatenate(FDT,Nr,NewAtom), | |
351 | %debug:debug_println(9,pack(T,Nr,NewAtom)), | |
352 | assert(pack_basic_fd_value(T,Nr,NewAtom)), | |
353 | assert(unpack_basic_fd_value(NewAtom,fd(Nr,T))),fail. | |
354 | precompile_state_packing. | |
355 | ||
356 | % ------------------------ | |
357 | ||
358 | :- dynamic stored_value/2, stored_value_hash_to_id/2, next_value_id/1. | |
359 | next_value_id(0). | |
360 | ||
361 | reset_stored_values :- | |
362 | retractall(bind_skeleton(_,_)), | |
363 | retractall(stored_value(_,_)), | |
364 | retractall(stored_value_hash_to_id(_,_)), | |
365 | retractall(next_value_id(_)), assert(next_value_id(0)). | |
366 | ||
367 | :- use_module(library(terms),[term_hash/3]). | |
368 | store_value(Value,ID) :- | |
369 | term_hash(Value,[range(smallint),algorithm(sdbm), depth(infinite),if_var(ignore)],Hash), | |
370 | %hashing:my_term_hash(Value,Hash), | |
371 | store_value_aux(Value,Hash,ID). | |
372 | ||
373 | store_value_aux(Value,Hash,ID) :- | |
374 | stored_value_hash_to_id(Hash,ID), | |
375 | stored_value(ID,Value),!. % we have already stored the value | |
376 | store_value_aux(Value,Hash,ID) :- | |
377 | retract(next_value_id(NID)), NID1 is NID+1, | |
378 | assert(next_value_id(NID1)), | |
379 | assert(stored_value(NID,Value)), assert(stored_value_hash_to_id(Hash,NID)), | |
380 | ID=NID. | |
381 | ||
382 | :- use_module(tools_printing, [print_dynamic_pred/3]). | |
383 | % state_packing:print_stored_values | |
384 | print_stored_values :- % for saving state_space to file | |
385 | print_dynamic_pred(state_packing,bind_skeleton,2), | |
386 | print_dynamic_pred(state_packing,stored_value,2), | |
387 | print_dynamic_pred(state_packing,stored_value_hash_to_id,2), | |
388 | print_dynamic_pred(state_packing,next_value_id,1). | |
389 | ||
390 | ||
391 | retract_stored_values_with_statistics :- | |
392 | retract_with_statistics(state_packing,[stored_value(_,_), | |
393 | stored_value_hash_to_id(_,_)]), | |
394 | reset_stored_values. | |
395 | ||
396 | % ------------------------------------- | |
397 | ||
398 | % utility to translate boolean variables into bit-vector integers (not used yet; degrades performance) | |
399 | ||
400 | :- use_module(self_check). | |
401 | :- 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)). | |
402 | :- 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)). | |
403 | :- 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)). | |
404 | ||
405 | % compress successive boolean values (at least 2) | |
406 | compress_bv([P|T],Val,Len,Rest) :- get_bool_bv(P,Acc), compress_bv2(T,Acc,Val,Len,Rest). | |
407 | get_bool_bv(pred_true,1). | |
408 | get_bool_bv(pred_false,0). | |
409 | compress_bv2([P|T],Acc,Val,Len,Rest) :- get_bool_bv(P,BoolVal),!, | |
410 | Acc2 is Acc + BoolVal*2, % BoolVal+(Acc << 1), | |
411 | compress_bv3(T,Acc2,Val,2,Len,Rest). | |
412 | compress_bv3([P|T],Acc,Val,AccLen,Len,Rest) :- %get_bool_bv(P,BoolVal),!, | |
413 | (P=pred_true -> Acc2 is Acc + (1 << AccLen) ; P=pred_false -> Acc2 = Acc), !, | |
414 | %Acc2 is Acc + BoolVal*(2^AccLen), | |
415 | AccLen2 is AccLen+1, compress_bv3(T,Acc2,Val,AccLen2,Len,Rest). | |
416 | compress_bv3(Rest,Acc,Acc,AccLen,AccLen,Rest). | |
417 | ||
418 | % uncompress bitvector Val of Len bits into list of pred_true, pred_false elements | |
419 | uncompress_bv(_,Len,Rest,Res) :- Len =< 0, !, Res=Rest. | |
420 | uncompress_bv(Val,Len,Rest,[BV|TRes]) :- | |
421 | (Val mod 2 =:= 1 -> BV = pred_true ; BV=pred_false), | |
422 | Val2 is Val >> 1, Len1 is Len-1, | |
423 | uncompress_bv(Val2,Len1,Rest,TRes). | |
424 | ||
425 |