clpfd_lists

assert_fdset_information(int_fdset(FDSet),X) :- !,
    (ground(X) -> true ; X=int(XX),in_set(XX,FDSet)).

assert_fdset_information(fd_fdset(FDSet,GS),X) :- !,
    (ground(X) -> true ; X=fd(XX,GS),in_set(XX,FDSet)).

assert_fdset_information(single_value(V),X) :- !, equal_object(V,X).

assert_fdset_information(_,_).

avl_fd_value_check(AVL,E,WF,FullyChecked) :-
    AVL = node(TopEl,_True,_,_,_),!,
    contains_fd_element(TopEl,Res,WF),
    (Res==pred_true
    -> avl_domain(AVL,DomainList),
    DomainList = [H|T],
    lazy_in_list_propagation_block_3(pred_true,H,T,E,WF,FullyChecked)
    ; FullyChecked=false).

avl_fd_value_check(AVL,E,WF,FullyChecked) :-
    add_internal_error('Illegal call: ',avl_fd_value_check(AVL,E,WF,FullyChecked)),
    FullyChecked=false.

bound_list(List,BoundList) :-
    (List = [] -> BoundList=pred_true
    ; List = [_|T] -> bound_list(T,BoundList)
    ; BoundList=pred_false). % we have avl_set or global_set or closure; TO DO: also allow avl_set

check_non_var_list(V) :- var(V),!,fail. %print(check_non_var_failed),nl,fail.

check_non_var_list([]).

check_non_var_list([H|T]) :- !, nonvar(H), check_non_var_list(T).

check_valid_fd_type(Type) :-
    (valid_type(Type) -> true
    ; add_internal_error('Illegal FD type:',check_valid_fd_type(Type)),fail).

combine_fdset_information(no_fdset_info,I,R) :- !, R=I.

combine_fdset_information(I,no_fdset_info,R) :- !, R=I.

combine_fdset_information(int_fdset(A),int_fdset(B),int_fdset(C)) :- !,
    %print(un(A,B,C)),nl,
    fdset_union(A,B,C).

combine_fdset_information(fd_fdset(A,GS),fd_fdset(B,GS),fd_fdset(C,GS)) :- !,
    fdset_union(A,B,C).

combine_fdset_information(single_value(V),single_value(W),R) :- !,
    (V==W -> R=single_value(V) ; R=no_fdset_info).

combine_fdset_information(A,B,C) :-
    add_internal_error('Illegal FD info: ',combine_fdset_information(A,B,C)),fail.

complete_type(global(_)).

complete_type(integer).

contains_fd_element(int(_),R,_WF) :- !, R=pred_true.

contains_fd_element(fd(_,_),R,_WF) :- !, R=pred_true.

contains_fd_element((A,B),R,WF) :- !,contains_fd_element(A,RA,WF), contains_fd_element(B,RB,WF),
    b_interpreter_check:disjoin(RA,RB,R,priority(16384),priority(16384),WF). % TO DO: examine priority to be used

contains_fd_element(rec(Fields),R,WF) :- !, contains_field_fd_el(Fields,R,WF).

contains_fd_element(freeval(_ID,_Case,_Val),R,_WF) :- !,
    % We assume that a freetype can contain FD elements; TO DO: really check !
    % ID is something of the form 'List'(integer) ; we use get_freeval_type(ID,_Case) from kernel_freetypes to get subtypes
    % we could look at the value; but we could be unlucky in that this particular Case has no fd subtype but others do
    % anyway: try_get_fd_value_type will fail if there is no fd type
    R=pred_true.

contains_fd_element(_,pred_false,_).

contains_field_fd_el([],R,_WF) :- !, R=pred_false.

contains_field_fd_el([field(_,V)|_],R,WF) :- contains_fd_element(V,R,WF). % TO DO: look at other fields

exact_member_nr(X,[Y|_],Acc,R) :- X==Y, !, Acc=R.

exact_member_nr(X,[_|T],Acc,R) :- A1 is Acc+1, exact_member_nr(X,T,A1,R).

finite_fd_set(V,FDSET) :- fd_set(V,FDSET), fdset_size(FDSET,N), number(N). %FDSET \= [[inf|sup]].

get_fd_value(T,V,E) :- var(V),var(T),!,
    add_internal_error('Variable arguments: ',get_fd_value(V,T,E)),fail.

