symmetry_marker

add_avl_count(AVL,Key,NewAVL) :- %print(add_count(Key)),nl,
    (avl_fetch(Key,AVL,OldCount)
    -> NewCount is OldCount+1,
    avl_change(Key,AVL,_,NewAVL,NewCount)
    ; avl_store(Key,AVL,1,NewAVL)
). %, print(ok(NewCount)),nl.

analyse_typed_varlist([]).

analyse_typed_varlist([b(identifier(ID),Type,_)|T]) :-
    (non_symmetric_type(Type)
    -> assertz(non_symmetric_var(ID,Type))
    %% ,print(non_sym(ID,Type)),nl
    ; true),
    analyse_typed_varlist(T).

assert_markers([],_).

assert_markers([marker(Type,Paths,Nr)|T],ID) :-
    get_same_markers(T,Type,Paths,Same,TT,NrSame), % get all other elements with same Paths information
    ID1 is ID+1,
    (NrSame=0 -> assertz(deferred_set_el_marker(Type,Nr,fdunique(ID1,Type)))
    ; assert_same_markers([Nr|Same],Type,ID1,NrSame)),
    assert_markers(TT,ID1).

assert_same_markers([],_,_,_).

assert_same_markers([Nr|T],Type,ID,NrSame) :-
    assertz(deferred_set_el_marker(Type,Nr,fdsame(ID,Type,NrSame))),
    assert_same_markers(T,Type,ID,NrSame).

avl_could_contain_deferred_set_element(node(X,_,_,_L,_R)) :- /* first underscore should be true */
    could_contain_deferred_set_elements(X).

avl_marker(Avl, Type,Local) :- avl_domain(Avl,List),
    l_marker(List,Type,Local).

compute_deferred_set_el_markers(CountAVL) :-
    avl_to_list(CountAVL,AList),
    %print(AList),nl,
    merge_paths(AList,BList),
    sort(BList,SBList),
    %print(merged(SBList)),nl,
    retractall(deferred_set_el_marker(_,_,_)),
    assert_markers(SBList,0),!.

compute_marker_for_state(State,Marker) :-
    (State = concrete_constants(BState)
    -> Marker = concrete_constants(BMarker)
    ; (State = csp_and_b(CSPState,BState)
    -> Marker = csp_and_b(CSPState,BMarker)
    ; (State=[] ; State = [_|_] ; State = const_and_vars(_,_) ),
    State=BState, Marker=BMarker
    )
    ),
    expand_const_and_vars_to_full_store(BState,FullBState),
    count_state(FullBState), /* first count the number of occurrences
    of every symmetric element in the State; this number will
    be used as the marker for that element */
    marker_for_state(FullBState,BMarker).

could_contain_deferred_set_elements([]).

could_contain_deferred_set_elements([H|_]) :- could_contain_deferred_set_elements(H).

could_contain_deferred_set_elements(fd(_Nr,_T)).

could_contain_deferred_set_elements((A,B)) :-
    (could_contain_deferred_set_elements(A) -> true ; could_contain_deferred_set_elements(B)).

could_contain_deferred_set_elements(avl_set(A)) :- avl_could_contain_deferred_set_element(A).

could_contain_deferred_set_elements(rec(Fields)) :-
    member(field(_,A),Fields), could_contain_deferred_set_elements(A),!.

count_avl(empty,_PathToObject) --> [].

count_avl(node(Key,_True,_,L,R),PathToObject) -->
    count_avl(L,PathToObject), count_obj(Key,PathToObject),
    count_avl(R,PathToObject).

count_env([],I,O) :- !, O=I.

count_env([bind(Var,Val)|T],In,Out) :- !,
    (non_symmetric_var(Var,_) -> In=I1
    ; %print(counting(Var)),nl,
    count_obj(Val,Var,In,I1)),
    count_env(T,I1,Out).

count_env(E,I,O) :- add_error(symmetry_marker,'Illegal env: ',E), O=I.

count_obj(fd(Nr,T),PathToObject,In,Out) :- !, %print(fd(Nr,T)),
    ((b_global_deferred_set_with_card_gt1(T) ;
    is_unused_b_global_constant(T,Nr) /* TO DO: only makes sense if more than one unused global constant */
    )
    -> %add_count(PathToObject,Nr,T,In,Out)
    add_avl_count(In,usage_count(Nr,T,PathToObject),Out)
    ; Out=In
).

count_obj((X,Y),PathToObject,In,Out) :- !, count_pair(X,Y,PathToObject,In,Out).

count_obj([X|Y],PathToObject,In,Out) :- !,
    (could_contain_deferred_set_elements(X)
    -> count_obj_list([X|Y],PathToObject,In,Out) /* only count set if there are deferred set elements inside */
    ; Out=In
).

count_obj(avl_set(A),PathToObject,In,Out) :- !,
    (avl_could_contain_deferred_set_element(A)
    -> count_avl(A,el(PathToObject),In,Out)
    ; Out=In
).

