bounds_analysis

add_outer_bound_info(bound_id_info(ID,Type,Bounds),bound_internal_info(ID,Type,InternalType)) :-
    convert_bounds_to_internal(Bounds,InternalType).

add_typed_id(TID,bound_id_info(ID,Type,Bounds),env(Env,Flags),env(NewEnv,Flags)) :- def_get_texpr_id(TID,ID),
    get_texpr_type(TID,Type),
    NewEnv = [bound_internal_info(ID,Type,Fresh)|Env],
    (bounds_type(Type,Fresh,_)
    -> compute_bound_info(ID,Type,Fresh,Bounds,Flags)
    ; format(user_output,'Ignoring identifier ~w in analysis~n',[ID]),
    Fresh=Type, Bounds=Type),
    label_id(ID,Type,Fresh,Flags).

add_typed_ids([],[]) --> [].

add_typed_ids([TID|T],[BoundsInfo|TB]) --> add_typed_id(TID,BoundsInfo), add_typed_ids(T,TB).

apply_binary_op(Op,bint(Res),bint(A),bint(B)) :- !, RHS =.. [Op,A,B],
    if(call('#=',Res,RHS),true, % TODO: catch overflows
    (format(user_output,'Inconsistent ~w #= (~w ~w ~w) constraint!',[Res, A,Op,B]),fail)).

apply_binary_op(ClpfdOp,Bounds,BoundsA,BoundsB) :-
    add_internal_error('Illegal call: ',apply_binary_op(ClpfdOp,Bounds,BoundsA,BoundsB)), fail.

apply_binary_pred(Pred,bint(A),bint(B)) :- !,
    if(call(Pred,A,B),true, % TODO: catch overflows
    (format(user_output,'Inconsistent ~w ~w ~w constraint!~n',[A,Pred,B]),fail)).

apply_binary_pred(ClpfdOp,BoundsA,BoundsB) :-
    add_internal_error('Illegal call: ',apply_binary_pred(ClpfdOp,BoundsA,BoundsB)), fail.

bounds_type(integer,bint(_),1).

bounds_type(string,bint(_),1).

bounds_type(set(integer),binterval(_,_,NonEmpty),NonEmpty).

bounds_type(set(string),binterval(_,_,NonEmpty),NonEmpty).

bounds_type(couple(A,B),bcouple(BA,BB),1) :-
    bounds_of_pair(A,B,BA,BB,_). % at least one part requires bounds

bounds_type(set(couple(A,B)),bcart(BA,BB,NonEmpty),NonEmpty) :-
    bounds_of_pair(set(A),set(B),BA,BB,NonEmpty).

compute_bound_info(ID,Type,Fresh,Bounds,_) :-
    get_bounds(Fresh,Type,Bounds),
    format(user_output,'Computed bounds ~w : ~w --> ~w~n',[ID,Type,Bounds]).

convert_bounds_to_internal(set(integer_in_range(From,To,_)),binterval(From2,To2,_NonEmpty)) :- !,
    (number(From) -> From2=From ; true), (number(To) -> To2=To ; true).

convert_bounds_to_internal(set(couple(A,B)),BCart) :- !,
    convert_bounds_to_internal(set(A),BA),
    convert_bounds_to_internal(set(B),BB),
    Dummy = b(empty_set,any,[]),
    construct_bcart(Dummy,Dummy,BA,BB,BCart).

convert_bounds_to_internal(X,X).

create_dummy_value(binterval(A,_,_),bint(DA)) :- !, (var(A),fd_min(A,Min),number(Min) -> DA=Min ; DA=0).

create_dummy_value(bcart(A,B,_),bcouple(DA,DB)) :- !, create_dummy_value(A,DA), create_dummy_value(B,DB).

create_dummy_value(T,T) :- finite_type(T).

eq_bounds(BoundsInfo,BoundsInfo2) :- format(user_output,'eq bounds: ~w = ~w~n',[BoundsInfo,BoundsInfo2]),
    if(eq_bounds2(BoundsInfo,BoundsInfo2),true,
    (format(user_output,'Inconsistent ~w = ~w constraint!~n',[BoundsInfo,BoundsInfo2]),fail)).

eq_bounds2(binterval(A,B,NonEmpty),binterval(A2,B2,NonEmpty2)) :- !,
    NonEmpty=NonEmpty2,
    eq_interval(NonEmpty,A,B,A2,B2).

