kernel_cardinality

add_cs_card(_CS,CSCard,Acc,Res,_WF) :- number(CSCard),!,Res is Acc+CSCard.

add_cs_card(CS,_,_Acc,_Res,WF) :- add_wd_error('card applied to infinite (or very large) set: ',CS,WF).

attach_int_cardinality(Var,VCard,_WF) :-
    frozen(Var,Goals), % print(frozen(Var,Goals)),nl,
    get_finite_int_card(Goals,Var,GCard),!, % there is already co-routine attached
    print(reusing_coroutine(Var,GCard)),nl,
    VCard=GCard.

attach_int_cardinality(Var,VCard,WF) :- geqzero(VCard),
    force_last_empty_set(Var,VCard,WF),
    block_finite_int_cardinality(Var,VCard,WF).

block_finite_int_cardinality([],Card,_) :- !, Card=0.

block_finite_int_cardinality([_|T],N,WF) :- !,plus1(N1,N),block_finite_int_cardinality(T,N1,WF).

block_finite_int_cardinality(CS,Res,WF) :-
    explicit_set_cardinality_wf(CS,CSCard,WF), % TO DO: use finite version and unify Card and CSCard
    add_cs_card(CS,CSCard,0,Res,WF).

delay_plus1(N,N1) :- var(N1),!, N1 is N+1.

delay_plus1(N,N1) :- N is N1-1.

finite_int_cardinality(V,int(Card),WF) :- finite_int_cardinality4(V,0,Card,WF).

finite_int_cardinality4(V,SoFar,Card,WF) :- var(V),!,
    int_plus(int(SoFar),int(VCard),int(Card)),
    attach_int_cardinality(V,VCard,WF).

finite_int_cardinality4([],Acc,Card,_) :- !, Card=Acc.

finite_int_cardinality4([_|T],Acc,N,WF) :- !, A1 is Acc+1, finite_int_cardinality4(T,A1,N,WF).

finite_int_cardinality4(CS,Acc,Card,WF) :-
    explicit_set_cardinality_wf(CS,CSCard,WF), % TO DO: use finite version which itself raises WD error when inf and use clpfd addition
    add_cs_card(CS,CSCard,Acc,Card,WF),
    % TO DO: instantiate list skeleton if last_finite_priority encountered as this sometimes enables detection of inconsistencies; see test 1611
    (var(Card) -> clpfd_geq(Card,Acc,_) ; true).

force_empty_set1(Set,0,WF) :- !, (var(Set) -> empty_set_wf(Set,WF) ; true).

force_empty_set1(Set,Nr,WF) :- force_empty_set2(Set,Nr,WF).

force_empty_set2([_|T],Nr,WF) :- !, N1 is Nr-1, force_empty_set1(T,N1,WF).

force_empty_set2(_,_,_).

force_last_empty_set(Set,Nr,WF) :- force_empty_set1(Set,Nr,WF).

get_finite_int_card(kernel_cardinality:block_finite_int_cardinality(Var,VarCard,_),W,GCard) :- W==Var,!, GCard=VarCard.

get_finite_int_card((A,B),W,GCard) :- get_finite_int_card(A,W,GCard) -> true ; get_finite_int_card(B,W,GCard).

plus1(N,N1) :- number(N),!,N1 is N+1.

plus1(N,N1) :- preference(use_clpfd_solver,false),!, delay_plus1(N,N1).