kodkod_process

adapt_seq_type(seq(T),S) :- !,S=set(couple(integer,T)).

adapt_seq_type(T,T).

check_correct_startup(S) :-
    catch( (read_line(S,Line),check_first_line(Line)),
    E,
    add_error_and_fail(kodkod_process, 'Exception while connecting to Kodkod process', E)).

check_first_line(Line) :-
    append("ProB-Kodkod started: ",Msg,Line),!,
    format('Kodkod module started up successfully (SAT solver ~s).~n',[Msg]).

check_first_line(_Line) :-
    add_error_and_fail(kodkod_process,'Unable to start-up Kodkod process.\n').

clear_java_comp_time :-
    retractall(java_comp_time(_)).

extract_all_relations(Idmap,Relations) :- avl_range(Idmap,Relations).

extract_all_types(Typemap,Types) :-
    avl_range(Typemap,Relations),
    include(is_base_relation,Relations,BaseRelations),
    %print(extract_int_types(Relations)),nl,
    extract_int_types(Relations,IntTypes),
    %print('Result : '), print(IntTypes),nl,
    append(IntTypes,BaseTypes,Types),
    maplist(extract_type, BaseRelations, BaseTypes).

extract_int_types(Relations,IntTypes) :-
    exclude(is_base_relation,Relations,IntRelations),
    extract_int_types2(IntRelations,IntTypes).

extract_int_types2([],[]) :- !.

extract_int_types2(IntRelations,[inttype(PowName,PowMin,PowMax,IntsetName,Min,Max)]) :-
    selectchk(relation(IntsetName,_,intsetrel(_Id,RMin,Max)),IntRelations,Rest),!,
    Min is min(RMin,0),
    extract_int_types2(Rest,RestResult),
    (RestResult = [inttype(PowName,PowMin,PowMax)] -> true
    ; RestResult = [] -> pow2integer_relation_kodkod_name(PowName),
    PowMin=Min, PowMax=Max % I have no idea if this is correct; TO DO: Daniel check this
). % What if RestResult is something else ???

extract_int_types2(IntRelations,[inttype(PowName,PowMin,PowMax)]) :-
    memberchk(relation(PowName,_,pow2rel(_Id,RPowMin,PowMax)),IntRelations),!,
    PowMin is min(RPowMin,0).

extract_known_value(Type,Prob,Kodkod,ValueMap,LocalState,State,KnownIn,KnownOut,UnknownIn,UnknownOut) :-
    lookup_value_for_existing_id(Prob,LocalState,State,Value),
    ( ground(Value) ->
    map_prob_value_to_kodkod(Type,Value,ValueMap,KValue),
    KnownIn = [kout(Kodkod,KValue)|KnownOut],
    UnknownIn = UnknownOut
    ;
    KnownIn = KnownOut,
    UnknownIn = [Kodkod-Value|UnknownOut]),!.

extract_known_value(_Type,Prob,_Kodkod,_ValueMap,_LocalState,_State,_KnownIn,_KnownOut,_UnknownIn,_UnknownOut) :-
    add_error_and_fail(kodkod_process,'mapping ProB value to Kodkod failed', Prob).

extract_known_values(probkodkod(ValueMap,Ids),LocalState,State,Out,Unknown) :-
    extract_known_values2(Ids,ValueMap,LocalState,State,Out,[],Unknown,[]).

extract_known_values2([],_ValueMap,_LocalState,_State,Known,Known,Unknown,Unknown).

extract_known_values2([bid(Type,Prob)-Kodkod|Rest],ValueMap,LocalState,State,
    KnownIn,KnownOut,UnknownIn,UnknownOut) :-
    extract_known_value(Type,Prob,Kodkod,ValueMap,LocalState,State,KnownIn,KnownInter,UnknownIn,UnknownInter),
    extract_known_values2(Rest,ValueMap,LocalState,State,KnownInter,KnownOut,UnknownInter,UnknownOut).

extract_type(relation(Id,Size,_Relspec),type(Id,Size)).