eq_bounds2(bint(A),bint(B)) :- !, A=B.

eq_bounds2(bcouple(A1,A2),bcouple(B1,B2)) :- !, eq_bounds2(A1,B1), eq_bounds2(A2,B2).

eq_bounds2(bcart(A1,A2,NonEmptyA),bcart(B1,B2,NonEmptyB)) :- !,
    NonEmptyA=NonEmptyB,
    eq_cart(NonEmptyA,A1,B1,A2,B2).

eq_bounds2(_,_).

eq_cart(0,_,_,_,_). % both cartesian products empty

eq_cart(1,A1,B1,A2,B2) :- eq_bounds2(A1,B1), eq_bounds2(A2,B2).

eq_interval(0,_,_,_,_). % both empty

eq_interval(1,A,B,X,Y) :- (A,B) = (X,Y).

eq_list(0,_,_). % both cartesian products empty

eq_list(1,A,B) :- subset_list(A,B), subset_list(B,A).

finite_type(boolean).

finite_type(global(_GS)).

finite_type(set(X)) :- finite_type(X).

finite_type(couple(X,Y)) :- finite_type(X), finite_type(Y).

force_non_empty(non_empty,binterval(_,_,NonEmpty)) :- !, NonEmpty=1.

force_non_empty(_,_).

get_bounds(bint(X),Type,integer_in_range(Min,Max,Type)) :- !, fd_min(X,Min), fd_max(X,Max).

get_bounds(binterval(X,Y,NonEmpty),set(Type),set(integer_in_range(Min,Max,Type))) :- !,
    ( NonEmpty == 0 -> Min=1, Max=0
    ; NonEmpty == 1 -> fd_min(X,Min), fd_max(Y,Max)
    ; get_non_empty_interval_bounds(X,Y,NonEmpty,Min,Max) % we do not know if set empty or not
).

get_bounds(bcouple(A,B),couple(TA,TB),couple(BA,BB)) :- !, get_bounds(A,TA,BA), get_bounds(B,TB,BB).

get_bounds(bcart(A,B,NonEmpty),set(couple(TA,TB)),set(couple(BA,BB))) :- !,
    ( NonEmpty == 0 -> get_bounds(A,set(TA),set(BA)), get_bounds(B,set(TB),set(BB)) % we could return empty_set for BA/BB
    ; NonEmpty == 1 -> get_bounds(A,set(TA),set(BA)), get_bounds(B,set(TB),set(BB))
    ; get_non_empty_cart_bounds(A,B,TA,TB,NonEmpty,BA,BB) % we do not know if cartesian product empty or not
).

get_bounds(B,_,R) :- finite_type(B),!, R=B.

get_bounds(B,Type,R) :- format(user_output,'Unknown bound: ~w (type ~w)~n',[B,Type]), R=B.

get_non_empty_cart_bounds(A,B,TA,TB,NonEmpty,_,_) :-
    bb_put(bounds_analysis_cart,(empty_set,empty_set)), % if propagation fails the set must be empty
    (NonEmpty=1 % force non-empty and check to see in which range the values must be
    -> get_bounds(A,set(TA),set(BA)), get_bounds(B,set(TB),set(BB)),
    bb_put(bounds_analysis_cart,(BA,BB))
    ; format(user_output,'Bounds cartesian product cannot be non-empty~n',[])
    ),
    fail.

get_non_empty_cart_bounds(_,_,_,_,_,BA,BB) :- bb_get(bounds_analysis_cart,(BA,BB)).

get_non_empty_flag(binterval(_,_,NE),R) :- !, R=NE.

get_non_empty_flag(bcart(_,_,NE),R) :- !, R=NE.

get_non_empty_flag(Expr,Bounds,NonEmpty) :-
    (definitely_not_empty_set(Expr) -> NonEmpty=1
    , format(user_output,'Def non-empty: ~w~n',[Expr])
    ; get_non_empty_flag(Bounds,NonEmpty)).

