kodkod

apply_transformation(AllConstants,PredicateList,Result) :-
    conjunct_predicates(PredicateList,Predicate1),
    (debug_mode(on) -> print('TRANSLATING FOR KODKOD: '),nl,translate:print_bexpr_with_limit(Predicate1,1500),nl ; true),
    apply_transformation2(AllConstants,Predicate1,Result).

apply_transformation2(AllConstants,Predicate1,Result) :-
    split_simple_equalities(Predicate1,Equalities,Predicate),
    (debug_mode(on) -> print('Equalities: '), translate:print_bexpr_with_limit(Equalities,1500),nl ; true),
    (is_truth(Predicate)
    -> debug_println(19,'Predicate for Kodkod has only equalities. Predicate will be solved by ProB.'),
    Result=Predicate1
    % we could also fail, but then we would create a kodkod_fail warning
    ; apply_transformation3(AllConstants,Predicate,Equalities,Result)
    -> (debug_mode(on) -> print('RESULT: '),nl,translate:print_bexpr_with_limit(Result,1500),nl ; true)
    ; add_warning(kodkod,'Kodkod Transformation Failed for Predicate over: ',AllConstants),
    %trace, apply_transformation3(AllConstants,Predicate,Equalities,Result),
    fail).

apply_transformation3(AllConstants,Predicate,Equalities,Result) :-
    restrict_to_used_constants(AllConstants,Predicate,Constants),
    apply_rewriting_rules(Predicate,Rewritten),
    extract_used_types(Rewritten,Types,Ints,Bits),
    create_atoms_for_types(Types,Ints,Bits,Typemap,Idmap1,Valuemap),
    % check if any types are used, if not Kodkod would exit with an
    % empty universe exception
    % (java.lang.IllegalArgumentException: Cannot create an empty universe. or something similar)
    \+ empty_avl(Typemap),
    typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,Idmap,Rewritten,KExpr),
   
    register_problem(Constants,KExpr,Idmap,Typemap,Valuemap,Predicate,ProblemNr),
    create_texpr(kodkod(ProblemNr,Constants),pred,[],KPred),
    conjunct_predicates([Equalities,KPred],Result).

constant_is_used(UsedIds,C) :-
    get_texpr_id(C,Id),memberchk(Id,UsedIds).

contains_kodkod_call(TExpr) :-
    get_texpr_expr(TExpr,Expr),
    contains_kodkod_call2(Expr),!.

contains_kodkod_call2(kodkod(_,_)).

contains_kodkod_call2(conjunct(A,_)) :- contains_kodkod_call(A).

contains_kodkod_call2(conjunct(_,B)) :- contains_kodkod_call(B).

current_solver_is_not_incremental :-
    get_preference(kodkod_sat_solver,Solver),
    not_incremental(Solver).

filter_translatable([],[],[]).

filter_translatable([Res|Rrest],ToKodkod,StayProb) :-
    ( Res = ok(_,P,_,_) -> ToKodkod=[P|Krest], StayProb=Prest
    ; Res = failure(_,P,_,_) -> ToKodkod=Krest, StayProb=[P|Prest]),
    filter_translatable(Rrest,Krest,Prest).

finalize_result(log(Predicate,Result,Index,Ints,Bits)) :-
    var(Result),!,Result=ok(Index,Predicate,Ints,Bits).

finalize_result(_).

get_max_nr_of_solutions(MaxNrOfSols) :-
    current_solver_is_not_incremental,!,
    MaxNrOfSols = 1.

get_max_nr_of_solutions(MaxNrOfSols) :-
    get_preference(kodkod_max_nr_solutions,MaxNrOfSols). % TO DO: we could look at kodkod_for_components and maxNrOfInitialisations preference

is_base_expression(TExpr) :-
    get_texpr_expr(TExpr,Expr),
    is_base_expression2(Expr).

is_base_expression2(identifier(Id)) :- b_global_set(Id),!. % a deferred set

is_base_expression2(identifier(Id)) :- lookup_global_constant(Id,_). % an enumerated set element

is_base_expression2(integer(_)).

is_base_expression2(couple(A,B)) :- is_base_expression(A),is_base_expression(B).

is_base_expression2(set_extension(L)) :- maplist(is_base_expression,L).

is_base_expression2(value(_)).

is_base_expression2(boolean_true).

is_base_expression2(boolean_false).

is_base_expression2(empty_set).

is_base_expression2(bool_set).

is_base_expression2(add(A,B)) :- is_base_expression(A),is_base_expression(B).

is_base_expression2(minus(A,B)) :- is_base_expression(A),is_base_expression(B).

is_base_expression2(unary_minus(A)) :- is_base_expression(A).

is_base_expression2(multiplication(A,B)) :- is_base_expression(A),is_base_expression(B).

is_base_expression2(div(A,B)) :- is_base_expression(A),is_base_expression(B).

is_base_expression2(floored_div(A,B)) :- is_base_expression(A),is_base_expression(B).

is_base_expression2(modulo(A,B)) :- is_base_expression(A),is_base_expression(B).