get_java_comp_time(Time) :-
    findall( T, (java_comp_time(Ts),member(T,Ts)), Times),
    sumlist(Times,Time).

get_kodkod_process(A,B,C) :- kodkod_process(A,B,C),!.

get_kodkod_process(_,_,_) :- add_error(kodkod_process,'No Kodkod process running'),fail.

get_new_problem_id(ProblemId) :-
    retract(next_problem_id(Id)),
    NextId is Id+1,
    assertz(next_problem_id(NextId)),
    ProblemId = Id.

get_original_problem(Id,OrigPredicate) :-
    known_problem(Id,_,_,_,_,_,OrigPredicate).

get_solution([],_,_).

get_solution([Binding|BRest],kodkodprob(VMap,IdMap),BValues) :-
    ( Binding = b(Name,KValues) -> true
    ; Binding = s(Name,KValues) -> Type = set(_)),
    avl_fetch(Name,BValues,BValue),
    avl_fetch(Name,IdMap,bid(Type,_BName)),
    map_kodkod_prob(Type,KValues,VMap,Result),!,
    equal_object(BValue,Result),
    get_solution(BRest,kodkodprob(VMap,IdMap),BValues).

get_solutions(Sols,_More,_ProblemId,_,ToProb,In) :-
    member(Sol,Sols), get_solution(Sol,ToProb,In).

get_solutions(_Sols,more,ProblemId,MaxNrOfSols,ToProb,In) :-
    read_rest(ProblemId,MaxNrOfSols,ToProb,In).

get_solutions_from_stream(OStream,IStream,ProblemId,MaxNrOfSols,ToProB,In) :-
    flush_output(OStream),
    read_answer_from_kodkod(IStream,Answer),
    !,
    process_answer(Answer,ProblemId,MaxNrOfSols,ToProB,In).

get_solutions_from_stream(_,_,ProblemId,MaxNrOfSols,ToProB,In) :-
    process_answer(end_of_file,ProblemId,MaxNrOfSols,ToProB,In).

is_base_relation(relation(_,_,reldef(_,_,_,_,_))).

kodkod_jar(KodkodJar) :-
    absolute_file_name(prob_lib('probkodkod.jar'), KodkodJar),
    ( file_exists(KodkodJar,read) -> true
    ;
    add_error_and_fail(kodkod_process,'Unable to read Kodkod library. Please check your installation or disable the use of Kodkod')).

kodkod_request_intern(ProblemId, Signum, MaxNrOfSols, LocalState, State) :-
    known_problem(ProblemId,_Size,_Relations,_Formula,ToKodkod,ToProB,_OrigPredicate),
    extract_known_values(ToKodkod,LocalState,State,Known,UnknownList),
    copy_term(UnknownList,UnknownListCopy),
    list_to_avl(UnknownListCopy,Unknown),
    !,
    debug_println(19,send_kodkod_request(ProblemId,Signum,MaxNrOfSols,Known)),
    send_request(ProblemId, ToProB, Signum, MaxNrOfSols, Known, Unknown),
    %describe_sol(UnknownListCopy),
    UnknownList=UnknownListCopy.

map_kodkod_prob(set(Type),Tuples,Map,Value) :-
    !,map_kodkod_prob2(Tuples,Type,Map,Value).

map_kodkod_prob(Type,KValue,Map,BValue) :-
    map_kodkod_prob2([KValue],Type,Map,[BValue]).

map_kodkod_prob2([],_,_,[]).

map_kodkod_prob2([Values|TRest],Type,Map,[BValue|BRest]) :-
    map_kodkod_prob3(Type,Map,BValue,Values,[]),
    map_kodkod_prob2(TRest,Type,Map,BRest).

map_kodkod_prob3(couple(TA,TB),Map,(BA,BB)) -->
    map_kodkod_prob3(TA,Map,BA),
    map_kodkod_prob3(TB,Map,BB).

map_kodkod_prob3(integer,_,int(Value)) --> !,[Value].

map_kodkod_prob3(Type,Map,BValue) -->
    [K],{avl_fetch(Type:K,Map,BValue),!}.

