kodkod.pl

analysis_for_counterexample(Variables,Assumption,Assertion,
    TaggedVariables,TaggedAssumption,TaggedAssertion) :-
    create_texpr(negation(Assertion),pred,[],NAssertion),
    create_texpr(conjunct(Assumption,NAssertion),pred,[],Conj),
    try_predicate_analysis_with_global_sets(Conj,Variables,TaggedVariables,TaggedConj),
    create_texpr(conjunct(TaggedAssumption,TaggedNAssertion),pred,_,TaggedConj),
    create_texpr(negation(TaggedAssertion),pred,_,TaggedNAssertion).

apply_kodkod_to_counterexample_search(Variables,Assumption,Assertion,KPred,Rest) :-
    get_preference(try_kodkod_on_load,true),
    % The predicates may already contain Kodkod calls, replace
    % them by their original B predicate
    undo_kodkod_replacements(Assumption,Assumption1),
    undo_kodkod_replacements(Assertion,Assertion1),
    % first we do a predicate analysis to determine ranges for integers
    analysis_for_counterexample(Variables,Assumption1,Assertion1,
    TaggedVariables,TaggedAssumption,TaggedAssertions),
   
    % analyse assumptions
    split_assumptions(TaggedAssumption,TaggedVariables,
    TAssumptions,NTAssumptions,AssumptionsComponents),
   
    % analyse assertions
    translate_assertions(TaggedAssertions,TaggedVariables,TAssumptions,NTAssumptions,
    UsedAssumptionNumbers,TAssertions,NTAssertions,UsedVariables),
   
    % if we do not find a translatalbe assertion, fail and do not apply Kodkod at all
    TAssertions = [_|_],
   
    findall( UP,
    (member(N,UsedAssumptionNumbers),nth1(N,AssumptionsComponents,component(UP,_))),
    UsedAssumptions),
    findall( UP,
    (nth1(N,AssumptionsComponents,component(UP,_)),nonmember(N,UsedAssumptionNumbers)),
    UnusedAssumptions),
   
    conjunct_predicates(TAssertions,TAssertion),
    create_texpr(negation(TAssertion),pred,[],Negation),
    append(UsedAssumptions,[Negation],ToTranslate),
    apply_transformation(UsedVariables,ToTranslate,KPred),
   
    ( NTAssertions = [] ->
    conjunct_predicates(UnusedAssumptions,Rest)
    ;
    conjunct_predicates(NTAssertions,RestAssertion),
    create_texpr(negate(RestAssertion),pred,[],RestNegated),
    conjunct_predicates([Assumption,RestNegated],Rest)).

find_predicate(_TAssumptions,NTAssumptions,Id,_UsedAssumption) :-
    % if the assertion uses an ID that is also used by a non-translatable
    % assumption, we do not translate the assumption
    avl_fetch(Id,NTAssumptions),!,fail.

find_predicate(TAssumptions,_NTAssumptions,Id,UsedAssumptions) :-
    ( avl_fetch(Id,TAssumptions,UsedAssumption) ->
    UsedAssumptions = [UsedAssumption]
    ;
    UsedAssumptions = []).

find_used_predicates(Ids,TAssumptions,NTAssumptions,UsedAssumptions) :-
    maplist(find_predicate(TAssumptions,NTAssumptions),Ids,AssumptionsL),
    append(AssumptionsL,Assumptions),
    sort(Assumptions,UsedAssumptions).

map_ids_to_assumption(AssumptionResults,AssumptionIds,NotTranslated) :-
    findall( Id-N,
    ( nth1(N,AssumptionResults,ok(Ids,_,_,_)),
    member(Id,Ids)),
    Ids1),
    list_to_avl(Ids1,AssumptionIds),
    findall( N,
    ( nth1(N,AssumptionResults,failure(Ids,_,_,_,_)),
    member(Id,Ids)),
    Ids2),
    list_to_avl(Ids2,NotTranslated).

split_assumptions(Assumption,Variables,Translatable,NotTranslated,AssumptionsComponents) :-
    predicate_components(Assumption,AssumptionsComponents),
    try_apply_transformation_to_components(AssumptionsComponents,Variables,1,AssumptionResults),
    map_ids_to_assumption(AssumptionResults,Translatable,NotTranslated).

translate_assertion(Assertion,Variables,TAssumptions,NTAssumptions,UsedAssumptions,Ids) :-
    find_identifier_uses(Assertion,[],Ids),
    find_used_predicates(Ids,TAssumptions,NTAssumptions,UsedAssumptions),
    try_apply_transformation(Assertion,Variables,1,R),
    functor(R,ok,_).

translate_assertions(Assertion,Variables,TAssumptions,NTAssumptions,UsedAssumptions,
    Translatable,NotTranslated,UsedVariables) :-
    conjunction_to_list(Assertion,Assertions),
    translate_assertions2(Assertions,Variables,TAssumptions,NTAssumptions,Unsorted,
    Translatable,NotTranslated,UIds),
    sort(Unsorted,UsedAssumptions),
    sort(UIds,Ids),
    findall(V,(member(V,Variables),get_texpr_id(V,I),memberchk(I,Ids)),UsedVariables).

translate_assertions2([],_Variables,_TAssumptions,_NTAssumptions,[],[],[],[]).

translate_assertions2([Assertion|Arest],Variables,TAssumptions,NTAssumptions,
    UsedAssumptions,Translatable,NotTranslated,Ids) :-
    ( translate_assertion(Assertion,Variables,TAssumptions,NTAssumptions,LUsedAssumptions,LUsedIds) ->
    append(LUsedAssumptions,Urest,UsedAssumptions),
    append(LUsedIds,Irest,Ids),
    Translatable = [Assertion|Trest], NotTranslated = NTrest
    ;
    UsedAssumptions = Urest,
    Ids = Irest,
    Translatable = Trest, NotTranslated = [Assertion|NTrest]),
    translate_assertions2(Arest,Variables,TAssumptions,NTAssumptions,Urest,Trest,NTrest,Irest).

try_apply_transformation_to_components([],_Vars,_,[]).

try_apply_transformation_to_components([component(Predicate,Ids)|Crest],Vars,I,[Result|Rrest]) :-
    try_apply_transformation(Predicate,Vars,I,Result1),
    Result1 =.. [Functor|Args],
    Result =.. [Functor,Ids|Args],
    I2 is I+1,
    try_apply_transformation_to_components(Crest,Vars,I2,Rrest).