get_non_empty_interval_bounds(X,Y,NonEmpty,_,_) :-
    bb_put(bounds_analysis_min_max,(1,0)), % if propagation fails the set must be empty
    (NonEmpty=1 % force non-empty and check to see in which range the values must be
    -> fd_min(X,Min2), fd_max(Y,Max2),
    bb_put(bounds_analysis_min_max,(Min2,Max2))
    ; format(user_output,'Bounds interval cannot be non-empty~n',[])
    ),
    fail.

get_non_empty_interval_bounds(_,_,_,Min,Max) :- bb_get(bounds_analysis_min_max,(Min,Max)).

imply_block(1,1).

imply_block(0,_).

imply_non_empty(Bounds,NonEmptyFlag) :- get_non_empty_flag(Bounds,NE),
    imply_block(NE,NonEmptyFlag).

infer_bounds(Paras,Pred,Res) :- infer_bounds(Paras,Pred,[],Res).

infer_bounds(Paras,Pred,Options,_Res) :-
    new_env(Env,Options),
    format(user_output,'Inferring bounds for: ~w~n',[Paras]),
    bb_put(infer_bounds_result,contradiction_found),
    (add_typed_ids(Paras,LocalBoundsInfo,Env,Env2),
    infer_pred_bounds(Pred,Env2)
    -> portray_env(Env2),
    (label_env(Env2,Options)
    -> bb_put(infer_bounds_result,LocalBoundsInfo)
    ; format(user_output,'No consistent labelled solution exists, predicate unsatisfiable~n',[])
    )
    ; format(user_output,'No consistent solution exists, predicate unsatisfiable~n',[])
    ),
    fail. % to avoid pending co-routines / CLPFD variables we fail and recover the result with bb_get:

infer_bounds(_,_,_,Res) :- bb_get(infer_bounds_result,Res).

infer_pred_bounds(b(Pred,pred,_Infos),Env) :- !,
    % format(user_output,' pred --> ~w~n',[Pred]),
    infer_pred_bounds(Pred,Env).

infer_pred_bounds(conjunct(A,B),Env) :- !,
    infer_pred_bounds(A,Env),
    infer_pred_bounds(B,Env).

infer_pred_bounds(truth,_) :- !.

infer_pred_bounds(member(A,B),Env) :-
    infer_scalar_bounds(A,Env,SetBoundsA),
    infer_set_bounds(B,Env,SetBoundsB), !,
    mem_bounds(SetBoundsA,SetBoundsB).

infer_pred_bounds(SubsetAB,Env) :- is_subset(SubsetAB,A,B,EmptyA,EmptyB),
    infer_set_bounds(A,Env,SetBoundsA),
    infer_set_bounds(B,Env,SetBoundsB), !,
    force_non_empty(EmptyA,SetBoundsA),
    force_non_empty(EmptyB,SetBoundsB),
    subset_bounds(SetBoundsA,SetBoundsB).

infer_pred_bounds(equal(A,B),Env) :- is_scalar(A),
    infer_scalar_bounds(A,Env,ScBoundsA),
    infer_scalar_bounds(B,Env,ScBoundsB), !,
    eq_bounds(ScBoundsA,ScBoundsB).

infer_pred_bounds(equal(A,B),Env) :- is_set(A),
    infer_set_bounds(A,Env,SetBoundsA),
    infer_set_bounds(B,Env,SetBoundsB), !,
    eq_bounds(SetBoundsA,SetBoundsB).

infer_pred_bounds(BOP,Env) :-
    scalar_binary_pred(BOP,A,B,ClpfdOp),
    infer_scalar_bounds(A,Env,BoundsA),
    infer_scalar_bounds(B,Env,BoundsB), !,
    apply_binary_pred(ClpfdOp,BoundsA,BoundsB).

infer_pred_bounds(Uncov,_Env) :- write(user_output,uncovered_pred(Uncov)), nl(user_output).

infer_scalar_bounds(b(E,T,_Infos),Env,Bounds) :- !,
    (finite_type(T) -> Bounds = T % we could try and infer bounds for fd(_,_) global set values
    ; infer_scalar_bounds2(E,T,Env,Bounds)).

infer_scalar_bounds2(integer(A),_,_Env,Bounds) :- !, Bounds = bint(A).

infer_scalar_bounds2(string(A),_,_Env,Bounds) :- !, get_string_nr(A,Nr),Bounds = bint(Nr).

infer_scalar_bounds2(identifier(A),Type,Env,Bounds) :- !, lookup_id_bounds(A,Env,Type,Bounds).