map_prob_value_to_kodkod(set(_),Prob,ValueMap,Kodkod) :-
    !, expand_custom_set_to_list(Prob,List),
    map_prob_values_to_kodkod(List,ValueMap,Kodkod).

map_prob_value_to_kodkod(_Type,Prob,ValueMap,Kodkod) :-
    map_prob_values_to_kodkod([Prob],ValueMap,Kodkod).

map_prob_value_to_kodkod2((A,B),ValueMap) -->
    !,map_prob_value_to_kodkod2(A,ValueMap),
    map_prob_value_to_kodkod2(B,ValueMap).

map_prob_value_to_kodkod2(int(I),_ValueMap) --> !,[I].

map_prob_value_to_kodkod2(Prob,ValueMap) --> [Kodkod],
    {avl_fetch(Prob,ValueMap,Kodkod)}.

map_prob_values_to_kodkod([],_,[]).

map_prob_values_to_kodkod([P|Prest],ValueMap,[tuple(K)|Krest]) :-
    map_prob_value_to_kodkod2(P,ValueMap,K,[]),
    map_prob_values_to_kodkod(Prest,ValueMap,Krest).

next_problem_id(0).

prepare_id_mapping(Ids,Idmap,ProbToKodkod,KodkodToProb) :-
    prepare_id_mapping2(Ids,Idmap,ProbToKodkod,KodkodToProbList),
    list_to_avl(KodkodToProbList, KodkodToProb).

prepare_id_mapping2([],_,[],[]).

prepare_id_mapping2([TId|Rest],Idmap,[PK|ProbToKodkod],[KP|KodkodToProb]) :-
    prepare_id_mapping3(TId,Idmap,PK,KP),
    prepare_id_mapping2(Rest,Idmap,ProbToKodkod,KodkodToProb).

prepare_id_mapping3(TId,Idmap,bid(BType,P)-K,K-bid(BType,P)) :-
    get_texpr_id(TId,P),
    get_texpr_type(TId,BType1),
    adapt_seq_type(BType1,BType),
    avl_fetch(P,Idmap,reldef(K,_Types,_SetOrSingle,_ExactOrSubset,_Set)).

prepare_value_mapping(Valuemap,ProbToKodkod,KodkodToProb) :-
    avl_to_list(Valuemap,ProbKodkodList),
    maplist(reverse_key_value, ProbKodkodList, KodkodProbList),
    list_to_avl(KodkodProbList,KodkodToProb),
    maplist(remove_type_info,ProbKodkodList, L1),
    list_to_avl(L1,ProbToKodkod).

process_answer(solutions(Sols,More,Times),ProblemId,MaxNrOfSols,ToProb,In) :-
    formatsilent('Times for computing solutions: ~w~n',[Times]),
    save_java_comp_time(Times),
    get_solutions(Sols,More,ProblemId,MaxNrOfSols,ToProb,In).

process_answer(sat_timeout,ProblemId,_,_ToProb,_In) :-
    add_warning(kodkod_process,'Kodkod SAT Solver Timeout for Problem Id: ',ProblemId),
    %throw(time_out). % can only be caught by time_out not by catch !
    throw(enumeration_warning(kodkod_timeout,ProblemId,'','',critical)).

process_answer(sat_non_incremental,ProblemId,_,_ToProb,_In) :-
    add_warning(kodkod_process,'Kodkod SAT Solver is non incremental and cannot compute all solutions for Problem Id: ',ProblemId),
    throw(enumeration_warning(kodkod_timeout,ProblemId,'','',critical)).

process_answer(unknown(_),ProblemId,_,_ToProb,_In) :-
    add_warning(kodkod_process,'Kodkod SAT Solver error occured for Problem Id: ',ProblemId),
    throw(enumeration_warning(kodkod_error,ProblemId,'','',critical)).

process_answer(end_of_file,ProblemId,_,_ToProb,_In) :-
    add_warning(kodkod_process,'Kodkod SAT Solver aborted for Problem Id: ',ProblemId),
    throw(enumeration_warning(kodkod_error,ProblemId,'','',critical)).