is_base_expression2(power_of(A,B)) :- is_base_expression(A),is_base_expression(B).

is_simple_equality(TExpr) :-
    get_texpr_expr(TExpr,equal(A,B)),
    ( get_texpr_id(A,_),is_base_expression(B)
    ; get_texpr_id(B,_),is_base_expression(A)),!.

kodkod_request(Id,Signum,LocalState,State,LWF) :-
    % MaxNrOfSols is the maximum number of solutions found in one go by Kodkod
    get_max_nr_of_solutions(MaxNrOfSols),
    kodkod_request(Id,Signum,MaxNrOfSols,LocalState,State,LWF).

kodkod_request(Id,Signum,MaxNrOfSols,LocalState,State,_LWF) :-
    catch(
    kodkod_request_intern(Id,Signum,MaxNrOfSols,LocalState,State),
    error(system_error,system_error(E)), % often SPIO_E_NET_CONNRESET
    (add_internal_error('System Error while processing Kodkod request: ',E), fail)).

kodkod_reset :-
    ( stop_kodkod -> true; true).

not_incremental(lingeling).

pdebug :-
    install_b_portray_hook,
    assertz(( user:portray(X) :- is_avl(X),!,portray_avl(X) )).

print_result(ok(_Ids,Index,P,Ints,Bits)) :-
    print_result(ok(Index,P,Ints,Bits)).

print_result(ok(_Index,P,Ints,Bits)) :-
    (silent_mode(on) -> true
    ; write('kodkod ok: '),print_bexpr_with_limit(P,50),
    write(' ints: '),write(Ints),write(', intatoms: '),write(Bits)
).

print_result(failure(_Ids,Index,P,Msg,Reason)) :-
    print_result(failure(Index,P,Msg,Reason)).

print_result(failure(_Index,P,Msg,Reason)) :-
    write('kodkod fail: '),
    translate_bexpression_with_limit(P,50,PS), write(PS),
    write(' , reason: '),write_reason(Reason),write(' while '),write(Msg),nl,
    (get_preference(kodkod_raise_warnings,false) -> true
    ; add_warning(kodkod,'Cannot translate predicate for Kodkod: ',PS,P)
).

print_results([]).

print_results([R|Rrest]) :-
    print_result(R),nls,
    print_results(Rrest).

replace_by_kodkod(Constants,Predicate,NewPredicate) :-
    % Remove any CSE lazy_lets as Kodkod translation cannot deal with them yet
    (get_preference(use_common_subexpression_elimination,true) ->
    expand_cse_lazy_lets(Predicate,Predicate0)
    ; Predicate0=Predicate),
    % The Predicate may already contain Kodkod calls, replace
    % them by their original B predicate
    undo_kodkod_replacements(Predicate0,Predicate1),
    % first we do a predicate analysis to determine ranges for integers
    try_predicate_analysis_with_global_sets(Predicate1,Constants,TaggedConstants,TaggedPredicate),
    replace_by_kodkod2(TaggedConstants,TaggedPredicate,NewPredicate).

replace_by_kodkod2(Constants,_Predicate,NewPredicate) :-
    % If the static analysis states that there is no possible solution for one
    % of the identifiers, we just say "false"
    somechk(is_inconsistent_expression,Constants),!,
    write('kodkod: Static analysis detected inconsistencies, new predicate is "false"'),nl,
    create_texpr(falsity,pred,[],NewPredicate).

replace_by_kodkod2(Constants,Predicate,NewPredicate) :-
    temporary_set_preference(partition_predicates_inline_equalities,false,CHNG),
    split_predicates(Predicate,PList), % will split into components if KODKOD_ONLY_FULL = FALSE
    reset_temporary_preference(partition_predicates_inline_equalities,CHNG),
    % we try to translate each predicate alone
    try_apply_transformation_l(PList,Constants,1,Result),
    print_results(Result),
    % split the result into two lists: the successfull translatable predicates (ToKodkod)
    % and those which were not translatable (StayProb)
    filter_translatable(Result,ToKodkod,StayProb),
    %%print('Stay ProB: '), conjunct_predicates(StayProb,StayPred), translate:print_bexpr(StayPred),nl,
    % fail if there are no translatable predicates
    ToKodkod = [_|_],
    % now, translate all translatable predicates in one run
    (StayProb = [_|_] -> add_message(kodkod,'Not translating all components/predicates with Kodkod') ; true ),
    % with a special preference to force full evaluation we could also abort here and return UNKNOWN
    apply_transformation(Constants,ToKodkod,KPred),
    % the new
    %%print('For Kodkod: '), translate:print_bexpr(KPred),nl,
    conjunct_predicates([KPred|StayProb],NewPredicate).

restrict_to_used_constants(Constants,Predicate,UsedConstants) :-
    find_identifier_uses(Predicate,['$examine_value_was_identifier_info'],UsedIds), % flag says: also get value(_) with was_identifier(_) field
    include(constant_is_used(UsedIds),Constants,UsedConstants).

split_predicates(Predicate,Parts) :-
    get_preference(kodkod_for_components,false),!,
    conjunction_to_list(Predicate,Parts).