infer_scalar_bounds2(couple(A,B),couple(_TA,_TB),Env,bcouple(BA,BB)) :- !,
    infer_scalar_bounds(A,Env,BA), % TODO: treat if one of them fails / is finite
    infer_scalar_bounds(B,Env,BB).

infer_scalar_bounds2(function(Rel,_Arg),Type,Env,Bounds) :- !,
    infer_set_bounds(range(Rel),set(Type),Env,RanBounds), % we ignore Arg
    %convert_set_bounds_to_scalar(RanBounds,Bounds). % we could use this if TRY_FIND_ABORT is TRUE
    if(mem_bounds(Bounds,RanBounds),
    true,
    create_dummy_value(RanBounds,Bounds)). % empty range probably meaning WD error; just return a concrete dummy value

infer_scalar_bounds2(BOP,_,Env,Bounds) :-
    scalar_binary_op(BOP,A,B,ClpfdOp), !,
    infer_scalar_bounds(A,Env,BoundsA),
    infer_scalar_bounds(B,Env,BoundsB),
    apply_binary_op(ClpfdOp,Bounds,BoundsA,BoundsB).

infer_scalar_bounds2(BOP,_,_,_) :- write(user_output,uncov_scalar(BOP)),nl(user_output),fail.

infer_set_bounds(b(E,Type,_Infos),Env,Bounds) :- !,
    (finite_type(Type) -> Bounds = Type % we could try and infer bounds for fd(_,_) global set values
    ; infer_set_bounds(E,Type,Env,Bounds)).

infer_set_bounds(empty_set,set(integer),_,Bounds) :- !, Bounds = binterval(1,0,0).

infer_set_bounds(integer_set('NATURAL'),set(integer),_,Bounds) :- !, init_binterval(0,_,Bounds,1).

infer_set_bounds(integer_set('NATURAL1'),set(integer),_,Bounds) :- !, init_binterval(1,_,Bounds,1).

infer_set_bounds(value(AVL),set(integer),_Env,Bounds) :- nonvar(AVL), AVL=avl_set(A), !,
    avl_min(A,int(Min)), %min_of_explicit_set_wf(Val,int(Min),no_wf_available),
    avl_max(A,int(Max)), Bounds = binterval(Min,Max,1).

infer_set_bounds(value(AVL),set(string),_Env,Bounds) :- nonvar(AVL), AVL=avl_set(A), !,
    findall(Nr,(avl_member(string(S),A), get_string_nr(S,Nr)),Nrs),
    min_member(Min,Nrs), max_member(Max,Nrs), Bounds = binterval(Min,Max,1).

infer_set_bounds(interval(A,B),_,Env,Bounds) :- !,
    infer_scalar_bounds(A,Env,bint(BA)),
    infer_scalar_bounds(B,Env,bint(BB)),
    init_binterval(BA,BB,Bounds,_).

infer_set_bounds(intersection(A,B),_,Env,Bounds) :- !,
    infer_set_bounds(A,Env,BoundsA),
    infer_set_bounds(B,Env,BoundsB), % TODO: treat if one of the two calls fails
    intersect_bounds(BoundsA,BoundsB,Bounds).

infer_set_bounds(union(A,B),_,Env,Bounds) :- !,
    infer_set_bounds(A,Env,BoundsA),
    infer_set_bounds(B,Env,BoundsB),
    union_bounds(BoundsA,BoundsB,Bounds).

infer_set_bounds(set_extension(List),_,Env,Bounds) :- !,
    (List = [A], infer_scalar_bounds(A,Env,bint(BA))
    -> Bounds = binterval(BA,BA,1)
    ; maplist(infer_set_ext_el(Env,Bounds),List)
% TODO: use union code instead? we loose info that these are all the elements of the set
).

infer_set_bounds(identifier(A),Type,Env,Bounds) :- !,
    lookup_id_bounds(A,Env,Type,Bounds).

infer_set_bounds(cartesian_product(A,B),_,Env,Bounds) :- !,
    infer_set_bounds(A,Env,BoundsA),
    infer_set_bounds(B,Env,BoundsB),
    construct_bcart(A,B,BoundsA,BoundsB,Bounds).

