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