get_fd_value(couple(TA,TB),(A,B),fd_pair(FDA,FDB)) :-
    get_fd_value(TA,A,FDA), get_fd_value(TB,B,FDB).

get_fd_value(couple_left(T),(A,_),FDA) :- get_fd_value(T,A,FDA).

get_fd_value(couple_right(T),(_,A),FDA) :- get_fd_value(T,A,FDA).

get_fd_value(rec_fields(T),rec(Fields),fd_rec(FD)) :- get_field_fd_values(T,Fields,FD).

get_fd_value(freeval_case(ID,Case,T),freeval(ID,Case,A),FDA) :-
    get_fd_value(T,A,FDA).

get_fd_value(global(GS),FD,X) :- get_global_type_value(FD,GS,X).

get_fd_value(integer,int(X),X).

get_fd_value_list(Set,Type,FDList,GroundList,El) :-
    get_fd_value_list5(Set,Type,FDList,true,GroundList,El,0).

get_fd_value_list5(V,_,_,_,_,_,_) :- var(V),!,fail.

get_fd_value_list5([],_,[],G,G,_,_).

get_fd_value_list5([H|T],Type,FDValList,GroundIn,GroundOut,El,NrMatch) :-
    (NrMatch<2 -> cannot_match_aggressive(H,El) % there is still hope of obtaining something deterministic; try more aggressive version; important for test 34; see also test 985 where too much propagation hurts
    ; cannot_match(H,El)),
    !, % we can filter this FD Value out
    get_fd_value_list5(T,Type,FDValList,GroundIn,GroundOut,El,NrMatch).

get_fd_value_list5([H|T],Type,FDValList,GroundIn,GroundOut,El,NrMatch) :-
    if(get_fd_value(Type,H,FDH),
    (FDValList = [FDH|FDT], N1 is NrMatch+1,
    (GroundIn=true,number(FDH) -> Ground1=true ; Ground1=false)),
    % Failure can happen when a variable gets instantiated (eg. X -> fd(_,t))
    % and triggers co-routines which fail (happens for SelfGrandpas.als for scope 3)
    % TO DO: review that this is the only possibility of failure
    (debug:debug_println(9,get_fd_value_failed(Type,H,_)),
    check_valid_fd_type(Type),fail)
    ),
    get_fd_value_list5(T,Type,FDT,Ground1,GroundOut,El,N1).

get_fdset_information(V,Info) :- var(V),!,Info=no_fdset_info.

get_fdset_information(int(V),int_fdset(FDSET)) :- fd_set(V,FDSET).

get_fdset_information(fd(V,GS),fd_fdset(FDSET,GS)) :- fd_set(V,FDSET).

get_fdset_information(pred_true,single_value(pred_true)).

get_fdset_information(pred_false,single_value(pred_false)).

get_fdset_information(string(S),single_value(string(S))) :- ground(S).

get_field_fd_values([],[],[]).

get_field_fd_values([field_no_fd(Name)|TTypes],[field(Name,_)|TF],FDVals) :-
    get_field_fd_values(TTypes,TF,FDVals).

get_field_fd_values([field(Name,T)|TTypes],[field(Name,Value)|TF],[FDVal|TFD]) :-
    get_fd_value(T,Value,FDVal),
    get_field_fd_values(TTypes,TF,TFD).

get_finite_fdset_information(V,_Info) :- var(V),!,fail.

get_finite_fdset_information(int(V),int_fdset(FDSET)) :- finite_fd_set(V,FDSET).

get_finite_fdset_information(fd(V,GS),fd_fdset(FDSET,GS)) :- finite_fd_set(V,FDSET).

get_finite_fdset_information(pred_true,single_value(pred_true)).

get_finite_fdset_information(pred_false,single_value(pred_false)).

get_finite_fdset_information(string(S),single_value(string(S))) :- ground(S).

get_next_fd_rec_field([],FieldList,RemList) :- !, FieldList=[], RemList=[].

get_next_fd_rec_field([fd_rec([FDV|Rem]) | TList], [FDV|TFieldList], [ fd_rec(Rem) | TRemList]) :- !,
    get_next_fd_rec_field(TList, TFieldList, TRemList).

get_next_fd_rec_field(List,FieldList,RemainingList) :-
    add_internal_error('Illegal call: ',get_next_fd_rec_field(List,FieldList,RemainingList)),
    FieldList=[], RemainingList=[].

ground_integer_list(Var) :- var(Var),!,fail.

ground_integer_list([]).