infer_set_bounds(domain(A),_,Env,DomBounds) :- !,
    infer_set_bounds(A,Env,bcart(DomBounds,_,NE)),
    imply_non_empty(DomBounds,NE). % if domain is non-empty, then full relation must be non-empty

infer_set_bounds(range(A),_,Env,RanBounds) :- !,
    infer_set_bounds(A,Env,bcart(_,RanBounds,NE)),
    imply_non_empty(RanBounds,NE). % if range is non-empty, then full relation must be non-empty

infer_set_bounds(image(Rel,_Set),Type,Env,RanBounds) :- !,
    infer_set_bounds(range(Rel),Type,Env,RanBounds). % we ignore Set

infer_set_ext_el(Env,Bounds,A) :-
    (infer_scalar_bounds(A,Env,BoundsA)
    -> mem_bounds(BoundsA,Bounds)
    ; format(user_output,'Cannot infer bounds for set-ext element:~w~n',[A])
).

is_pow(b(P,_,_),B,EmptyA,EmptyB) :- is_pow(P,B,EmptyA,EmptyB).

is_pow(pow_subset(B),B, can_be_empty,can_be_empty).

is_pow(pow1_subset(B),B,non_empty,non_empty).

is_pow(fin_subset(B),B, can_be_empty,can_be_empty).

is_pow(fin1_subset(B),B,non_empty,non_empty).

is_rel_fun(b(P,_,_),Dom,Ran) :- is_rel_fun(P,Dom,Ran).

is_rel_fun(relations(A,B),A,B).

is_rel_fun(total_relation(A,B),A,B).

is_rel_fun(partial_function(A,B),A,B).

is_rel_fun(partial_injection(A,B),A,B).

is_rel_fun(partial_surjection(A,B),A,B).

is_rel_fun(partial_bijection(A,B),A,B).

is_rel_fun(total_function(A,B),A,B).

is_rel_fun(total_injection(A,B),A,B).

is_rel_fun(total_surjection(A,B),A,B).

is_rel_fun(total_bijection(A,B),A,B).

is_rel_fun(perm(B),A,B) :- iset(A,'NATURAL1').

is_rel_fun(seq(B),A,B) :- iset(A,'NATURAL1').

is_rel_fun(iseq(B),A,B) :- iset(A,'NATURAL1').

is_rel_fun(seq1(B),A,B) :- iset(A,'NATURAL1').

is_rel_fun(iseq1(B),A,B) :- iset(A,'NATURAL1').

is_scalar(A) :- get_texpr_type(A,integer).

is_scalar(A) :- get_texpr_type(A,string).

is_scalar(A) :- get_texpr_type(A,couple(_,_)).

is_set(A) :- get_texpr_type(A,TA), is_set_type(TA,_).

is_subset(subset(A,B),A,B, can_be_empty,can_be_empty).

is_subset(subset_strict(A,B),A,B,can_be_empty,non_empty).

is_subset(member(A,PB),A,B,EmptyA,EmptyB) :- is_pow(PB,B,EmptyA,EmptyB).

is_subset(member(A,RelFun),A,Cart,can_be_empty,can_be_empty) :- is_rel_fun(RelFun,Dom,Ran),
    create_cartesian_product(Dom,Ran,Cart).

iset(b(integer_set(SET),set(integer),[]),SET).

label_bounds(_,no_labeling) :- !.

label_bounds(bint(X),_) :- !, label_fd_var(X).

label_bounds(binterval(X,Y,Empty),_) :- !, (Empty=0 ; Empty=1), label_fd_var(X), label_fd_var(Y).

label_bounds(bcouple(X,Y),F) :- !, label_bounds(X,F), label_bounds(Y,F).

label_bounds(bcart(X,Y,Empty),F) :- !, (Empty=0 ; Empty=1), label_bounds(X,F), label_bounds(Y,F).

label_bounds(Term,_) :- ground(Term),finite_type(Term),!.

label_bounds(Term,_) :- add_internal_error('Unknown bounds info to label:', label_bounds(Term)).

label_env(env(_,Flags),Options) :- !,Flags=copy_bounds(F2),
    (member(label,Options) -> F2=label_now ; F2=no_labeling).

label_env(E,_) :- add_internal_error('Illegal env: ', label_env(E)).

label_fd_var(X) :- fd_size(X,Sz), (number(Sz) -> indomain(X) ; true).

