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