kodkod_integer_recalc

extract_max_card_id(b(identifier(_),_,Info),MaxCard) :-
    member(analysis(I),Info),
    member(interval:irange(A,B),I), % should we support other analysis infos ??
    number(A),number(B),
    !,
    MaxCard is B+1-A.

extract_max_card_id(b(_,Type,_),MaxCard) :- % use max card of type; maybe other identifiers have restricted cardinality
    max_type_cardinality(Type,MaxCard), number(MaxCard).

extract_min_max_card(b(E,_,_),Type,MinCard,MaxCard) :- extract_min_max_card2(E,MinCard,MaxCardE),
    ((max_type_cardinality(Type,CType), number(CType), CType < MaxCardE)
    -> MaxCard = CType
    ; MaxCard = MaxCardE).

extract_min_max_card2(comprehension_set(IDs,_), 0, Card) :-
    maplist(extract_max_card_id,IDs,Cards),
    simple_mul_list(Cards,1,Card).

extract_min_max_card2(set_extension(L), MinCard, MaxCard) :- length(L,MaxCard),
    (MaxCard>0 -> MinCard=1 ; MinCard=0). % should always be 1

extract_min_max_card2(sequence_extension(L), MinCard, MaxCard) :- length(L,MaxCard),
    (MaxCard>0 -> MinCard=1 ; MinCard=0). % should always be 1

extract_min_max_card2(empty_set,0,0).

extract_min_max_card2(empty_sequence,0,0).

get_interval_info(TExpr,I) :-
    get_texpr_info(TExpr,Info),
    memberchk(analysis(An),Info),
    memberchk(interval:I,An).

integer_recalc(TExpr,NTExpr) :-
    create_texpr(Expr,Type,Info,TExpr),
    create_texpr(NExpr,Type,NInfo,NTExpr),
    syntaxtransformation(Expr,Subs,_,NSubs,NExpr),
    maplist(integer_recalc,Subs,NSubs),
    (integer_recalc2(NExpr,Interval) -> safe_add_interval_info(Interval,Info,NInfo) ; Info=NInfo).

integer_recalc2(value(IV),irange(I,I)) :- nonvar(IV), IV=int(I), number(I).

integer_recalc2(integer(I),irange(I,I)).

integer_recalc2(add(A,B),C) :-
    get_interval_info(A,AI), get_interval_info(B,BI),
    interval_addition(AI,BI,C).

integer_recalc2(minus(A,B),C) :-
    get_interval_info(A,AI), get_interval_info(B,BI),
    interval_subtraction(AI,BI,C).

integer_recalc2(unary_minus(A),C) :-
    get_interval_info(A,AI),
    interval_negation(AI,C).

integer_recalc2(multiplication(A,B),C) :-
    get_interval_info(A,AI), get_interval_info(B,BI),
    interval_multiplication(AI,BI,C).

integer_recalc2(division(A,B),C) :-
    get_interval_info(A,AI), get_interval_info(B,BI),
    AI=irange(Am,AMNr),BI=irange(Bm,_BM),
    ( number(Bm), Bm>=0 -> C = AI
    ; number(Am),number(AMNr) ->
    M is max(abs(Am),abs(AMNr)),
    C = irange(-M,M)
    ;
    C = irange(-inf,inf)).

integer_recalc2(card(S),irange(MinCard,MaxCard)) :-
    % TODO[DP,2016-04-20]: This is a very pessimistic approach:
    % The cardinality is maximally as high as the type allows
    % Maybe an alternative approach would be to add a second infered information to each node,
    % the "guaranteed" integer interval which is independent of overflows. E.g. "card({a,b,c}) : 1..3"
    get_texpr_set_type(S,Type),
    % print(recalc(Type,S)),nl,
    ( extract_min_max_card(S,Type,C1,C2) -> (MinCard,MaxCard)=(C1,C2),
    debug_println(9,extract_max_card_for_kodkod(C1,C2))
    ; max_type_cardinality(Type,MaxCard) -> MinCard=0
    %; Card=64 % TO DO allow user to provide a custom upper bound ???
    ; MinCard=0, MaxCard = inf).

safe_add_interval_info(Interval,Info,[analysis([interval:Interval|AnRest])|InfoRest]) :-
    selectchk(analysis(A),Info,InfoRest),!,
    (selectchk(interval:_,A,AnRest) -> true ; AnRest=A).

safe_add_interval_info(Interval,Info,[analysis([interval:Interval])|Info]).

simple_mul_list([],A,A).

simple_mul_list([H|T],Acc,R) :- NA is Acc*H, simple_mul_list(T,NA,R).