label_id(_ID,_Type,Fresh,copy_bounds(Flag)) :- %format(user_output,'Labeling ~w : ~w~n',[ID,Fresh]),
    label_bounds(Fresh,Flag).

lookup_id_bounds(ID,env(Env,_),Type,BoundsInfo) :-
    (member(bound_internal_info(ID,Type,StoredBounds),Env)
    -> BoundsInfo=StoredBounds
    ; format(user_output,'Could not find identifier ~w !!~n',[ID]),
    bounds_type(Type,BoundsInfo,_)). % set up unconstrained bounds

mem_bounds(BoundsInfo,SetBounds) :- format(user_output,'member ~w ~w~n',[BoundsInfo,SetBounds]),
    if(mem_bounds2(BoundsInfo,SetBounds),true,
    (format(user_output,'Inconsistent ~w : ~w constraint!~n',[BoundsInfo,SetBounds]),fail)).

mem_bounds2(bcouple(X,Y),bcart(BoundsA,BoundsB,NonEmpty)) :- !,
    NonEmpty = 1,
    mem_bounds2(X,BoundsA), mem_bounds2(Y,BoundsB).

mem_bounds2(A,B) :- format(user_output,'Uncovered mem_bounds ~w : ~w~n',[A,B]).

new_env(env(E,_),Opts) :-
    (member(outer_bounds(OB),Opts)
    -> maplist(add_outer_bound_info,OB,E)
    % outer bounds are already ground and need no labeling; they provide bounds for outer variables
    ; member(open,Opts) -> true ; E=[]).

portray_bounds(bint(X)) :- !, portray_int(X).

portray_bounds(binterval(X,Y,_E)) :- !,
    write(user_output,'('), portray_int(X), write(user_output,' .. '), portray_int(Y), write(user_output,')').

portray_bounds(bcouple(X,Y)) :- !, portray_bounds(X), write(user_output,' , '), portray_bounds(Y).

portray_bounds(bcart(X,Y,_E)) :- !, portray_bounds(X), write(user_output,' * '), portray_bounds(Y).

portray_bounds(T) :- finite_type(T), !, write(user_output,T).

portray_bounds(U) :- write(user_output,'*** UNKNOWN '), write(user_output,U), write(user_output,' ***').

portray_env(env(NE,_)) :- portray_env2(NE).

portray_env2(X) :- var(X),!, write(user_output,' - ... '),nl(user_output).

portray_env2([]) :- !.

portray_env2([bound_internal_info(ID,Type,BoundsInfo)|TT]) :- !,
    format(user_output,' - ~w (~w) : ',[ID,Type]), portray_bounds(BoundsInfo), nl(user_output),
    portray_env2(TT).

portray_env2(E) :-
    format(user_output,' *** ILLEGAL ENV *** ~w~n',[E]).

portray_int(X) :- nonvar(X),!, write(user_output,X).

portray_int(X) :- fd_dom(X,Dom), write(user_output,Dom).

scalar_binary_op(add(A,B),A,B,'+').

scalar_binary_op(multiplication(A,B),A,B,'*').

scalar_binary_op(minus(A,B),A,B,'-').

scalar_binary_pred(less(A,B),A,B,'#<').

scalar_binary_pred(greater(A,B),A,B,'#>').

scalar_binary_pred(less_equal(A,B),A,B,'#=<').

scalar_binary_pred(greater_equal(A,B),A,B,'#>=').

subset_bounds(BoundsInfo,SetBounds) :- format(user_output,'subset_bounds ~w ~w~n',[BoundsInfo,SetBounds]),
    if(subset_bounds2(BoundsInfo,SetBounds),true,
    (format(user_output,'Inconsistent ~w <: ~w constraint!~n',[BoundsInfo,SetBounds]),fail)).

subset_bounds2(A,B) :- format(user_output,'Uncovered subset_bounds2 ~w : ~w~n',[A,B]).

subset_cart(_,_,0,_,_,_). % first set empty

subset_cart(X,Y,1,A,B,1) :- subset_bounds2(X,A), subset_bounds2(Y,B).

subset_interval(_,_,0,_,_,_). % first set empty

subset_list([],_).

subset_list([H|T],List2) :- member(H,List2), !, % will instantiate List2 if necessary
    subset_list(T,List2).