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