kernel_card_arithmetic

add_card2(A,B,R) :- safe_add_card(A,B,R).

blocking_add_card(X,Y,R) :- X==0,!,R=Y.

blocking_add_card(X,Y,R) :- Y==0,!,R=X.

blocking_add_card(X,_,R) :- X==inf,!,R=inf.

blocking_add_card(_,Y,R) :- Y==inf,!,R=inf.

blocking_add_card(X,Y,R) :- add_card2(X,Y,R).

blocking_factorial(inf,R) :- !, R=inf.

blocking_factorial(inf_overflow,R) :- !, R=inf_overflow.

blocking_factorial(X,R) :- X<0,!, add_error(blocking_factorial,'Negative arg: ',blocking_factorial(X,R)),R=0.

blocking_factorial(X,R) :- X>1000,!,
    % here we overapproximate: throw finite warning in Disprover mode ? or when checking for finite
    set_inf_due_to_overflow(R).

blocking_factorial(A,Res) :- fact(A,1,Res).

blocking_factorial_k(_X,0,R) :- !, R=1.

blocking_factorial_k(inf,_,R) :- !, R=inf.

blocking_factorial_k(_N,K,R) :- K=inf,!, R=0. % only finitely many _N

blocking_factorial_k(inf_overflow,_,R) :- !, R=inf_overflow.

blocking_factorial_k(_N,K,R) :- K=inf_overflow,!, R=0.

blocking_factorial_k(N,K,R) :- K>N,!, R=0.

blocking_factorial_k(A,K,Res) :- fact_k(A,K,1,Res).

blocking_nr_iseq(inf,R) :- !, R=inf.

blocking_nr_iseq(inf_overflow,R) :- !, R=inf_overflow.

blocking_nr_iseq(X,R) :- X<0,!, add_error(blocking_nr_iseq,'Negative arg: ',blocking_nr_iseq(X,R)),R=0.

blocking_nr_iseq(X,R) :- X>500,!, set_inf_due_to_overflow(R).

blocking_nr_iseq(A,Res) :- nr_iseq(A,Res). % , print(nr_iseq(A,Res)),nl.

blocking_nr_iseq1(inf,R) :- !, R=inf.

blocking_nr_iseq1(inf_overflow,R) :- !, R=inf_overflow.

blocking_nr_iseq1(A,Res1) :- blocking_nr_iseq(A,Res) , safe_add_card(Res,-1,Res1). %, print(nr_iseq1(A,Res1)),nl.

choose_nk(N,K,Res) :- (K=0;K=N),!,Res=1.

choose_nk(N,K,Res) :- K > N/2,!, KN is N-K, choose_nk2(N,KN,Res).

choose_nk(N,K,Res) :- choose_nk2(N,K,Res).

choose_nk2(N,K,Res) :- blocking_factorial_k(N,K,NK), blocking_factorial(K,KF),
    safe_div(NK,KF,Res).

fact(0,Acc,Res) :- !,Res=Acc.

fact(N,Acc,Res) :- (is_inf_or_overflow_card(Acc) -> Res=Acc
    ; safe_mul(N,Acc,NAcc), N1 is N-1, fact(N1,NAcc,Res)).

fact_k(0,_,Acc,Res) :- !, Res=Acc.

fact_k(_,K,Acc,Res) :- K<1,!,Res=Acc.

fact_k(N,K,Acc,Res) :- (is_inf_or_overflow_card(Acc) -> Res=Acc
    ; safe_mul(N,Acc,NAcc), N1 is N-1, K1 is K-1, fact_k(N1,K1,NAcc,Res)).

infinite_pown(Base,Exp) :- Exp > 1023, !, Base >= 2.

infinite_pown(Base,Exp) :- Exp > 646, !, Base >= 3. % was not really necessary when using overflow_float_pown

infinite_pown(Base,Exp) :- Exp > 511, !, Base >= 4.

infinite_pown(Base,Exp) :- Exp > 441, !, Base >= 5.

is_finite_card(Card) :- number(Card).

is_inf_or_overflow_card(inf).

is_inf_or_overflow_card(inf_overflow).

is_overflowcheck(Var,Expr) :-
    (Expr=inf -> Var=inf
    ; catch(Var is Expr, error(_,_),
    set_inf_due_to_overflow(Var)) % optionally add enumeration warning in scope
).

nr_iseq(0,Res) :- !,Res=1.

nr_iseq(N,Res) :- N1 is N-1, nr_iseq(N1,N1Res),
    safe_mul(N,N1Res,NAcc), safe_add_card(NAcc,1,Res).

