| 1 | % (c) 2009-2022 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(kodkod_process, [register_problem/7, kodkod_request_intern/5, | |
| 6 | get_original_problem/2, | |
| 7 | clear_java_comp_time/0, | |
| 8 | get_java_comp_time/1, | |
| 9 | stop_kodkod/0 | |
| 10 | ]). | |
| 11 | ||
| 12 | :- use_module(library(avl)). | |
| 13 | :- use_module(library(lists)). | |
| 14 | :- use_module(library(process)). | |
| 15 | :- use_module(library(file_systems)). | |
| 16 | ||
| 17 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 18 | :- use_module(probsrc(store), [lookup_value_for_existing_id/4]). | |
| 19 | :- use_module(probsrc(bsyntaxtree)). | |
| 20 | :- use_module(probsrc(kernel_objects), [equal_object/2]). | |
| 21 | :- use_module(probsrc(custom_explicit_sets), [expand_custom_set_to_list/2]). | |
| 22 | :- use_module(probsrc(error_manager)). | |
| 23 | :- use_module(probsrc(system_call)). | |
| 24 | :- use_module(probsrc(preferences), [get_preference/2]). | |
| 25 | :- use_module(probsrc(debug), [debug_format/3, formatsilent/2]). | |
| 26 | ||
| 27 | :- use_module(kodkodsrc(kodkod_printer)). | |
| 28 | ||
| 29 | ||
| 30 | :- module_info(group,kodkod). | |
| 31 | :- module_info(description,'This is the inter-process communication with the Java process that contains the Kodkod engine.'). | |
| 32 | ||
| 33 | :- set_prolog_flag(double_quotes, codes). | |
| 34 | ||
| 35 | :- dynamic known_problem/7, next_problem_id/1. | |
| 36 | ||
| 37 | next_problem_id(0). | |
| 38 | ||
| 39 | register_problem(Ids,KExpr,Idmap,Typemap,Valuemap,Predicate,ProblemId) :- | |
| 40 | startup_kodkod, | |
| 41 | get_new_problem_id(ProblemId), | |
| 42 | extract_all_types(Typemap,Types), | |
| 43 | extract_all_relations(Idmap,Relations), | |
| 44 | prepare_value_mapping(Valuemap,ProbToKodkodVal,KodkodToProbVal), | |
| 45 | prepare_id_mapping(Ids,Idmap,ProbToKodkodId,KodkodToProbId), | |
| 46 | assertz( known_problem(ProblemId,Types,Relations,KExpr, | |
| 47 | probkodkod(ProbToKodkodVal,ProbToKodkodId), | |
| 48 | kodkodprob(KodkodToProbVal,KodkodToProbId), | |
| 49 | Predicate) ), | |
| 50 | catch( send_problem(ProblemId), | |
| 51 | error(_,Err), % usually error(system_error,system_error('SPIO_E_NET_CONNRESET')) | |
| 52 | (format('Restarting Kodkod process due to: ~w~n',[Err]), | |
| 53 | reset_kodkod_process, | |
| 54 | startup_kodkod, | |
| 55 | send_problem(ProblemId))). | |
| 56 | ||
| 57 | get_original_problem(Id,OrigPredicate) :- | |
| 58 | known_problem(Id,_,_,_,_,_,OrigPredicate). | |
| 59 | ||
| 60 | extract_all_types(Typemap,Types) :- | |
| 61 | avl_range(Typemap,Relations), | |
| 62 | include(is_base_relation,Relations,BaseRelations), | |
| 63 | %print(extract_int_types(Relations)),nl, | |
| 64 | extract_int_types(Relations,IntTypes), | |
| 65 | %print('Result : '), print(IntTypes),nl, | |
| 66 | append(IntTypes,BaseTypes,Types), | |
| 67 | maplist(extract_type, BaseRelations, BaseTypes). | |
| 68 | ||
| 69 | is_base_relation(relation(_,_,reldef(_,_,_,_,_))). | |
| 70 | extract_type(relation(Id,Size,_Relspec),type(Id,Size)). | |
| 71 | ||
| 72 | :- use_module(kodkod_tools,[pow2integer_relation_kodkod_name/1]). | |
| 73 | extract_int_types(Relations,IntTypes) :- | |
| 74 | exclude(is_base_relation,Relations,IntRelations), | |
| 75 | extract_int_types2(IntRelations,IntTypes). | |
| 76 | extract_int_types2([],[]) :- !. | |
| 77 | extract_int_types2(IntRelations,[inttype(PowName,PowMin,PowMax,IntsetName,Min,Max)]) :- | |
| 78 | selectchk(relation(IntsetName,_,intsetrel(_Id,RMin,RMax)),IntRelations,Rest),!, | |
| 79 | % probkodkod requires 0 to be an atom (see checkIntsetArgs in Problem.java) | |
| 80 | Min is min(RMin,0), Max is max(RMax,0), | |
| 81 | extract_int_types2(Rest,RestResult), | |
| 82 | (RestResult = [inttype(PowName,PowMin,PowMax)] -> true | |
| 83 | ; RestResult = [] -> pow2integer_relation_kodkod_name(PowName), | |
| 84 | PowMin=Min, PowMax=Max % I have no idea if this is correct; TO DO: Daniel check this | |
| 85 | ). % What if RestResult is something else ??? | |
| 86 | extract_int_types2(IntRelations,[inttype(PowName,PowMin,PowMax)]) :- | |
| 87 | memberchk(relation(PowName,_,pow2rel(_Id,RPowMin,PowMax)),IntRelations),!, | |
| 88 | PowMin is min(RPowMin,0). | |
| 89 | ||
| 90 | prepare_id_mapping(Ids,Idmap,ProbToKodkod,KodkodToProb) :- | |
| 91 | prepare_id_mapping2(Ids,Idmap,ProbToKodkod,KodkodToProbList), | |
| 92 | list_to_avl(KodkodToProbList, KodkodToProb). | |
| 93 | prepare_id_mapping2([],_,[],[]). | |
| 94 | prepare_id_mapping2([TId|Rest],Idmap,[PK|ProbToKodkod],[KP|KodkodToProb]) :- | |
| 95 | prepare_id_mapping3(TId,Idmap,PK,KP), | |
| 96 | prepare_id_mapping2(Rest,Idmap,ProbToKodkod,KodkodToProb). | |
| 97 | prepare_id_mapping3(TId,Idmap,bid(BType,P)-K,K-bid(BType,P)) :- | |
| 98 | get_texpr_id(TId,P), | |
| 99 | get_texpr_type(TId,BType1), | |
| 100 | adapt_seq_type(BType1,BType), | |
| 101 | avl_fetch(P,Idmap,reldef(K,_Types,_SetOrSingle,_ExactOrSubset,_Set)). | |
| 102 | ||
| 103 | adapt_seq_type(seq(T),S) :- !,S=set(couple(integer,T)). | |
| 104 | adapt_seq_type(T,T). | |
| 105 | ||
| 106 | prepare_value_mapping(Valuemap,ProbToKodkod,KodkodToProb) :- | |
| 107 | avl_to_list(Valuemap,ProbKodkodList), | |
| 108 | maplist(reverse_key_value, ProbKodkodList, KodkodProbList), | |
| 109 | list_to_avl(KodkodProbList,KodkodToProb), | |
| 110 | maplist(remove_type_info,ProbKodkodList, L1), | |
| 111 | list_to_avl(L1,ProbToKodkod). | |
| 112 | reverse_key_value((T:P)-K, (T:K)-P). | |
| 113 | remove_type_info((_T:P)-K, P-K). | |
| 114 | ||
| 115 | get_new_problem_id(ProblemId) :- | |
| 116 | retract(next_problem_id(Id)), | |
| 117 | NextId is Id+1, | |
| 118 | assertz(next_problem_id(NextId)), | |
| 119 | ProblemId = Id. | |
| 120 | ||
| 121 | extract_all_relations(Idmap,Relations) :- avl_range(Idmap,Relations). | |
| 122 | ||
| 123 | send_problem(Id) :- | |
| 124 | get_kodkod_process(_,KOut,_), | |
| 125 | known_problem(Id,Types,Relations,Formula,_ToKodkod,_ToProB,_OrigPredicate), | |
| 126 | get_preference(time_out,TO), | |
| 127 | get_preference(kodkod_symmetry_level,Symmetry), | |
| 128 | get_preference(kodkod_sat_solver,Solver), | |
| 129 | kodkod_printer:kkp_problem(KOut,TO,Symmetry,Solver,Id,problem(Types,Relations,Formula,xxx,none)). | |
| 130 | ||
| 131 | get_kodkod_process(A,B,C) :- kodkod_process(A,B,C),!. | |
| 132 | get_kodkod_process(_,_,_) :- add_error(kodkod_process,'No Kodkod process running'),fail. | |
| 133 | ||
| 134 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 135 | % communication with external java process | |
| 136 | :- dynamic kodkod_process/3. | |
| 137 | ||
| 138 | reset_kodkod_process :- retractall(kodkod_process(_,_,_)). | |
| 139 | ||
| 140 | startup_kodkod :- kodkod_process(_,_,_), !. | |
| 141 | startup_kodkod :- | |
| 142 | absolute_file_name(prob_lib('.'), KodkodDir), | |
| 143 | kodkod_jar(KodkodJar), | |
| 144 | ||
| 145 | atom_concat('-Djava.library.path=', KodkodDir, JLibpath), | |
| 146 | ||
| 147 | get_command_path('java',CmdPath), | |
| 148 | ||
| 149 | %format('Starting Kodkod JAR ~w using ~w~n',[KodkodJar,JLibpath]), | |
| 150 | get_preference(kodkod_sat_solver,Solver), | |
| 151 | ||
| 152 | process_create(CmdPath, | |
| 153 | [JLibpath, '-Xmx1024M','-jar', KodkodJar,Solver], | |
| 154 | [process(KProc),stdout(pipe(KIn)),stdin(pipe(KOut))]), | |
| 155 | check_correct_startup(KIn), | |
| 156 | ||
| 157 | assertz(kodkod_process(KProc,KOut,KIn)). | |
| 158 | ||
| 159 | check_correct_startup(S) :- | |
| 160 | catch( (read_line(S,Line),check_first_line(Line)), | |
| 161 | E, | |
| 162 | add_error_and_fail(kodkod_process, 'Exception while connecting to Kodkod process', E)). | |
| 163 | check_first_line(Line) :- | |
| 164 | append("ProB-Kodkod started: ",Msg,Line),!, | |
| 165 | format('Kodkod module started up successfully (SAT solver ~s).~n',[Msg]). | |
| 166 | check_first_line(_Line) :- | |
| 167 | add_error_and_fail(kodkod_process,'Unable to start-up Kodkod process.\n'). | |
| 168 | ||
| 169 | kodkod_jar(KodkodJar) :- | |
| 170 | absolute_file_name(prob_lib('probkodkod.jar'), KodkodJar), | |
| 171 | ( file_exists(KodkodJar,read) -> true | |
| 172 | ; | |
| 173 | add_error_and_fail(kodkod_process,'Unable to read Kodkod library. Please check your installation or disable the use of Kodkod')). | |
| 174 | ||
| 175 | stop_kodkod :- | |
| 176 | get_kodkod_process(PId,KOut,KIn), | |
| 177 | call_cleanup( (write(KOut, 'stop.\n'), flush_output(KOut) ), | |
| 178 | ( process_wait(PId,_), close(KOut), close(KIn), | |
| 179 | retractall(kodkod_process(_,_,_)))). | |
| 180 | ||
| 181 | %kodkod_problem(Id,Problem) :- | |
| 182 | % kodkod_process(_,KOut,_), | |
| 183 | % get_preference(time_out,TO),get_preference(kodkod_symmetry_level,Symmetry),get_preference(kodkod_sat_solver,Solver), | |
| 184 | % kkp_problem(KOut,TO,Symmetry,Solver,Id,Problem). | |
| 185 | ||
| 186 | kodkod_request_intern(ProblemId, Signum, MaxNrOfSols, LocalState, State) :- | |
| 187 | known_problem(ProblemId,_Size,_Relations,_Formula,ToKodkod,ToProB,_OrigPredicate), | |
| 188 | extract_known_values(ToKodkod,LocalState,State,Known,UnknownList), | |
| 189 | copy_term(UnknownList,UnknownListCopy), | |
| 190 | list_to_avl(UnknownListCopy,Unknown), | |
| 191 | !, | |
| 192 | debug_println(19,send_kodkod_request(ProblemId,Signum,MaxNrOfSols,Known)), | |
| 193 | ? | send_request(ProblemId, ToProB, Signum, MaxNrOfSols, Known, Unknown), |
| 194 | %describe_sol(UnknownListCopy), | |
| 195 | UnknownList=UnknownListCopy. | |
| 196 | %translate:print_bstate(State). | |
| 197 | ||
| 198 | %describe_sol(List) :- | |
| 199 | % nl,write('Kodkod solution:'),nl,describe_sol2(List). | |
| 200 | %describe_sol2([]). | |
| 201 | %describe_sol2([Id-Value|Rest]) :- | |
| 202 | % describe_sol3(Id,Value), | |
| 203 | % describe_sol2(Rest). | |
| 204 | %describe_sol3(Id,Value) :- | |
| 205 | % write(Id),write(': '),translate:print_bvalue(Value),nl. | |
| 206 | ||
| 207 | ||
| 208 | extract_known_values(probkodkod(ValueMap,Ids),LocalState,State,Out,Unknown) :- | |
| 209 | extract_known_values2(Ids,ValueMap,LocalState,State,Out,[],Unknown,[]). | |
| 210 | extract_known_values2([],_ValueMap,_LocalState,_State,Known,Known,Unknown,Unknown). | |
| 211 | extract_known_values2([bid(Type,Prob)-Kodkod|Rest],ValueMap,LocalState,State, | |
| 212 | KnownIn,KnownOut,UnknownIn,UnknownOut) :- | |
| 213 | extract_known_value(Type,Prob,Kodkod,ValueMap,LocalState,State,KnownIn,KnownInter,UnknownIn,UnknownInter), | |
| 214 | extract_known_values2(Rest,ValueMap,LocalState,State,KnownInter,KnownOut,UnknownInter,UnknownOut). | |
| 215 | extract_known_value(Type,Prob,Kodkod,ValueMap,LocalState,State,KnownIn,KnownOut,UnknownIn,UnknownOut) :- | |
| 216 | lookup_value_for_existing_id(Prob,LocalState,State,Value), | |
| 217 | ( ground(Value) -> | |
| 218 | map_prob_value_to_kodkod(Type,Value,ValueMap,KValue), | |
| 219 | KnownIn = [kout(Kodkod,KValue)|KnownOut], | |
| 220 | UnknownIn = UnknownOut | |
| 221 | ; | |
| 222 | KnownIn = KnownOut, | |
| 223 | UnknownIn = [Kodkod-Value|UnknownOut]),!. | |
| 224 | extract_known_value(_Type,Prob,_Kodkod,_ValueMap,_LocalState,_State,_KnownIn,_KnownOut,_UnknownIn,_UnknownOut) :- | |
| 225 | add_error_and_fail(kodkod_process,'mapping ProB value to Kodkod failed', Prob). | |
| 226 | ||
| 227 | map_prob_value_to_kodkod(set(_),Prob,ValueMap,Kodkod) :- | |
| 228 | !, expand_custom_set_to_list(Prob,List), | |
| 229 | map_prob_values_to_kodkod(List,ValueMap,Kodkod). | |
| 230 | map_prob_value_to_kodkod(_Type,Prob,ValueMap,Kodkod) :- | |
| 231 | map_prob_values_to_kodkod([Prob],ValueMap,Kodkod). | |
| 232 | map_prob_values_to_kodkod([],_,[]). | |
| 233 | map_prob_values_to_kodkod([P|Prest],ValueMap,[tuple(K)|Krest]) :- | |
| 234 | map_prob_value_to_kodkod2(P,ValueMap,K,[]), | |
| 235 | map_prob_values_to_kodkod(Prest,ValueMap,Krest). | |
| 236 | map_prob_value_to_kodkod2((A,B),ValueMap) --> | |
| 237 | !,map_prob_value_to_kodkod2(A,ValueMap), | |
| 238 | map_prob_value_to_kodkod2(B,ValueMap). | |
| 239 | map_prob_value_to_kodkod2(int(I),_ValueMap) --> !,[I]. | |
| 240 | map_prob_value_to_kodkod2(Prob,ValueMap) --> [Kodkod], | |
| 241 | {avl_fetch(Prob,ValueMap,Kodkod)}. | |
| 242 | ||
| 243 | ||
| 244 | :- use_module(probsrc(debug),[debug_println/2]). | |
| 245 | send_request(ProblemId, ToProb, Signum, MaxNrOfSols,OutValues, In) :- | |
| 246 | get_kodkod_process(_,OStream,IStream), | |
| 247 | debug:debug_println(19,sending_kodkod_request(ProblemId,Signum,MaxNrOfSols)), | |
| 248 | kkp_request(ProblemId, Signum, MaxNrOfSols, OutValues, OStream), | |
| 249 | ? | get_solutions_from_stream(OStream,IStream,ProblemId,MaxNrOfSols,ToProb,In). |
| 250 | ||
| 251 | read_rest(ProblemId,MaxNrOfSols,ToProb,In) :- | |
| 252 | get_kodkod_process(_,OStream,IStream), | |
| 253 | kkp_list(ProblemId,MaxNrOfSols,OStream), | |
| 254 | get_solutions_from_stream(OStream,IStream,ProblemId,MaxNrOfSols,ToProb,In). | |
| 255 | ||
| 256 | get_solutions_from_stream(OStream,IStream,ProblemId,MaxNrOfSols,ToProB,In) :- | |
| 257 | flush_output(OStream), | |
| 258 | read_answer_from_kodkod(IStream,Answer), | |
| 259 | !, | |
| 260 | ? | process_answer(Answer,ProblemId,MaxNrOfSols,ToProB,In). |
| 261 | get_solutions_from_stream(_,_,ProblemId,MaxNrOfSols,ToProB,In) :- | |
| 262 | process_answer(end_of_file,ProblemId,MaxNrOfSols,ToProB,In). | |
| 263 | ||
| 264 | % read an answer but skip over statistics infos: | |
| 265 | read_answer_from_kodkod(IStream,Answer) :- | |
| 266 | read(IStream,Answer1), | |
| 267 | (Answer1=stats(T,S,C,V,P) % special statistics info fact | |
| 268 | -> debug_format(20,'Kodkod Statistics: ~w ms translation, ~w ms solving, ~w clauses, ~w variables, ~w primary variables~n',[T,S,C,V,P]), | |
| 269 | read_answer_from_kodkod(IStream,Answer) | |
| 270 | ; Answer=Answer1). | |
| 271 | ||
| 272 | process_answer(solutions(Sols,More,Times),ProblemId,MaxNrOfSols,ToProb,In) :- | |
| 273 | formatsilent('Times for computing solutions: ~w~n',[Times]), | |
| 274 | save_java_comp_time(Times), | |
| 275 | ? | get_solutions(Sols,More,ProblemId,MaxNrOfSols,ToProb,In). |
| 276 | process_answer(sat_timeout,ProblemId,_,_ToProb,_In) :- | |
| 277 | add_warning(kodkod_process,'Kodkod SAT Solver Timeout for Problem Id: ',ProblemId), | |
| 278 | %throw(time_out). % can only be caught by time_out not by catch ! | |
| 279 | throw(enumeration_warning(kodkod_timeout,ProblemId,'','',critical)). | |
| 280 | process_answer(sat_non_incremental,ProblemId,_,_ToProb,_In) :- | |
| 281 | add_warning(kodkod_process,'Kodkod SAT Solver is non incremental and cannot compute all solutions for Problem Id: ',ProblemId), | |
| 282 | throw(enumeration_warning(kodkod_timeout,ProblemId,'','',critical)). | |
| 283 | process_answer(unknown(_),ProblemId,_,_ToProb,_In) :- | |
| 284 | add_warning(kodkod_process,'Kodkod SAT Solver error occured for Problem Id: ',ProblemId), | |
| 285 | throw(enumeration_warning(kodkod_error,ProblemId,'','',critical)). | |
| 286 | process_answer(end_of_file,ProblemId,_,_ToProb,_In) :- | |
| 287 | add_warning(kodkod_process,'Kodkod SAT Solver aborted for Problem Id: ',ProblemId), | |
| 288 | throw(enumeration_warning(kodkod_error,ProblemId,'','',critical)). | |
| 289 | ||
| 290 | ||
| 291 | get_solutions(Sols,_More,_ProblemId,_,ToProb,In) :- | |
| 292 | ? | member(Sol,Sols), get_solution(Sol,ToProb,In). |
| 293 | get_solutions(_Sols,more,ProblemId,MaxNrOfSols,ToProb,In) :- | |
| 294 | read_rest(ProblemId,MaxNrOfSols,ToProb,In). | |
| 295 | ||
| 296 | get_solution([],_,_). | |
| 297 | get_solution([Binding|BRest],kodkodprob(VMap,IdMap),BValues) :- | |
| 298 | ( Binding = b(Name,KValues) -> true | |
| 299 | ; Binding = s(Name,KValues) -> Type = set(_)), | |
| 300 | avl_fetch(Name,BValues,BValue), | |
| 301 | avl_fetch(Name,IdMap,bid(Type,_BName)), | |
| 302 | ? | map_kodkod_prob(Type,KValues,VMap,Result),!, |
| 303 | equal_object(BValue,Result), | |
| 304 | get_solution(BRest,kodkodprob(VMap,IdMap),BValues). | |
| 305 | ||
| 306 | map_kodkod_prob(set(Type),Tuples,Map,Value) :- | |
| 307 | ? | !,map_kodkod_prob2(Tuples,Type,Map,Value). |
| 308 | map_kodkod_prob(Type,KValue,Map,BValue) :- | |
| 309 | map_kodkod_prob2([KValue],Type,Map,[BValue]). | |
| 310 | map_kodkod_prob2([],_,_,[]). | |
| 311 | map_kodkod_prob2([Values|TRest],Type,Map,[BValue|BRest]) :- | |
| 312 | ? | map_kodkod_prob3(Type,Map,BValue,Values,[]), |
| 313 | ? | map_kodkod_prob2(TRest,Type,Map,BRest). |
| 314 | map_kodkod_prob3(couple(TA,TB),Map,(BA,BB)) --> | |
| 315 | ? | map_kodkod_prob3(TA,Map,BA), |
| 316 | map_kodkod_prob3(TB,Map,BB). | |
| 317 | map_kodkod_prob3(integer,_,int(Value)) --> !,[Value]. | |
| 318 | map_kodkod_prob3(Type,Map,BValue) --> | |
| 319 | [K],{avl_fetch(Type:K,Map,BValue),!}. | |
| 320 | ||
| 321 | :- dynamic java_comp_time/1. | |
| 322 | clear_java_comp_time :- | |
| 323 | retractall(java_comp_time(_)). | |
| 324 | get_java_comp_time(Time) :- | |
| 325 | findall( T, (java_comp_time(Ts),member(T,Ts)), Times), | |
| 326 | sumlist(Times,Time). | |
| 327 | save_java_comp_time(Times) :- | |
| 328 | assertz(java_comp_time(Times)). |