ground_integer_list([H|T]) :- integer(H), ground_integer_list(T).

in_fd_value_list_wf(Element,List,WF) :-
    (ground_integer_list(List) -> Gr=true ; Gr=false),
    in_fd_value_list_wf(Gr,Element,List,WF).

in_fd_value_list_wf(true,Element,List,_WF) :-
    List \= [], % avoid calling in case Element is compound (as try_get_fd_value_list will return ground for empty list)
    clpfd_inlist(Element,List). % element should not be a compound like fd_pair!

in_fd_value_list_wf(false,Element,List,WF) :-
    %get_enumeration_finished_wait_flag(WF,EWF),
    get_enumeration_starting_wait_flag(in_fd_value_list_wf,WF,EWF), % relevant for test 2070 to avoid enum warning
    in_non_ground_fd_value_lists(Element,List,EWF,top).

in_non_ground_fd_value_lists(FDP,List,EWF,_) :- nonvar(FDP), FDP = fd_pair(A,B), !,
    split_fd_pair_list(List,ListA,ListB),
    in_non_ground_fd_value_lists(A,ListA,EWF,left),
    in_non_ground_fd_value_lists(B,ListB,EWF,right).

in_non_ground_fd_value_lists(FDR,List,EWF,_) :- nonvar(FDR), FDR = fd_rec(Fields), !,
    %print(treat_fd_rec_fields(Fields,List)),nl,
    treat_fd_rec_fields(Fields,List,EWF).

in_non_ground_fd_value_lists(Element,List,_EWF,Path) :-
    Path \= top, % otherwise we know List not to be ground
    ground(List), %ground_number_list(List,Min,Max,Len), List can be a large term
    !,
    clpfd_interface:clpfd_inlist(Element,List). % this is considerably faster; especially in compiled version (see SLOT-PERFORMANCE2)

in_non_ground_fd_value_lists(Element,List,_EWF,_Path) :-
    tools:exact_member(Element,List), % avoid generating choice point for element position below
    !.

in_non_ground_fd_value_lists(Element,List,EWF,_Path) :-
    % asserts that Element is the _Nr-th element of List; in contrast to clpfd_inlist List do not have to be numbers
    post_clpfd_element(List,Element,EWF).

label_el_nr(ElementNr,Element,List,_) :-
    (number(ElementNr) -> true % clpfd:element already has a solution
    ; exact_member_nr(Element,List,1,Nr) -> ElementNr=Nr
    ; \+ fd_var(ElementNr) -> print(already_enumerating(Element,ElementNr)),nl
    % probably co-routine got activated while enumerating Element and clpfd has not yet set ElementNr,
    % but clpfd has removed the fd domain
    ; ground(List) -> (labeling([],[ElementNr]) -> true) % avoid pending co-routines in case the Element appears multiple times in the list by picking an arbitrary solution !)
    ; %translate:print_clpfd_variable(ElementNr),nl,
    labeling([],[ElementNr]) % enumerate ElementNr -> before infinite enumeration we chose possible values
% we cannot use cut after labeling, labeling ElementNr can instantiate List
% example where this is needed, {r|3 : {r,r+1} } in CLPFD=TRUE mode
).

lazy_fd_value_check(Set,E,_,FC) :- nonvar(Set), Set=[H|T], T==[],
    !, % we have a one-element singleton set
    %tools_printing:print_term_summary(equal_object(H,E)),nl,
    equal_object(H,E),
    FC=true.

lazy_fd_value_check(Set,E,WF,FullyChecked) :- preferences:preference(use_clpfd_solver,true),!,
    lazy_in_list_propagation_block(Set,E,WF,FullyChecked).

lazy_fd_value_check(_Set,_E,_WF,false).

lazy_in_list_propagation_block([],_,_,_) :- fail. % nothing can be element of empty set

lazy_in_list_propagation_block([H|T],E,WF,FullyChecked) :- contains_fd_element(H,Res,WF),
    lazy_in_list_propagation_block_2(Res,H,T,E,WF,FullyChecked).

lazy_in_list_propagation_block_2(pred_false,_H,_T,_E,_WF,false). % nothing to propagate

lazy_in_list_propagation_block_2(pred_true,H,T,E,WF,FullyChecked) :- % print(bound_h(H)),nl,
    bound_list(T,Bound),
    lazy_in_list_propagation_block_3(Bound,H,T,E,WF,FullyChecked).