partial_bijection_card(_X,0,R) :- !, R=1. % the empty set is a solution

partial_bijection_card(inf,X,R) :- !,
    print_inf_warning(X,'>+>>'), % we could have : INTEGER >+>> POW(INTEGER); TO DO: use omega(inf) for POW ?
    R=inf. % we know _X>0

partial_bijection_card(DomCard,RanCard,Res) :-
    infless(DomCard,RanCard),!,Res=0. % -> no way to cover all elements in range

partial_bijection_card(DomCard,RanCard,XCard) :-
    choose_nk(DomCard,RanCard,CNK), % ways to choose domain of size RanCard
    blocking_factorial(RanCard,Card),
    safe_mul(CNK,Card,XCard).

partial_injection_card(Dom,Ran,R) :- (Dom=0;Ran=0),!, R=1. % only one solution: empty function

partial_injection_card(Dom,1,R) :- !, (Dom=inf -> R=inf ; R is Dom+1). % empty function + for every domain element one function

partial_injection_card(inf,inf,Card) :- !, print_inf_warning(inf,'>+>'), Card=inf.

partial_injection_card(inf_overflow,inf_overflow,Card) :- !, print_inf_overflow_warning('>+>'), Card=inf_overflow.

partial_injection_card(Dom,Ran,R) :- (Dom=inf;Ran=inf),!, R=inf.

partial_injection_card(Dom,Ran,R) :- Dom>1000,Ran>1000,!, set_inf_due_to_overflow(R). % TO DO: refine this

partial_injection_card(DCard,RCard,Card) :-
    pinj_card(1,DCard,RCard,1,Card).

partial_surjection_card(_X,0,R) :- !, R=1. % the empty set is a solution

partial_surjection_card(inf,X,R) :- !,print_inf_warning(X,'+->>'),R=inf. % we know _X>0

partial_surjection_card(DomCard,RanCard,R) :-
    infless(DomCard,RanCard), !, R=0. % -> no way to cover all elements in range

partial_surjection_card(inf_overflow,_,R) :- !, R=inf_overflow.

partial_surjection_card(A,B,Res) :- tsurjcard(A,1,B,Res). % 1 because we can choose to leave the function undefined

pinj_card(I,M,N,Acc,Res) :- (I>M ; I>N ; Acc=inf),!, Res=Acc.

pinj_card(I,M,N,Acc,Res) :-
    choose_nk(M,I,MI), % ways to choose domain of size I
    blocking_factorial_k(N,I,NI), % ways to map the domain of size I to N
    safe_mul(MI,NI,MINI), safe_add_card(MINI,Acc,NewAcc),
    I1 is I+1, pinj_card(I1,M,N,NewAcc,Res).

print_inf_overflow_warning(FUN) :- !, print('### WARNING: Assuming '),
    print(FUN), print(' exists for two very large sets sets'),nl.

print_inf_warning(inf,FUN) :- !, print('### WARNING: Assuming '),
    print(FUN), print(' exists for two infinite sets'),nl.

print_inf_warning(_,_).

safe_add_card(inf,_,R) :- !, R=inf.

safe_add_card(_,inf,R) :- !, R=inf.

safe_add_card(inf_overflow,_,R) :- !, R=inf_overflow.

safe_add_card(_,inf_overflow,R) :- !, R=inf_overflow.

safe_add_card(X,Y,R) :- is_overflowcheck(R,X+Y).

safe_div(X,0,R) :- print(div_by_zero(X,0,R)),nl, !, R=inf.

safe_div(inf,K,R) :-
    (number(K) -> true ; K=inf_overflow -> true ; print(safe_div(inf,K,R)),nl), !, R=inf.

safe_div(_N,inf,R) :- !, R=0.

safe_div(inf_overflow,K,R) :-
    (number(K) -> true ; print(safe_div(inf_overflow,K,R)),nl), !, R=inf_overflow.

safe_div(_N,inf_overflow,R) :- !, R=0.

safe_div(X,Y,Z) :- Z is X//Y.

safe_minus(_,inf,R) :- !, print('### Warning: cannot compute X - inf'),nl, R=0.

safe_minus(inf,_,R) :- !, R=inf.

safe_minus(_,inf_overflow,R) :- !, print('### Warning: cannot compute X - inf_overflow'),nl, R=0.

safe_minus(inf_overflow,_,R) :- !, R=inf.

safe_minus(X,Y,R) :- R is X-Y.