read_answer_from_kodkod(IStream,Answer) :-
    read(IStream,Answer1),
    (Answer1=stats(T,S,C,V,P) % special statistics info fact
    -> debug_format(20,'Kodkod Statistics: ~w ms translation, ~w ms solving, ~w clauses, ~w variables, ~w primary variables~n',[T,S,C,V,P]),
    read_answer_from_kodkod(IStream,Answer)
    ; Answer=Answer1).

read_rest(ProblemId,MaxNrOfSols,ToProb,In) :-
    get_kodkod_process(_,OStream,IStream),
    kkp_list(ProblemId,MaxNrOfSols,OStream),
    get_solutions_from_stream(OStream,IStream,ProblemId,MaxNrOfSols,ToProb,In).

register_problem(Ids,KExpr,Idmap,Typemap,Valuemap,Predicate,ProblemId) :-
    startup_kodkod,
    get_new_problem_id(ProblemId),
    extract_all_types(Typemap,Types),
    extract_all_relations(Idmap,Relations),
    prepare_value_mapping(Valuemap,ProbToKodkodVal,KodkodToProbVal),
    prepare_id_mapping(Ids,Idmap,ProbToKodkodId,KodkodToProbId),
    assertz( known_problem(ProblemId,Types,Relations,KExpr,
    probkodkod(ProbToKodkodVal,ProbToKodkodId),
    kodkodprob(KodkodToProbVal,KodkodToProbId),
    Predicate) ),
    catch( send_problem(ProblemId),
    error(_,Err), % usually error(system_error,system_error('SPIO_E_NET_CONNRESET'))
    (format('Restarting Kodkod process due to: ~w~n',[Err]),
    reset_kodkod_process,
    startup_kodkod,
    send_problem(ProblemId))).

remove_type_info((_T:P)-K, P-K).

reset_kodkod_process :- retractall(kodkod_process(_,_,_)).

reverse_key_value((T:P)-K, (T:K)-P).

save_java_comp_time(Times) :-
    assertz(java_comp_time(Times)).

send_problem(Id) :-
    get_kodkod_process(_,KOut,_),
    known_problem(Id,Types,Relations,Formula,_ToKodkod,_ToProB,_OrigPredicate),
    get_preference(time_out,TO),
    get_preference(kodkod_symmetry_level,Symmetry),
    get_preference(kodkod_sat_solver,Solver),
    kodkod_printer:kkp_problem(KOut,TO,Symmetry,Solver,Id,problem(Types,Relations,Formula,xxx,none)).

send_request(ProblemId, ToProb, Signum, MaxNrOfSols,OutValues, In) :-
    get_kodkod_process(_,OStream,IStream),
    debug:debug_println(19,sending_kodkod_request(ProblemId,Signum,MaxNrOfSols)),
    kkp_request(ProblemId, Signum, MaxNrOfSols, OutValues, OStream),
    get_solutions_from_stream(OStream,IStream,ProblemId,MaxNrOfSols,ToProb,In).

startup_kodkod :- kodkod_process(_,_,_), !.

startup_kodkod :-
    absolute_file_name(prob_lib('.'), KodkodDir),
    kodkod_jar(KodkodJar),
   
    atom_concat('-Djava.library.path=', KodkodDir, JLibpath),
   
    get_command_path('java',CmdPath),
   
    %format('Starting Kodkod JAR ~w using ~w~n',[KodkodJar,JLibpath]),
    get_preference(kodkod_sat_solver,Solver),
   
    process_create(CmdPath,
    [JLibpath, '-Xmx1024M','-jar', KodkodJar,Solver],
    [process(KProc),stdout(pipe(KIn)),stdin(pipe(KOut))]),
    check_correct_startup(KIn),
   
    assertz(kodkod_process(KProc,KOut,KIn)).

stop_kodkod :-
    get_kodkod_process(PId,KOut,KIn),
    call_cleanup( (write(KOut, 'stop.\n'), flush_output(KOut) ),
    ( process_wait(PId,_), close(KOut), close(KIn),
    retractall(kodkod_process(_,_,_)))).