split_predicates(Predicate,Parts) :-
    % only translate full components (or component not at all)
    predicate_components(Predicate,Components),
    findall(P,member(component(P,_),Components),Parts).

split_simple_equalities(InPredicate,Equalities,Rest) :-
    conjunction_to_list(InPredicate,InPredicates),
    split_list(is_simple_equality,InPredicates,EqualitiesL,RestL),
    conjunct_predicates(EqualitiesL,Equalities),
    conjunct_predicates(RestL,Rest).

try_apply_transformation(Predicate,Constants,Index,Result) :-
    %%print('TRY KODKOD ON: '), translate:print_bexpr(Predicate),nl,
    Log = log(Predicate,Result,Index,Ints,Bits),
    try_call( 'applying rewriting rules', Log,
    apply_rewriting_rules(Predicate,Rewritten)),
    %%print('REWRITTEN: '), translate:print_bexpr(Rewritten),nl,
    try_call( 'extracting used types', Log,
    extract_used_types(Rewritten,Types,Ints,Bits)),
    try_call( 'creating Kodkod atoms for types', Log,
    create_atoms_for_types(Types,Ints,Bits,Typemap,Idmap1,_Valuemap)),
    try_call( 'translate and type Kodkod formula', Log,
    typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,_Idmap,Rewritten,_KExpr)),
    finalize_result(Log).

try_apply_transformation_l([],_Constants,_,[]).

try_apply_transformation_l([Predicate|Prest],Constants,I,[Result|Rrest]) :-
    try_apply_transformation(Predicate,Constants,I,Result),
    I2 is I+1,
    try_apply_transformation_l(Prest,Constants,I2,Rrest).

try_call(_Msg,log(_Predicate,Result,_Index,_,_),_Call) :-
    nonvar(Result),!.

try_call(Msg,log(Predicate,Result,Index,_,_),Call) :-
    %%format('Try ~w ~n',[Msg]),
    ( catch(Call,
    kodkod(T),
    ( %%format('Exception: ~w~n',[T]),
    Result = failure(Index,Predicate,Msg,kodkod_exception(T)))
    ) -> true
    ;
    %%format('Failure for: ~w~n',[Msg]),
    Result = failure(Index,Predicate,Msg,failed)
).

try_predicate_analysis_with_global_sets(Predicate,Constants,TaggedConstants,TaggedPredicate) :-
    catch(predicate_analysis_with_global_sets(Predicate,[],Constants,TaggedConstants,TaggedPredicate),
    failed_analysis(Expr),
    ( write('kodkod fail: predicate analysis failed on expression '),
    translate_bexpression_with_limit(Expr,80,Msg),
    write(Msg),nl,fail)),
    !.

try_predicate_analysis_with_global_sets(_Predicate,_Constants,_TaggedConstants,_TaggedPredicate) :-
    write('kodkod fail: predicate analysis failed.\n'),
    fail.

typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,Idmap,Rewritten,KExpr) :-
    % Create the relations for the constants that are actually used
    restrict_to_used_constants(Constants,Predicate,UsedConstants),
    create_identifier_relations(UsedConstants,Typemap,Bits,Idmap1,Idmap),
    % translate the formula in two steps:
    kodkod_translate(Rewritten,Typemap,Idmap,Formula),
    kodkod_insert_casts(Formula,Typemap,Idmap,KExpr),
    !.

undo_kodkod_replacements(Old,New) :-
    contains_kodkod_call(Old),!,
    undo_kodkod_replacements2(Old,New).

undo_kodkod_replacements(Old,Old).

undo_kodkod_replacements2(TOld,TNew) :-
    get_texpr_expr(TOld,Old),
    undo_kodkod_replacements3(Old,TOld,TNew).

undo_kodkod_replacements3(conjunct(A,B),_TOld,TNew) :-
    !,create_texpr(conjunct(NewA,NewB),pred,[],TNew),
    undo_kodkod_replacements2(A,NewA),
    undo_kodkod_replacements2(B,NewB).

undo_kodkod_replacements3(kodkod(Id,_),_TOld,Orig) :-
    !,get_original_problem(Id,Orig).

undo_kodkod_replacements3(_Old,TOld,TOld).

write_reason(kodkod_exception(KE)) :-
    write_reason2(KE),!.

write_reason(E) :- write(E).

write_reason2(unsupported_type(T)) :-
    pretty_type(T,PT),
    write('unsupported type '),write(PT).

write_reason2(unsupported_expression(TE)) :-
    get_texpr_expr(TE,T),
    functor(T,Functor,Arity),
    translate_bexpression(TE,PE),
    format('unsupported expression ~w/~w: ~w',[Functor,Arity,PE]).

write_reason2(unsupported_int(Msg)) :-
    write(Msg).

write_reason2(side_condition(Msg,PPExpr,Info)) :-
    (extract_span_description(Info,Desc)
    -> format('~w: ~w (~w)',[Msg,PPExpr, Desc])
    ; format('~w: ~w',[Msg,PPExpr])).