b_enumerate

add_enum_warning_info(lambda_result(Trigger),Res) :- !, Res=lambda_result(Trigger).

add_enum_warning_info(Trigger,lambda_result(Trigger)).

b_enumerate_typed_values(Values,Types,WF) :- % called by b_execute_eventb_action(becomes_element_of, ...
    b_generate_typed_values(Values,Types,TypedVals),
    b_tighter_enumerate_all_values(TypedVals,WF).

b_enumerate_values_in_store(Variables,Types,Values,Store,WF) :-
    generate_typed_var_list(Variables,Types,Store,Values,TypedValues),
    b_tighter_enumerate_all_values(TypedValues,WF).

b_extract_typedvalc([],[],_,_,[]).

b_extract_typedvalc([Variable|VT],[Type|TT],Infos,Store,Res) :-
    (is_lambda_result_or_useless(Variable,Infos,[]) % TO DO: check if we can pass DO_NOT_ENUMERATE Infos
    % TO DO: use lambda_result info field ?; Note the check is repeated below in sort_typed_values
    -> b_extract_typedvalc(VT,TT,Infos,Store,Res)
    % lambda result does not need to be enumerated; will be computed from rest
    % TO DO: should we also deal specially with _lambda_result_ below in b_tighter_enumerate_values;
    % or even infer in ANY statements, ... which variables are simply defined by equalities from the others
    ; Res=[ExtractedH|ET],
    b_extract_typedvalc_var(Variable,Type,Infos,Store,ExtractedH),
    b_extract_typedvalc(VT,TT,Infos,Store,ET)).

b_extract_typedvalc_var(Var,Type,Infos,Store,typedval(Val,Type,VarID,TINFO)) :-
    (Var = 'Identifier'(VarID)
    -> print(b_tighter_enumerate_value_in_store(Var,Type)),print(' variable not in proper form'),nl
    ; VarID = Var),
    construct_typedval_infos(VarID,Infos,trigger_true(VarID),TINFO),
    (store:lookup_value_for_existing_id(VarID,Store,Val), Val \== fail
    -> true
    ; add_internal_error('Variable has not been given value: ',VarID)
).

b_generate_typed_values([],[],[]).

b_generate_typed_values([Val|Vrest],[Type|Trest],[typedval(Val,Type,'$UNKNOWN_ID',TINFO)|TVrest]) :-
    construct_typedval_infos('$unknown',[],trigger_true(unknown),TINFO),
    b_generate_typed_values(Vrest,Trest,TVrest).

b_tighter_enumerate_all_values(TypedValues,WF) :-
    b_tighter_enumerate_values(TypedValues,enum_info([],[]),WF).

b_tighter_enumerate_single_value(Val,Type,Infos,VarID,WF) :-
    construct_typedval_infos(VarID,Infos,trigger_true(VarID),TINFO),
    b_tighter_enumerate_all_values([typedval(Val,Type,VarID,TINFO)],WF).

b_tighter_enumerate_sorted_value_and_continue(_LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
    (Rest = [] -> true ; get_minimum_waitflag_prio(WF,Prio,_), Prio < 20000),
    % only check for useless if there are either other variables to chose from or other WF goals
    currently_useless_variable(Val),
    !,
    b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF).

b_tighter_enumerate_sorted_value_and_continue(_LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
    check_reached(Val,Type,VarID,Card,WF), %% <-----
    %% tools:print_bt_message(enumerate(VarID,Val)),
    enum_tight_with_wf(Val,Type,EnumWarning,WF),
    %% tools:print_bt_message(after_enumerate(VarID,Val)),
    %(VarID=='VS_NOERRORCOND' -> print(done_enum(VarID,Val)),nl ; true),
    b_tighter_enumerate_sorted_values(Rest,WF).

b_tighter_enumerate_sorted_values([],_WF).

b_tighter_enumerate_sorted_values([typedvalc(Val,Type,VarID,EnumWarningInfos,Card)|Rest],WF) :-
    (ground_value(Val)
    -> check_reached(Val,Type,VarID,Card,det,WF), %% <-----
    b_tighter_enumerate_sorted_values(Rest,WF) %% no need to enumerate this value
    ; treat_next_typed_valc(Type,Val,VarID,EnumWarningInfos,Card,Rest,WF)).

b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
    get_next_useful_variable(Rest,RVal,RType,RVarID,REnumWarning,RCard,RRest), % ,print(using(RVarID,RVal,RType)),nl
    !,
    %debug_println(9,skipping(Val,VarID,Card,new(RVal,RType,RVarID,RCard))),
    (RCard =< Card /* we can enumerate straight away */
    -> check_reached(RVal,RType,RVarID,RCard,WF), %% <------
    enum_tight_with_wf(RVal,RType,EnumWarning,WF),
    b_tighter_enumerate_sorted_values([typedvalc(Val,Type,VarID,EnumWarning,Card)|RRest],WF)
    ; b_tighter_enumerate_sorted_values([typedvalc(RVal,RType,RVarID,REnumWarning,RCard),
    typedvalc(Val,Type,VarID,EnumWarning,Card)|RRest],WF)
).

b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
    %debug_println(19,all_variables_useless(Val,Card)),
    get_minimum_waitflag_prio(WF,Prio,_Info),
    Prio < 20000, % avoid infinite enumeration ... TO DO: improve check
    %debug_println(19,all_variables_useless_info(Prio,Info)),
    !,
    ground_wait_flag_to(WF,Prio),
    % Now try again:
    b_tighter_enumerate_sorted_value_and_continue(1,Val,Type,VarID,EnumWarning,Card,Rest,WF).

b_tighter_enumerate_useless(Val,Type,VarID,EnumWarning,Card,Rest,WF) :-
    check_reached(Val,Type,VarID,Card,WF), %% <-----
    %% tools:print_bt_message(enumerate(VarID,Val)),
    enum_tight_with_wf(Val,Type,EnumWarning,WF),
    %% tools:print_bt_message(after_enumerate(VarID,Val)),
    %(VarID=='VS_NOERRORCOND' -> print(done_enum(VarID,Val)),nl ; true),
    b_tighter_enumerate_sorted_values(Rest,WF).

b_tighter_enumerate_values(TypedValues,enum_info(UselessIds,DelayedIds),WF) :- !,
    %print(sort_typed(UselessIds,DelayedIds)),nl,
    sort_typed_values(TypedValues,[],UselessIds,DelayedIds,SortedValues),
    b_tighter_enumerate_sorted_values(SortedValues,WF).

b_tighter_enumerate_values(TV,EI,WF) :-
    add_internal_error('Illegal call: ',b_tighter_enumerate_values(TV,EI,WF)),
    fail.

b_tighter_enumerate_values_in_ctxt(TypedValues,ContextPred,WF) :-
    extract_do_not_enum_ids_from_predicate(ContextPred,UselessIds),
    b_tighter_enumerate_values(TypedValues,UselessIds,WF).

b_type_value_in_store(Var,Type,Store) :-
    (Var = 'Identifier'(VarID)
    -> add_internal_error('Variable not in proper form: ',b_type_value_in_store(Var,Type,_))
    ; VarID = Var),
    lookup_value_for_existing_id(VarID,Store,Val),
    (Val==fail
    -> add_internal_error('Variable has not been given value: ',b_type_value_in_store(Var,Type,Store))
    ; kernel_objects:basic_type(Val,Type)).

b_type_values_in_store([],[],_).

b_type_values_in_store([Variable|VT],[Type|TT],Store) :-
    b_type_value_in_store(Variable,Type,Store),
    b_type_values_in_store(VT,TT,Store).

better_enum((A,B),Trigger,Val,Depth) :- better_enum(A,Trigger,Val,Depth), better_enum(B,Trigger,Val,Depth).

better_enum(prolog:trig_and(_,_,_,_,Trigger1),Trigger,Val,Depth) :- !,
    (Trigger1==Trigger -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).

better_enum(prolog:trig_or(_,Trigger1,_),Trigger,Val,Depth) :- !,
    (Trigger1==Trigger -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).

better_enum(prolog:trig_ground(VV,_,_,Trigger1,_),Trigger,Val,Depth) :- !,
    (Trigger1==Trigger -> true ; VV=Val -> true ; triggers_better_enumeration(Trigger1,Val,Depth)).

better_enum(prolog:when(WT,_,G), Trigger,Val,Depth) :- !,
    Trigger==WT, better_enum(G,Trigger,Val,Depth).

better_enum(custom_explicit_sets:couple_element_of_avl_set(_X,_Y,_AVL,_WF1,_WF),_,_Val,_Depth) :- !,
    % TO DO: add more enumerators of Val
    % TO DO: VAL occurs in _X !!
    true.

better_enum(external_functions:G,_,_Val,_Depth) :- external_debug_function(G).

cardval_greater_than(C1,_,Card,_) :- infgreater(C1,Card). %Card \== inf, (C1=inf -> true ; C1>Card).

cardval_greater_than(Card,V1,Card,Val) :-
    var(V1), nonvar(Val). % if card equal give priority to nonvariable values

cardval_greater_than(Card,_,Card,_) :-
    preferences:preference(randomise_enumeration_order,true),
    % TO DO: maybe we even want to change the order if cardinality different ?
    % this also does not really generate random permutation of variables with same cardinality
    random(1,3,1).

check_reached(Val,Type,Var,Card,_WF) :- is_lambda_result_id(Var),
    Card \= det, \+ ground_value(Val), !,
    format('~n*** Enumerating lambda result ~w : ~w (Type=~w, Card=~w)~n~n',[Var,Val,Type,Card]).

check_reached(_Val,_Type,_VarID,_Card,_WF). % :- format('Enumerating ~w (~w) : ~w~n',[_VarID,_Card,_Val]).

check_reached(_Val,_Type,_VarID,_Card,_Info,_WF). % :- format('Enumerating ~w (~w:~w) : ~w~n',[_VarID,_Card,_Info,_Val]).

construct_typedval_infos(VarID,Infos,Trigger,Res) :-
    member(Info,Infos),
    lambda_result_info(Info,VarID),
    !,
    Res = lambda_result(Trigger).

construct_typedval_infos(_,_,Trigger,Trigger).

currently_useless_variable(Val) :- var(Val),!,frozen(Val,Goal), % this can be expensive when Goal is large !
    (enumeration_only_goal(Goal,Val) -> true).

currently_useless_variable(int(Val)) :- currently_useless_variable(Val).

currently_useless_variable(fd(Val,_)) :- currently_useless_variable(Val).

currently_useless_variable(string(Val)) :- currently_useless_variable(Val).

degree_value(integer,Val,Dg) :- %translate:print_value_variable(Val),nl,
    nonvar(Val), Val=int(FD), fd_degree(FD,Dg), number(Dg).

enum_tight_with_wf(Val,Type,EnumWarningInfos,WF) :-
    get_enum_warning_info(EnumWarningInfos,EnumWarning),
    enumerate_tight_type_wf(Val,Type,EnumWarning,WF).

enumeration_only_goal(true,_).

enumeration_only_goal((A,B),Val) :-
    (enumeration_only_goal(A,Val) -> enumeration_only_goal(B,Val)
    ; % we have not detected A as enumeration only: check if we can find an annotation not to enumerate
    force_enumeration_only_goal(A,Val) % Note: we only check first component; on the assumption that these co-routines are added early and to avoid useless lookups; TO DO: is there a better solution ?
).

enumeration_only_goal(dif(A,B),Var) :- (Var==A ; Var==B). % SWI

enumeration_only_goal(Module:Call,Val) :- enumeration_only_goal_m(Module,Call,Val).

enumeration_only_goal_m(kernel_objects,call_enumerate_int(V,_,_,_),Val) :- !, V==Val.

enumeration_only_goal_m(kernel_objects,enumerate_int_wf(V,_,_),Val) :- !, V==Val.

enumeration_only_goal_m(kernel_objects,enumerate_natural(V,_,_,_),Val) :- !, V==Val.

enumeration_only_goal_m(prolog,dif(A,B),Var) :- !, (Var==A ; Var==B).

enumeration_only_goal_m(bsets_clp,is_sequence_wf_ex(V,GS,_,_),Val) :- V==Val,
    nonvar(GS),GS=global_set(_). % only constraint: we should generate a sequence

enumeration_only_goal_m(external_functions,string_to_int2(_,V,_,_),Val) :- !, V==Val.

enumeration_only_goal_m(external_functions,printf(_,V,_,_),Val) :-!, V==Val.

enumeration_only_goal_m(external_functions,block_print_value(_,_,_V,_,_),_Val) :- !. % from observe

enumeration_only_goal_m(external_functions,block_print_value_complete(_,_,_,_,_),_Val). % from observe

enumeration_only_goal_m(b_interpreter_components,observe_variable_block(_,_,_,_,_),_) :- !. % in -p TRACE_INFO TRUE mode

enumeration_only_goal_m(b_interpreter_components,observe_variable1_block(_,_,_,_),_).

enumeration_only_goal_m(prolog,trig_ground(A1,_,_,_,Trigger),Val) :- Val==A1,
    triggers_better_enumeration(Trigger,Val,3). % if this only triggers an enumeration of Val itself; it is better to let the other variable trigger the enumeration

external_debug_function(fprintf2(_,_,_,_)). % TO DO: add more

extract_do_not_enum_ids_from_predicate(b(Pred,_,Infos),enum_info(SortedUselessIds,DelayedIds)) :- !,
    findall(ID,member(prob_annotation('DO_NOT_ENUMERATE'(ID)),Infos),UselessIds1),
    findall(ID,find_useless_enumeration_id(Pred,ID),UselessIds,UselessIds1),
    findall(delay_enum(PosNr,ID),member(prob_annotation('DELAY_ENUMERATION'(PosNr,ID)),Infos),DelayedIds),
    sort(UselessIds,SortedUselessIds).

extract_do_not_enum_ids_from_predicate(P,Res) :-
    add_internal_error('Illegal call: ',extract_do_not_enum_ids_from_predicate(P,Res)),
    Res=enum_info([],[]).

extract_useless(b(couple(A,B),_,_),UselessID) :-
    (extract_useless(A,UselessID) ; extract_useless(B,UselessID)).

extract_useless(b(identifier(UselessID),_,_),UselessID) :-
    % the identifier is bound by the member test; we do not need to enumerate it
    debug_println(9,not_enum_inside_closure(UselessID)).

find_useless_enumeration_id(member(LHS,b(value(V),_,_)),UselessID) :-
    % we enumerate the identifier using memberships of avl_sets which will be more precise than naive enumeration
    nonvar(V), V=avl_set(_),
    extract_useless(LHS,UselessID).

find_useless_enumeration_id(conjunct(TA,TB),UselessID) :-
    (get_preference(use_clpfd_solver,false) -> true
    ; get_preference(data_validation_mode,true)),
    % only look deeper if CLPFD is off; useful for test 1945, 1162
    % in general it could be better to enumerate a variable if it occurs in multiple sets and we using CLPFD intersection we can narrow down the interval
    % e.g., x: 1..100 & x:99..1000 --> we can narrow down x to 99..100 and it would be better to enumerate x
    (get_texpr_expr(TA,P) ; get_texpr_expr(TB,P)),
    find_useless_enumeration_id(P,UselessID).

finite_fields(_Type,Val,_) :- var(Val),!,fail.

finite_fields([],[],1).

finite_fields([HType|TTypes],[H|T],Size) :- finite_fields(TTypes,T,SizeT), finite_value(HType,H,SizeH),
    safe_mul(SizeT,SizeH,Size), number(Size).

finite_value(integer,Val,Size) :- nonvar(Val), Val=int(FD), clpfd_size(FD,Size), number(Size).

finite_value(boolean,Val,Size) :- (ground(Val) -> Size = 1 ; Size =2).

finite_value(string(_),Val,Size) :- ground(Val), Size=1.

finite_value(real(_),Val,Size) :- ground(Val), Size=1.

finite_value(global(G),Val,Size) :- (ground(Val) -> Size = 1 ; b_global_set_cardinality(G,Size)).

finite_value(set(T),Val,Size) :- nonvar(Val), l_finite_value(T,Val,Size).

finite_value(couple(T1,T2),Val,Size) :- nonvar(Val), Val = (V1,V2),
    finite_value(T1,V1,Size1),
    finite_value(T2,V2,Size2),
    safe_mul(Size1,Size2,Size), number(Size). % can also be inf_overflow !

finite_value(record(Fields),Val,Size) :-
    nonvar(Val), Val=rec(FVals),
    finite_fields(Fields,FVals,Size), nl,print(finite_field(Val,Size)),nl,nl.

force_enumeration_only_goal((A,B),Val) :-
    (force_enumeration_only_goal(A,Val) -> true ; force_enumeration_only_goal(B,Val) ).

force_enumeration_only_goal(external_functions:'DO_NOT_ENUMERATE'(V,_,_),Val) :- V==Val.

generate_typed_var_list([],[],_,[],[]).

generate_typed_var_list([VarID|VT],[Type|TT],Store,Values,Res) :-
    (store:lookup_value_for_existing_id(VarID,Store,Val), Val \== fail
    -> construct_typedval_infos(VarID,[],trigger_true(VarID),TINFO),
    Res = [typedval(Val,Type,VarID,TINFO)|Rest], % always trigger enumeration warning
    Values=[Val|ValT]
    ; add_internal_error('Variable has not been given value: ',VarID),
    Res=Rest,Values=ValT
    ),
    generate_typed_var_list(VT,TT,Store,ValT,Rest).

get_enum_warning_info(lambda_result(Trigger),Res) :- !, Res=Trigger.

get_enum_warning_info(Trigger,Trigger).

get_max_cardinality_as_priority(integer,Prio) :- !, integer_priority(Prio).

get_max_cardinality_as_priority(Type,Prio) :-
    max_cardinality(Type,Card), !,
    (number(Card) % \= inf or inf_overflow
    -> %Prio=Card
    get_bounded_priority(Card,Prio)
    ; inf_type_prio(Type,Prio)
).

get_max_cardinality_as_priority(Type,Prio) :-
    add_internal_error('Failed: ',max_cardinality(Type,_)),
    integer_priority(Prio).

get_next_useful_variable([typedvalc(Val,Type,VarID,EnumWarning,Card)|Rest],RVal,RType,RVarID,REnumWarning,RCard,RRest) :-
    (currently_useless_variable(Val)
    -> RRest=[typedvalc(Val,Type,VarID,EnumWarning,Card)|TRRest],
    get_next_useful_variable(Rest,RVal,RType,RVarID,REnumWarning,RCard,TRRest)
    ; RRest=Rest, RVal=Val, RType=Type, RVarID=VarID, REnumWarning = EnumWarning, RCard=Card
).

get_typedvalc_finite_size(Type,Val,Size) :-
    finite_value(Type,Val,Size),
    (Size=1 -> true ;
    \+ currently_useless_variable(Val)). % ,print(finite(Val,Size)),nl.

get_typedvalc_priority(typedvalc(Val,Type,_,Enum,_Prio),Res) :- %Type=integer,
    (Enum = lambda_result(_) -> Res=sup(1) % do not give priority to lambda_result
    ; get_typedvalc_finite_size(Type,Val,Size)
    -> Res=Size % we have a finite value: use size
    ; degree_value(Type,Val,Dg)
    -> NDg is -Dg, Res=sup(NDg) % use negative number of degree, so that larger degrees get priority
    % relevant for e.g. test 1484: res=x*x+4*x+14
    ; Res = sup(1)
).

inf_type_prio(integer,Prio) :- !, integer_priority(Prio).

inf_type_prio(real,Prio) :- !, integer_priority(P1), Prio is P1+11.

inf_type_prio(seq(X),Prio) :- !, inf_type_prio(X,P1), Prio is P1+11.

inf_type_prio(set(X),Prio) :- !, inf_type_prio(X,P1), Prio is P1+10.

inf_type_prio(_,Prio) :- !, integer_priority(P), Prio is P+1.

insert_val([],Val,Type,VarID,EnumWarning,Card,[typedvalc(Val,Type,VarID,EnumWarning,Card)]).

insert_val([TC|T], Val,Type, VarID, EnumWarning, Card, Res) :-
    TC = typedvalc(V1,_T1,_Var1,_W1,C1),
    (cardval_greater_than(C1,V1,Card,Val)
    -> Res = [typedvalc(Val,Type,VarID,EnumWarning,Card),TC|T]
    ; Res = [TC|RT],
    insert_val(T,Val,Type,VarID,EnumWarning,Card,RT)
).

is_lambda_result_annotated(ID,lambda_result(Trigger)) :-
    (var(Trigger) -> add_internal_error('Illegal trigger for enumeration variable:',ID),fail
    ; true).

is_lambda_result_id('_lambda_result_'). % TO DO: use lambda_result info field ?

is_lambda_result_or_useless(ID,TINFO,DoNotEnumIds) :-
    (is_lambda_result_id(ID) -> true
    ; is_lambda_result_annotated(ID,TINFO) -> true
    ; ord_member(ID,DoNotEnumIds)).

l_finite_value(_Type,Val,_) :- var(Val),!,fail.

l_finite_value(_,avl_set(_),1).

l_finite_value(_Type,[],1).

l_finite_value(Type,[H|T],Size) :- l_finite_value(Type,T,SizeT), finite_value(Type,H,SizeH),
    safe_mul(SizeT,SizeH,Size), number(Size).

lambda_result_info(lambda_result(VarID),VarID).

lambda_result_info(prob_annotation('DO_NOT_ENUMERATE'(VarID)),VarID).

portray_typed_values(List) :- maplist(print_typedvalc,List),nl.

print_typedvalc(typedvalc(_Val,_Type,VarID,_EnumWarning,Card)) :-
    format('~w (card:~w) ',[VarID,Card]).

smallest_value([H|T],Selected,Rest,Prio) :-
    get_typedvalc_priority(H,HPrio),
    smallest_value_aux(T,H,HPrio,Selected,Rest,Prio).

smallest_value_aux([],H,HPrio,H,[],HPrio).

smallest_value_aux([H|T],Acc,AccPrio,Selected,Rest,SelPrio) :-
    get_typedvalc_priority(H,HPrio),
    (HPrio=1 -> smallest_value_aux(T,Acc,AccPrio,Selected,Rest,SelPrio) % remove this TC from list; does not need to be enumerated anymore
    ; HPrio @< AccPrio
    -> Rest = [Acc|TRest],
    smallest_value_aux(T,H,HPrio,Selected,TRest,SelPrio)
    ; Rest = [H|TRest],
    smallest_value_aux(T,Acc,AccPrio,Selected,TRest,SelPrio)
).

sort_typed_values([],R,_,_,R).

sort_typed_values([typedval(Val,Type,VarID,EnumWarningInfo)|Rest],SortedSoFar,UselessIds,DelayedIds,Res) :-
    %% comment in next line to keep track of variable names for enumeration warnings, etc...
    %% register_prolog_variable_name(Val,VarID,Type), % dummy call to register variable name with free Prolog variables
    (is_lambda_result_or_useless(VarID,EnumWarningInfo,UselessIds) -> % DO_NOT_ENUMERATE
    (%Rest=[],SortedSoFar=[], % we used to check it is the only non-ground value to enumerate
    \+ ground_value(Val)
    % could be relevant if a variable was annotated as do_not_enumerate and there is a WD error in
    % the expression defining it, e.g. in test 2337: {id19,id20|id19 : BOOL & id20 <: INTEGER}(id1) = x
    -> % Note: we can have a construct {lambda_result| #x.( P(x) & lambda_result=E(x))},
    % we want to enumerate it after trying to solve the existential quantifier
    last_priority(Prio), % important that it is higher than existential quantifier prio, cf test 1492
    add_enum_warning_info(EnumWarningInfo,NewInfo),
    insert_val(SortedSoFar,Val,Type,VarID,NewInfo,Prio,NewSorted),
    (debug:debug_level_active_for(9),
    Rest\=[], SortedSoFar \= [] % then it is the only variable anyway
    -> format('~n*** Possibly enumerating lambda result ~w : ~w (~w:~w)~n~n',[VarID,Val,Type,Prio])
    ; true)
    % was triggered in test 1093 and 1161, but seems no longer necessary there
    ; NewSorted=SortedSoFar % completely skip enumeration
    )
    ; ground_value(Val) -> NewSorted=SortedSoFar
    ; get_max_cardinality_as_priority(Type,CardPrio),
    (member(delay_enum(PosNr,VarID),DelayedIds),
    integer_pow2_priority(Prio), P2 is Prio+PosNr,
    P2>CardPrio
    -> debug_println(9,'DELAY_ENUMERATION'(VarID,PosNr,P2,CardPrio)),
    get_bounded_priority(P2,EnumPrio)
    ; EnumPrio=CardPrio),
    %% TO DO: maybe also take shape of Val into account; e.g. if cardinality of a set already fixed...
    insert_val(SortedSoFar,Val,Type,VarID,EnumWarningInfo,EnumPrio,NewSorted)
    ),
    sort_typed_values(Rest,NewSorted,UselessIds,DelayedIds,Res).

treat_next_integer(LWF,_,Val,VarID,EnumWarning,_Card,Rest,WF) :- LWF \== first_iteration, % print(treat(Val,VarID,Rest)),nl,
    nonvar(Val), Val=int(FD),
    clpfd_size(FD,Size), % will return sup if no bounds + also works in non-CLPFD mode
    %print(treat_next_integer(VarID,Val,Size,_Card,Rest)),nl,
    number(Size),!,
    (Size = 1 % for Size=1 no enumeration is necessary anyway
    -> b_tighter_enumerate_sorted_values(Rest,WF) % no enumeration required
    ; treat_next_typed_valc_normal(integer,Val,VarID,EnumWarning,Size,Rest,WF)).

treat_next_integer(_,Prios,Val,VarID,EnumWarning,Card,OtherTCs,WF) :- % ideally we should move this above the clause with NextPrio; but then test 412 fails
    CurTC = typedvalc(Val,integer,VarID,EnumWarning,Card),
    smallest_value([CurTC|OtherTCs],TC,Rest,Size),
    (number(Size) % finite domain found
    ;
    Prios = [] % no more delaying; we have to enumerate an unbounded value
    ),
    !,
    (Size == 1 % no enumeration required for this variable
    -> b_tighter_enumerate_sorted_values(Rest,WF)
    ; treat_next_typed_valc_normal4(TC,Size,Rest,WF)
).

treat_next_integer(_,[NextPrio|Prios],Val,VarID,EnumWarning,Card,Rest,WF) :- !, % for test 1161 this clause causes a considerable slowdown
    get_wait_flag(NextPrio,treat_next_integer(VarID,Val),WF,LWF),
    treat_next_integer(LWF,Prios,Val,VarID,EnumWarning,Card,Rest,WF).

treat_next_integer(_,_,Val,VarID,EnumWarning,Card,Rest,WF) :-
    treat_next_typed_valc_normal(integer,Val,VarID,EnumWarning,Card,Rest,WF). % we have already delayed; no need to delay further

treat_next_typed_valc(integer,Val,VarID,EnumWarningInfos,_Card,Rest,WF) :-
    nonvar(Val), Val=int(FD),
    clpfd_size(FD,Size), % will return sup if no bounds + also works in non-CLPFD mode
    number(Size),!,
    treat_next_typed_valc_normal(integer,Val,VarID,EnumWarningInfos,Size,Rest,WF).

treat_next_typed_valc(integer,Val,VarID,EnumWarningInfos,Card,Rest,WF) :-
    !,
    large_finite_priority(LP),
    treat_next_integer(first_iteration,[LP],Val,VarID,EnumWarningInfos,Card,Rest,WF). % TO DO: maybe do several iterations 1000,LP

treat_next_typed_valc(Type,Val,VarID,EnumWarningInfos,Card,Rest,WF) :- % TO DO: also look for finite values in Rest if Type is infinite but not integer
    treat_next_typed_valc_normal(Type,Val,VarID,EnumWarningInfos,Card,Rest,WF).

treat_next_typed_valc_normal(Type,Val,VarID,EnumWarning,Card,Rest,WF) :-
    get_wait_flag(Card,tighter_enum(VarID,Val,Type),WF,LWF),
    b_tighter_enumerate_sorted_value_and_continue(LWF,Val,Type,VarID,EnumWarning,Card,Rest,WF).

treat_next_typed_valc_normal4(typedvalc(Val,Type,VarID,EnumWarning,Card),Size,Rest,WF) :-
    (number(Size) -> NewCard=Size ; NewCard=Card), % use narrowed down card if possible
    treat_next_typed_valc_normal(Type,Val,VarID,EnumWarning,NewCard,Rest,WF).

triggers_better_enumeration(Trigger,Val,Depth) :- Depth>0, D1 is Depth-1,
    frozen(Trigger,TrigGoal),
    ( better_enum(TrigGoal,Trigger,Val,D1) -> true).