count_obj(rec(Fields),PathToObject,In,Out) :- !,
    count_obj_field_list(Fields,PathToObject,In,Out).

count_obj(freeval(ID,Case,Val),freeval(ID,Case,PathToObject),In,Out) :- !,
    count_obj(Val,PathToObject,In,Out).

count_obj(_,_,O,O).

count_obj_field_list([],_,O,O).

count_obj_field_list([field(FX,VX)|T],PathToObject,In,Out) :-
    count_obj(VX,field(FX,PathToObject),In,I1),
    count_obj_field_list(T,PathToObject,I1,Out).

count_obj_list([],_,O,O).

count_obj_list([X|Y],PathToObject,In,Out) :-
    count_obj(X,el(PathToObject),In,I1),
    count_obj(Y,PathToObject,I1,Out).

count_pair(X,Y,PathToObject,In,Out) :- not_symmetric(Y),!,
    count_obj(X,mapped_to(PathToObject,Y),In,Out).

count_pair(X,Y,PathToObject,In,Out) :- not_symmetric(X),!,
    count_obj(Y,mapped_from(X,PathToObject),In,Out).

count_pair(X,X,PathToObject,In,Out) :- !, /* is this correct ??
    should we only do it for simple X, what about sets: should
    work if normalised ?? */
    count_obj(X,leftright(PathToObject),In,Out).

count_pair(X,Y,PathToObject,In,Out) :- !,
    count_obj(X,left(PathToObject),In,I1),
    count_obj(Y,right(PathToObject),I1,Out).

count_state(State) :- empty_avl(E),
    %nl,translate:print_bstate(State),nl,
    count_env(State,E,Out),
    %portray_avl(Out),nl,
    compute_deferred_set_el_markers(Out).

fields_allows_for_precise_marker([]).

fields_allows_for_precise_marker([field(_Name,Type)|T]) :-
    type_allows_for_precise_marker(Type),
    fields_allows_for_precise_marker(T).

fields_marker([], _Type, []).

fields_marker([field(Name,H)|T], [field(Name,Type1)|TR], [LH|LT]) :- % field name not required in marker
    marker(H,Type1,LH),
    fields_marker(T,TR,LT).

get_same_markers([marker(Type,Paths,Nr)|T],Type,Paths,[Nr|SM],TT,ResNr) :- !,
    get_same_markers(T,Type,Paths,SM,TT,SNr), ResNr is SNr+1.

get_same_markers(T,_,_,[],T,0).

hash_model_checking_imprecise(ID,BasicType) :- %print(check),nl,
    get_preference(symmetry_mode,hash),
    (b_get_machine_constants(TL) ; b_get_machine_variables(TL)),
    member(b(identifier(ID),BasicType,_),TL),
    \+ type_allows_for_precise_marker(BasicType).

l_marker([], _Type, []).

l_marker([H|T], Type, [LH|LT]) :-
    marker(H,Type,LH),
    l_marker(T,Type,LT).

marker(closure(P,T,B),set(any),closure(P,T,B)).

marker(global_set(GS),set(Type),Local) :-
    marker_explicit_set(global_set(GS),set(Type),Local).

marker(avl_set(S),set(Type),SLocal) :- % marker_explicit_set(avl_set(S),set(Type),Val,Local).
    (avl_marker(S, Type,Local) -> true ; print(failed_avl_marker(S)),nl,fail),
    sort_markers(Local,SLocal).

marker(closure_x(P,T,B,E),set(Type),Local) :-
    marker_explicit_set(closure_x(P,T,B,E),set(Type),Local).

marker(int(N), integer, N). % int(N)

marker(string(S), string, S). % string(S)).

marker(term(F), real, R) :- is_real(term(F),R).

marker(fd(Nr,T), global(T), Term) :-
    (deferred_set_el_marker(T,Nr,Term)
    -> true
    ; (b_global_deferred_set_with_card_gt1(T)
    -> print(not_counted(Nr,T)),nl ; true),
    Term=fd(Nr,T) /*should not happen for deferred sets */
).

marker(pred_false /* bool_false */, boolean, pred_false).

marker(pred_true /* bool_true */, boolean, pred_true).

marker(freeval(ID,Case,V),_Type,freeval_marker(Case,VM)) :-
    freetype_case_db(Case,ID,CaseType),
    marker(V,CaseType,VM).

marker((X,Y), couple(T1,T2), Mark) :-
    (X==Y -> Mark = id_couple(L1), marker(X,T1,L1) % added 7/9/2011 by leuschel
    ; Mark = couple(L1,L2), marker(X,T1,L1),marker(Y,T2,L2)).

marker([], set(_), []).

marker([H|T], set(Type), Local) :-
    l_marker([H|T],Type,LL),
    sort_markers(LL,Local).

marker(rec(Fields), record(FTypes), Local) :-
    fields_marker(Fields,FTypes,Local).