lazy_in_list_propagation_block_3(pred_false,_H,_T,_E,_WF,FC) :- !, FC=false. % nothing to propagate

lazy_in_list_propagation_block_3(pred_true,H,T,E,WF,FullyChecked) :-
    try_get_fd_value_type(E,H,Type), % print(fd_val_type(E,H,Type)),nl,
    get_fd_value_list([H|T],Type,FDVals,GroundList,E), % try and extract values which can be used for CLPFD
    get_fd_value(Type,E,EFD),!,
    FDVals \= [], % if we have the empty list then membership fails
    (complete_type(Type) -> FullyChecked = true ; FullyChecked = false),
    % print(lazy_in_element(FullyChecked,GroundList,E,[H|T],WF)),nl,
    % print(in_fd_value_list_wf(GroundList,EFD,FDVals,WF,FullyChecked)),nl,
    in_fd_value_list_wf(GroundList,EFD,FDVals,WF).

lazy_in_list_propagation_block_3(pred_true,_H,_T,_E,_WF,FullyChecked) :- !,
    % should only happen for freeval with no fd type inside or for freevalues if element is not instantiated (we don't know which freval case we have)
    FullyChecked=false.

lazy_in_list_propagation_block_3(P,H,T,E,WF,false) :-
    add_internal_error('Illegal call: ',lazy_in_list_propagation_block_3(P,H,T,E,WF,false)).

post_clpfd_element(List,Element,EWF) :-
    element(Nr,List,Element),
    label_el_nr(Nr,Element,List,EWF).

split_fd_pair_list([],[],[]).

split_fd_pair_list([fd_pair(A,B)|T],[A|TA],[B|TB]) :- split_fd_pair_list(T,TA,TB).

treat_fd_rec_fields([],_,_).

treat_fd_rec_fields([V|TF],List,EWF) :-
    get_next_fd_rec_field(List,FieldFDList,RemainingList),
    %print(check(V,FieldFDList)),nl,
    in_non_ground_fd_value_lists(V,FieldFDList,EWF,rec),
    treat_fd_rec_fields(TF,RemainingList,EWF).

try_get_fd_value(T,V,_) :- var(V),var(T),!,fail.

try_get_fd_value(TV,(A,B),FD) :- var(TV),!,
    (try_get_fd_value(TA,A,FDA)
    -> (try_get_fd_value(TB,B,FDB) % What if this fails because B is still a variable !? --> ideally, typing info would help
    -> TV = couple(TA,TB), FD=fd_pair(FDA,FDB) % we have two values
    ; TV = couple_left(TA), FD=FDA)
    ; TV = couple_right(TB),
    try_get_fd_value(TB,B,FD)).

try_get_fd_value(couple(TA,TB),(A,B),fd_pair(FDA,FDB)) :-
    try_get_fd_value(TA,A,FDA),try_get_fd_value(TB,B,FDB).

try_get_fd_value(couple_left(T),(A,_),FDA) :- try_get_fd_value(T,A,FDA). % useful for domain checks

try_get_fd_value(couple_right(T),(_,A),FDA) :- try_get_fd_value(T,A,FDA). % useful for range checks

try_get_fd_value(rec_fields(T),rec(Fields),fd_rec(FD)) :-
    try_get_field_fd_values(T,Fields,FD),
    T \= [].

try_get_fd_value(global(GS),fd(X,GS),X).

try_get_fd_value(integer,int(X),X).

try_get_fd_value_list(Set,Type,FDList,GroundList) :-
    try_get_fd_value_list5(Set,Type,FDList,true,GroundList).

try_get_fd_value_list5(V,_,_,_,_) :- var(V),!,fail.

try_get_fd_value_list5([],_,[],G,G). % Note if this is the base case then the type could be that of an empty list of pairs !

try_get_fd_value_list5([H|T],Type,FDList,GroundIn,GroundOut) :-
    try_get_fd_value(Type,H,Value),!, FDH=Value,
    (GroundIn=true,integer(FDH) -> Ground1=true ; Ground1=false),
    %%(ground(T) -> true ; print(get_fd_val_list(H,T)),nl),
    check_non_var_list(T), % do not instantiate any free variable ! otherwise we get full domain probably anyway ?
    if(get_fd_value_list5(T,Type,FDT,Ground1,GroundOut,_NoFilterEl,1),
    FDList = [FDH|FDT],
    FDList = []). % obtaining FD value triggered inconsistency

try_get_fd_value_list5(avl_set(A),_,_,_,_) :-
    add_internal_error('Not a list: ',try_get_fd_value_list5(avl_set(A),_,_,_,_)),fail.

try_get_fd_value_list5(node(A,B,C,D,E),_,_,_,_) :-
    add_internal_error('Not a list: ',try_get_fd_value_list5(node(A,B,C,D,E),_,_,_,_)),fail.

try_get_fd_value_list5(closure(A,B,C),_,_,_,_) :-
    add_internal_error('Not a list: ',try_get_fd_value_list5(closure(A,B,C),_,_,_,_)),fail.

try_get_fd_value_type(V1,V2,T) :- var(V1),!, try_get_fd_value(T,V2,_).

try_get_fd_value_type((A1,_),(A2,_),T) :- nonvar(T),T=couple_left(TA),!,
    try_get_fd_value_type(A1,A2,TA). % useful for domain checks

try_get_fd_value_type((A1,B1),(A2,B2),Type) :- !,
    (try_get_fd_value_type(A1,A2,TA)
    -> (try_get_fd_value_type(B1,B2,TB)
    -> Type = couple(TA,TB) % we have two values
    ; %print(failed_right(B1,B2,TB)),nl,
    Type = couple_left(TA))
    ; Type = couple_right(TB),
    try_get_fd_value_type(B1,B2,TB)).

try_get_fd_value_type(freeval(ID,Case,Val1),V2, freeval_case(ID,Case,Type)) :- !,
    nonvar(Case), ground(ID),
    (nonvar(V2),V2 = freeval(ID2,Case2,Val2),
    (ID,Case) == (ID2,Case2)
    -> try_get_fd_value_type(Val1,Val2,Type)
    ; % TO DO: if the cases do not match and if Val1 is a variable then we may miss FD values
    %print(case_mismatch(ID,Case,V2)),nl,
    get_freeval_type(ID,Case,_CaseType),
    %print(freeval_case_type(ID,Case,CaseType,Val1)),nl,
    % TO DO: use CaseType in case Val1 is not instantiated enough
    try_get_fd_value(Type,Val1,_)).

try_get_fd_value_type(V1,V2,T) :-
    (var(V2) -> try_get_fd_value(T,V1,_) ; try_get_fd_value(T,V2,_)).

try_get_field_fd_values(_,Fields,_) :- var(Fields),!,fail. % we don't know all the fields; better do nothing

try_get_field_fd_values(Types,[],FDVals) :- !,Types=[],FDVals=[].

try_get_field_fd_values(_,[FN|_],_) :- var(FN),!,fail.

try_get_field_fd_values(_,[field(Name,_)|_],_) :- var(Name),!,fail.

try_get_field_fd_values(Types,[field(Name,Value)|TF],FDVals) :-
    try_get_fd_value(T,Value,FDVal),
    !,
    Types = [field(Name,T)|TTypes],
    FDVals = [FDVal|TFD],
    try_get_field_fd_values(TTypes,TF,TFD).

try_get_field_fd_values([field_no_fd(Name)|Types],[field(Name,_)|TF],FDVals) :-
    try_get_field_fd_values(Types,TF,FDVals).

try_in_fd_value_list_check([],_,_,_) :- fail.

try_in_fd_value_list_check([H|T],El,Type,WF) :-
    try_get_fd_value_type(El,H,Type), % print(fd_val_type(El,H,T)),nl,
    !,
    get_fd_value_list([H|T],Type,FDList,GroundList,El),
    get_fd_value(Type,El,ElFD),
    in_fd_value_list_wf(GroundList,ElFD,FDList,WF).

try_in_fd_value_list_check(S,El,Type,WF) :-
    (S=[_|_] -> true
    ; add_internal_error('Illegal call: ',try_in_fd_value_list_check(S,El,Type,WF))).

valid_rec_type(field(_,T)) :- valid_type(T).

valid_rec_type(field_no_fd(_)).

valid_type(couple(TA,TB)) :- valid_type(TA),valid_type(TB).

valid_type(couple_left(TA)) :- valid_type(TA).

valid_type(couple_right(TA)) :- valid_type(TA).

valid_type(global(GS)) :- atomic(GS).

valid_type(rec_fields(Fs)) :- maplist(valid_rec_type,Fs).

valid_type(freeval_case(_,_,TA)) :- valid_type(TA).

valid_type(integer).