% version 1.0-1

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                %
%                     {log}                      %                                               
%                    library                     %                                            
%                      for                       %                                          
%               integer intervals                %
%                                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% S is not an integer interval
nint(S) :-
  integer(A) & A in S & integer(B) & B in S & A < N & N < B & N nin S
  or
  A in S & ninteger(A).

% Int is the interior of interval int(M,N)
interior(int(M,N),Int) :-
  M1 is M + 1 &
  N1 is N - 1 &
  Int = int(M1,N1).

% M is the minimum of set S
setmin(S,M) :-
  M in S &
  subset(S,int(M,_)).

% M is the maximum of set S
setmax(S,M) :-
  M in S &
  subset(S,int(_,M)).

% Maximum (Max) of lower bounds (Lb) of S w.r.t. N
% Minimum (Min) of upper bounds (Ub) of S w.r.t. N
% assumes:
%   S is a set of integers
%   N nin S
mnlb_mxub(S,N,Lb,Max,Ub,Min) :-
  un(Lb,Ub,S) & disj(Lb,Ub) &
  (Max < N &
   Max in Lb &
   subset(Lb,int(_,Max))
   or
   Lb = {}
  ) &
  (N < Min &
   Min in Ub &
   subset(Ub,int(Min,_))
   or
   Ub = {}
  ).
  
% snth_min(S,N,E)
% E is the N-th smallest element of set S
%
% snth_min({7,8,2,14},1,2)
% snth_min({7,8,2,14},2,7)
% snth_min({7,8,2,14},3,8)
% snth_min({7,8,2,14},4,14)
%
% assumes:
%   S is a set of integers
snth_min(S,N,E) :-
  un(Smin,Smax,S) & disj(Smin,Smax) &
  subset(S,int(Min,_)) &
  Min in Smin &
  E in Smin &
  E1 is E + 1 &
  size(Smin,N) &
  subset(Smin,int(Min,E)) &
  subset(Smax,int(E1,_)).

% snth_max(S,N,E)
% E is the N-th largest element of set S
%
% snth_max({7,8,2,14},1,14)
% snth_max({7,8,2,14},2,8)
% snth_max({7,8,2,14},3,7)
% snth_max({7,8,2,14},4,2)
%
% assumes:
%   S is a set of integers
snth_max(S,N,E) :-
  un(Smin,Smax,S) & disj(Smin,Smax) &
  subset(S,int(_,Max)) &
  Max in Smax &
  E in Smax &
  E1 is E - 1 &
  size(Smax,N) &
  subset(Smin,int(_,E1)) &
  subset(Smax,int(E,Max)).

% medians(S,Med1,Med2)
% (median is a value separating the higher half from 
% the lower half of a data sample; in this definition
% repetitions aren't considered)
% if S has an odd cardinality then Med1 = Med2 = median of S
% if S has an even cardinality then Med1 < Med2 and
% median of S is (Med1 + Med2) / 2
medians(S,Med1,Med2) :-
  S = {Med1,Med2 / S1} & 
  Med1 nin S1 & Med2 nin S1 & 
  un(R1,R2,S1) & 
  disj(R1,R2) &
  Med1 =< Med2 &
  Medi is Med1 - 1 &
  subset(R1,int(_,Medi)) &
  size(R1,K) &
  Meds is Med2 + 1 &
  subset(R2,int(Meds,_)) &
  size(R2,K).

% int_max_prop(S,M,N)
% int(M,N) is a proper maximal subinterval of S
int_max_prop(S,M,N) :-
  un(int(M,N),R,S) & 
  M < N & 
  disj(int(M,N),R) &
  M1 is M - 1 &
  M1 nin R &
  N1 is N + 1 &
  N1 nin R.

% lb_ub(S,Lb,Ub)
% Lb is the subset of S with the lowest elements
% Ub is the subset of S with the greatest elements
% Lb's cardinality is equal to Ub's
% if S has an odd cardinality, lb_ub fails
lb_ub(S,Lb,Ub) :-
  un(Lb,Ub,S) & 
  disj(Lb,Ub) &
  subset(Lb,int(_,M)) &
  size(Lb,K) &
  M < N &
  subset(Ub,int(N,_)) &
  size(Ub,K).