kernel_objects.pl

card_leq(Set,Card) :-
    ((nonvar(Set),is_custom_explicit_set(Set,card_leq))
    -> explicit_set_cardinality(Set,CCard), leq_int_peano(CCard,Card)
    ; card_leq2(Set,Card) ).

card_leq2([],_C).

card_leq2([_|T],s(C)) :- card_leq2(T,C). %when(nonvar(T),card_leq2(T,C)).

card_leq2(avl_set(A),C) :- card_leq(avl_set(A),C).

card_leq2(closure(P,T,B),C) :- card_leq(closure(P,T,B),C).

card_leq2(global_set(A),C) :- card_leq(global_set(A),C).

card_leq2(freetype(A),C) :- card_leq(freetype(A),C).

check_finite_card(CardValue,C,Set,WF) :- % print(check_finite_card(CardValue,C)),nl,
    (CardValue==inf -> add_wd_error('card applied to infinite (or very large) set: ',b(value(Set),any,[]),WF)
    % if CardValue not yet instantiated we may want to delay the unification below for stronger wd-checking:
    % i.e., if find_abort_values preference is true
    ; C=CardValue).

finite_cardinality_as_int(Set,int(Card),WF) :- % print(card(Set)),nl,trace,
    % if Card is already known we could give it to cardinality_as_int1 straightaway; but we would not detect certain WD-problems
    %(number(Card) -> CardValue=Card ; true),
    cardinality_as_int1(Set,Card,CardValue,WF), % print(card_value(CardValue,Card)),nl,
    % clpfd_domain(CardValue,Low,Up), print(card(CardValue,Low,Up,Set)),nl,trace,
    (clpfd_max_bounded(CardValue)
    -> Card=CardValue % we cannot have an infinite return value for CardValue
    ; (nonvar(Set),is_interval_closure(Set,_,_)) -> % we must have a finite interval; no need to guard against inf
    Card=CardValue % TO DO: let cardinality_as_int1 return a flag whether set can be infinite
    % example i=2..x & card(i):10..2122110 & x > 2121000; see test 1625
    ; check_finite_card(CardValue,Card,Set,WF) % check that we have obtained a finite value; only propagate then
% TO DO: maybe detect a few more cases where infinite return values are not possible; e.g., based on type
% indeed: check_finite_card prevents propagation of CLPFD information
).

gen_strict_subsets(T,[_H2|T2],WF) :- gen_subsets(T,T2,WF).

gen_strict_subsets(SubSet,[H2|T2],WF) :-
    equal_object_wf([H2|T],SubSet,gen_strict_subsets,WF),
    gen_strict_subsets(T,T2,WF).

leq_int_peano(0,_).

leq_int_peano(inf,_) :- !,fail.

leq_int_peano(X,s(C)) :- X>0, X1 is X-1, leq_int_peano(X1,C).

remove_element(X,Set,Res) :- equal_cons(Set,X,Res).

strict_subset_of_aux_block(Set1,Set2,WF,_LWF) :-
    var(Set1),ground(Set2),
    !, % DO WE STILL NEED THIS VERSION ????
    %non_free(Set1), % as we used to force order, now we use equal_object_wf and no longer need non_free marking ?
    expand_custom_set_to_list_wf(Set2,ESet2,_,strict_subset_of_wf,WF),
    %print(gen_strict(Set1,ESet2)),nl,
    gen_strict_subsets(Set1,ESet2,WF).