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