marker_explicit_set(ES,set(Type),Local) :-
    expand_custom_set_to_list_now(ES,Res),
    l_marker(Res,Type,LL),
    sort_markers(LL,Local).

marker_for_state([],[]).

marker_for_state([bind(Var,Val)|T],[M|TM]) :-
    (non_symmetric_var(Var,_)
    -> TermMarker=Val
    ; marker(Val, _Type,TermMarker)),
    M=mark(Var,TermMarker),
    marker_for_state(T,TM).

merge_paths([],[]).

merge_paths([usage_count(Nr,Type,Path)-Count|Tail],Res) :-
    merge_paths(Tail,Nr,Type,[count(Path,Count)],Res).

merge_paths([],Nr,Type,MarkerPaths,[marker(Type,MarkerPaths,Nr)]). % :- print(marker(Type,MarkerPaths,Nr)),nl.

merge_paths([usage_count(Nr,Type,Path)-Count|Tail],Nr,Type,M,Res) :- !,
    merge_paths(Tail,Nr,Type,[count(Path,Count)|M],Res).

merge_paths([usage_count(Nr,Type,Path)-Count|Tail],Nr2,T2,M,[marker(T2,M,Nr2)|Res]) :-
    % print(marker(T2,Nr2,M)),nl,
    merge_paths(Tail,Nr,Type,[count(Path,Count)],Res).

non_symmetric_fields([]).

non_symmetric_fields([field(_Name,Type)|T]) :- non_symmetric_type(Type),
    non_symmetric_fields(T).

non_symmetric_type(integer) :- !.

non_symmetric_type(boolean) :- !.

non_symmetric_type(real) :- !.

non_symmetric_type(string) :- !.

non_symmetric_type(set(X)) :- !, non_symmetric_type(X).

non_symmetric_type(couple(X,Y)) :- !,non_symmetric_type(X), non_symmetric_type(Y).

non_symmetric_type(global(X)) :- !, \+ b_global_set_with_potential_symmetry(X).

non_symmetric_type(seq(X)) :- !, non_symmetric_type(X).

non_symmetric_type(record(F)) :- !, non_symmetric_fields(F).

non_symmetric_type(freetype(_)) :- !.

non_symmetric_type(any) :- !.

non_symmetric_type(constant(_)) :- !.

non_symmetric_type(X) :- add_error_fail(non_symmetric_type,'Unknown type: ',X).

not_symmetric([]).

not_symmetric((X,Y)) :- not_symmetric(X), not_symmetric(Y).

not_symmetric(pred_false /* bool_false */).

not_symmetric(pred_true /* bool_true */).

not_symmetric(string(_)).

not_symmetric(fd(Nr,T)) :-
    \+ b_global_deferred_set_with_card_gt1(T),
    \+ is_unused_b_global_constant(T,Nr). /* TO DO: only makes sense if more than one unused global constant */

not_symmetric(int(_)).

not_symmetric(term(_)).

not_symmetric(freeval(_,_,Val)) :- not_symmetric(Val).

not_symmetric(rec(Fields)) :- \+ (member(field(_,X),Fields), \+ not_symmetric(X)).

precompile_marker_typing_info :-
    retractall(non_symmetric_var(_,_)),
    bmachine:b_get_machine_variables(TypedVarList),
    bmachine:b_get_machine_constants(TypedCstList),
    append(TypedCstList,TypedVarList,List),
    analyse_typed_varlist(List).

print_fail(_T) :-
    %print('*** type may lead to imprecise hash marker:'),
    %translate:pretty_type(T,S),print(S),nl,
    fail.

sort_markers(X,SX) :- samsort(X,SX). % sort without duplicate removal

type_allows_for_precise_marker(integer).

type_allows_for_precise_marker(real).

type_allows_for_precise_marker(string).

type_allows_for_precise_marker(boolean).

type_allows_for_precise_marker(set(global(_))) :- !. % ok, whether global set deferred or not

type_allows_for_precise_marker(set(couple(X,Y))) :- !,
    (Y=global(_),non_symmetric_type(X) -> true
    % type_allows_for_precise_marker(Y) not ok; unless we are guaranteed to have a function
    ; X=global(_),non_symmetric_type(Y) -> true % see comment above
    ; non_symmetric_type(X), non_symmetric_type(Y) -> true
    ; print_fail(set(couple(X,Y)))).

type_allows_for_precise_marker(set(X)) :-
    (non_symmetric_type(X) -> true
    ; print_fail(set(X))).

type_allows_for_precise_marker(seq(X)) :- !, type_allows_for_precise_marker(set(couple(integer,X))).

type_allows_for_precise_marker(global(_)).

type_allows_for_precise_marker(couple(X,Y)) :- !,type_allows_for_precise_marker(X),
    type_allows_for_precise_marker(Y).

type_allows_for_precise_marker(record(F)) :- !, fields_allows_for_precise_marker(F).