safe_mul(0,_,R) :- !, R=0. % true for cartesian product: card({}*INTEGER)=0

safe_mul(_,0,R) :- !, R=0. % ditto

safe_mul(inf,_,R) :- !, R=inf.

safe_mul(_,inf,R) :- !, R=inf.

safe_mul(inf_overflow,_,R) :- !, R=inf_overflow.

safe_mul(_,inf_overflow,R) :- !, R=inf_overflow.

safe_mul(X,Y,R) :- is_overflowcheck(R,X*Y).

safe_pow2(Exp,Res) :-
    (Exp==inf -> Res=inf
    ; Exp==inf_overflow -> Res=inf_overflow
    ; Exp>1023 /* the limit where SICStus 4.2.1 reported inf; 4.2.3 goes further but uses a huge amount of memory */
    -> set_inf_due_to_overflow(Res)
    ; Res is 2^Exp % ^ integer exponentiation operator new in SICStus 4.3
).

safe_pown(Base,Exp,Res) :-
    ( Base=inf -> (Exp=0 -> Res=1 ; Res=Base)
    ; Exp=inf -> (Base=0 -> Res=0 ; Base=1 -> Res=1 ; Res=Exp)
    ; Base=inf_overflow -> (Exp=0 -> Res=1 ; Res=Base)
    ; Exp=inf_overflow -> (Base=0 -> Res=0 ; Base=1 -> Res=1 ; Res=Exp)
    ; infinite_pown(Base,Exp) /* SICStus 4.2.1 reported inf; 4.2.3 goes further but uses a huge amount of memory */
    -> set_inf_due_to_overflow(Res)
    ; Res is Base ^ Exp % ^ integer exponentiation operator new in SICStus 4.3
).

set_inf_due_to_overflow(Res) :- debug_println(9,'** OVERFLOW (cardinality)**'),Res=inf_overflow.

total_bijection_card(inf,inf,Card) :- !, print_inf_warning(inf,'>->>'), Card=inf.

total_bijection_card(inf_overflow,inf_overflow,Card) :- !, print_inf_overflow_warning('>->>'), Card=inf_overflow.

total_bijection_card(DCard,RCard,Card) :- DCard \= RCard,!,Card=0.

total_bijection_card(RCard,RCard,Card) :- blocking_factorial(RCard,Card).

total_relation_card(0,_RanC,Card) :- !, Card=1. % empty set is a solution

total_relation_card(_DomC,0,Card) :- !, Card=0. % no element to choose from in the range

total_relation_card(inf,RanC,Card) :- !, (RanC=1 -> Card=1 ; Card=inf).

total_relation_card(_,inf,Card) :- !, Card=inf.

total_relation_card(DomC,RanC,Card) :- safe_pow2(RanC,SubRan),
    safe_minus(SubRan,1,S1), % as we have a total relation we cannot choose empty set
    safe_pown(S1,DomC,Card).

total_surjection_card(0,Range,R) :- !,(Range=0 -> R=1 % the empty set is a solution
    ; R=0). % no solution

total_surjection_card(_X,0,R) :- !, R=0. % as _X>0 there is no way to construct a total function

total_surjection_card(_X,1,R) :- !, R=1. % we only have one choice for every element of _X

total_surjection_card(inf,X,R) :- !,print_inf_warning(X,'-->>'),R=inf. % we know _X>0

total_surjection_card(DomCard,RanCard,R) :-
    infless(DomCard,RanCard), !, R=0. % -> no way to cover all elements in range, applicable if RanCard=inf

total_surjection_card(inf_overflow,_,R) :- !, R=inf_overflow.

total_surjection_card(A,B,Res) :- tsurjcard(A,0,B,Res).

tsurjcard(Rem,_AlreadyUsed,StillToBeUsed,Res) :- Rem<StillToBeUsed,!,Res=0. % no solution

tsurjcard(0,_AlreadyUsed,_StillToBeUsed,Res) :- !, Res=1. % we have finished

tsurjcard(Rem,AlreadyUsed,StillToBeUsed,Res) :-
    R1 is Rem-1, A1 is AlreadyUsed+1, S1 is StillToBeUsed-1,
    (AlreadyUsed=0 -> ResA=0 ; tsurjcard(R1,AlreadyUsed,StillToBeUsed,ResA)),
    (StillToBeUsed=0 -> ResB =0 ; tsurjcard(R1,A1,S1,ResB)),
    Res is AlreadyUsed*ResA+StillToBeUsed*ResB.