%   File   : clpset.pl 
%   Author : Neng-Fa ZHOU
%   Last update : 10,2000
%   Version  : 1.1
%   Purpose: interpreter for set constraints
/* This file contains the primitives for specifying and solving integer set 
   constraints. A set-domain variable is represented as a term of the following 
   form:

    $set(Sp,Sa,Card,Value)

   where Sp is a finite-domain representing the set of possible values in the set 
   (upper bound),  Sa is a finite-domain representing the complement of the set of 
   values that are definitely allowed in the set (low bound), Card is a finite-domain 
   that constrains the cardinality of the set, and Value is the value  (in the form 
   of [...]) of the set variable.

   Special thanks to Joachim Schimpf who gave me some suggestions for improving the 
   performance while I worked with him on a set solver in Eclipse based on the same idea.
*/
/*  export:
    clpset_add(E,S): add E into the low bound of S
    clpset_card(S,C): the cardinality of S is C
    clpset_difference(X,Y,Z): Z = X - Y
    clpset_disjoint(X,Y): X /\ Y= {}
    clpset_domain(S): S is an integer set domain variable
    clpset_domain(S,L,U): S is an integer set domain variable over the universal set {L,...,U}.
    clpset_domain_var(S): S is an integer set domain variable
    clpset_inclusion(X,Y): X =< Y
    clpset_indomain(S): enumerate the values for the set variable S
    clpset_intersection(X,Y,Z): Z = X /\ Y
    clpset_is_in(E,S): E is included in the low bound of S
    clpset_is_out(E,S): E is not included in the upper bound of S
    clpset_remove(E,S): Remove E from the upper bound of S
    clpset_union(X,Y,Z): Z = X \/ Y
    clpset_unify(X,Y): X and Y are the same set
    clpset_value(S,V): the value part of set variable S is V 
    clpset_write(T): write term T with set variables
    clpset_writeln(T): write term T with set variables followed by a new line
*/
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% R<=S
:-write('compile it first as compile(clpset).'),nl.

clpset_inclusion(R,S):-
    $set(RP,RA,RCard,_)=R,
    $set(SP,SA,SCard,_)=S :
    RCard #=< SCard,
    set_inclusion_consistency(R,S), %remove(\Sp,R),%add(R+,S)
    clpset_inclusion_forward(R,S),
    clpset_inclusion_backward(R,S).
clpset_inclusion(R,S):-true ?
    clpset_check_domain(R,R1),
    clpset_check_domain(S,S1),!,
    clpset_inclusion(R1,S1).
clpset_inclusion(R,S):-
    handle_exception(illegal_arguments,clpset_inclusion).

%remove(\Sp,R),%add(R+,S)
set_inclusion_consistency(R,S):-
    $set(RP,RA,RCard,_)=R,
    $set(SP,SA,SCard,_)=S :
    b_DM_MIN_MAX_cff(SP,MinS,MaxS), 
    clpset_shrink_universe(R,MinS,MaxS),
    clpset_notin_notin(S,R),
    clpset_in_in(R,S).
   
% for each element x, if x notin S then remove(x,R)
clpset_notin_notin(S,R):-
    $set(SP,SA,SCard,_)=S,
    $set(RP,RA,RCard,_)=R,
    dvar_bv(SP) :
    b_DM_MIN_MAX_cff(RP,Min,Max),
    Start is Min+1,
    End is Max-1,
    clpset_notin_notin(Start,End,S,R).
clpset_notin_notin(S,R):-true : true.

clpset_notin_notin(N0,N,S,R):-N0>N : true.
clpset_notin_notin(N0,N,S,R):-
    $clpset_is_out(N0,S),!,
    $clpset_remove(N0,R),
    N1 is N0+1,
    clpset_notin_notin(N1,N,S,R).
clpset_notin_notin(N0,N,S,R):-
    true :
    N1 is N0+1,
    clpset_notin_notin(N1,N,S,R).

% for each element x, if x in R then add(x,S)
clpset_in_in(R,S):-
    $set(SP,SA,SCard,_)=S,
    $set(RP,RA,RCard,_)=R,
    dvar_bv(RA) :
    b_DM_MIN_MAX_cff(RP,Min,Max),
    Start is Min+1,
    End is Max-1,
    clpset_in_in(Start,End,R,S).
clpset_in_in(R,S):-true : true.

clpset_in_in(N0,N,R,S):-N0>N : true.
clpset_in_in(N0,N,R,S):-
    $clpset_is_in(N0,R),!,
    $clpset_add(N0,S),
    N1 is N0+1,
    clpset_in_in(N1,N,R,S).
clpset_in_in(N0,N,R,S):-
    true :
    N1 is N0+1,
    clpset_in_in(N1,N,R,S).
    
% R--> S
% add(d,R) => add(d,S)
clpset_inclusion_forward(R,S), 
    $set(RP,RA,_,SetR)=R,
    $set(SP,SA,_,SetS)=S,
    {dom(RA,Elm)}
    =>
    $clpset_add(Elm,S).

% R <-- S
% remove(d,S) => remove(d,R)
clpset_inclusion_backward(R,S),
    $set(SP,SA,_,SetS)=S,
    {dom(SP,Elm)}
    =>
    $clpset_remove(Elm,R).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% R.S=T 
clpset_intersection(R,S,T):-
    $set(RP,RA,_,_)=R,
    $set(SP,SA,_,_)=S,
    $set(TP,TA,_,TV)=T :
    clpset_inclusion(T,R),
    clpset_inclusion(T,S),
    clpset_intersection_consistency(R,S,T),
    clpset_intersection_forward(R,S,T),
    clpset_intersection_forward(S,R,T),
    clpset_intersection_backward(R,S,T),
    clpset_propagate_ins_ins_to_ins(R,S,T).
clpset_intersection(R,S,T):-
    clpset_check_domain(R,R1),
    clpset_check_domain(S,S1),
    clpset_check_domain(T,T1),!,	
    clpset_intersection(R1,S1,T1).
clpset_intersection(R,S,T):-
    handle_exception(illegal_arguments,clpset_intersection).

%add(R+.S+,T)
clpset_intersection_consistency(R,S,T):-
    $set(RP,RA,_,_)=R,
    $set(SP,SA,_,_)=S,
    $set(TP,TA,CardT,TV)=T :
    b_DM_MIN_MAX_cff(TP,MinT,MaxT),
    First is MinT+1,
    Last is MaxT-1,
    ((dvar_bv(RA);dvar_bv(SA)) -> 
     clpset_in_in_intersection_in(First,Last,R,S,T);
     true
     ).

clpset_in_in_intersection_in(N0,N,R,S,T):-N0>N : true.
clpset_in_in_intersection_in(N0,N,R,S,T):-
    clpset_is_in(N0,R),clpset_is_in(N0,S),!,
    $clpset_add(N0,T),
    N1 is N0+1,
    clpset_in_in_intersection_in(N1,N,R,S,T).
clpset_in_in_intersection_in(N0,N,R,S,T):-
    N1 is N0+1,
    clpset_in_in_intersection_in(N1,N,R,S,T).

%add(d,R) -> add(d,T) if d in S
clpset_intersection_forward(R,S,T),
    $set(RP,RA,_,SetR)=R,
    $set(SP,SA,_,SetS)=S,
    {dom(RA,Elm)}
    =>
    ($clpset_is_in(Elm,S)->$clpset_add(Elm,T);true).

%remove(d,T)->(x notin R or x notin S)
clpset_intersection_backward(R,S,T),
    $set(TP,TA,_,SetT)=T,
    {dom(TP,Elm)}
    =>
    clpset_intersection_backward_action(Elm,R,S).

clpset_intersection_backward_action(Elm,R,S):-
    $clpset_is_in(Elm,R),!,
    $clpset_remove(Elm,S).
clpset_intersection_backward_action(Elm,R,S):-
    $clpset_is_in(Elm,S),!,
    $clpset_remove(Elm,R).
clpset_intersection_backward_action(Elm,R,S).
    
/*
    clpset_intersection_notin_both(Elm,R,S),
    clpset_intersection_notin_both(Elm,S,R).

clpset_intersection_notin_both(X,R,S),
    arg(2,R,RA), % $set(RP,RA,_,SetR)=R
    {dom(RA,Elm)}
    =>
    clpset_intersection_notin_both_aux(Elm,S,X).

clpset_intersection_notin_both_aux(Elm,S,X):-
    X==Elm : $clpset_remove(Elm,S).
clpset_intersection_notin_both_aux(Elm,S,X).
*/
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% R+S=T 
clpset_union(R,S,T):-
    $set(RP,RA,_,_)=R,
    $set(SP,SA,_,_)=S,
    $set(TP,TA,_,TV)=T :
    clpset_inclusion(R,T),
    clpset_inclusion(S,T),
    b_DM_MIN_MAX_cff(RP,MinR,MaxR),
    b_DM_MIN_MAX_cff(SP,MinS,MaxS),
    $minimum2(MinR,MinS,MinT),
    $maximum2(MaxR,MaxS,MaxT),
    clpset_shrink_universe(T,MinT,MaxT),
    clpset_union_consistency(R,S,T),
    clpset_union_forward(R,S,T),
    clpset_union_forward(S,R,T),
    clpset_union_backward(R,S,T),
    clpset_propagate_ins_ins_to_ins(R,S,T).
clpset_union(R,S,T):-
    clpset_check_domain(R,R1),
    clpset_check_domain(S,S1),
    clpset_check_domain(T,T1),!,	
    clpset_union(R1,S1,T1).
clpset_union(R,S,T):-
    handle_exception(illegal_arguments,clpset_union).

%remove(R-.S-,T): for each x, if x is not in R or S then x is not in T
clpset_union_consistency(R,S,T):-
    $set(RP,RA,_,_)=R,
    $set(SP,SA,_,_)=S,
    $set(TP,TA,CardT,TV)=T ?
    (dvar_bv(RP);dvar_bv(SP)),!,
    b_DM_MIN_MAX_cff(TP,LowT,UpT),
    First is LowT+1,
    Last is UpT-1,
    clpset_notin_notin_union_notin(First,Last,R,S,T).
clpset_union_consistency(R,S,T).

clpset_notin_notin_union_notin(N0,N,R,S,T):-N0>N : true.
clpset_notin_notin_union_notin(N0,N,R,S,T):-
    $clpset_is_out(N0,R),$clpset_is_out(N0,S),!,
    $clpset_remove(N0,T),
    N1 is N0+1,
    clpset_notin_notin_union_notin(N1,N,R,S,T).
clpset_notin_notin_union_notin(N0,N,R,S,T):-
    N1 is N0+1,
    clpset_notin_notin_union_notin(N1,N,R,S,T).

%remove(d,R) -> remove(d,T) if d notin S
clpset_union_forward(R,S,T),
    $set(RP,RA,_,SetR)=R,
    {dom(RP,Elm)}
    =>
    clpset_union_forward_action(Elm,S,T).

clpset_union_forward_action(X,S,T):-
    $clpset_is_out(X,S),!,
    $clpset_remove(X,T).
clpset_union_forward_action(X,S,T).

%add(d,T)-> (x in R or x in S)
clpset_union_backward(R,S,T),
    $set(TP,TA,_,SetT)=T,
    {dom(TA,Elm)} 
    =>
    ($clpset_is_out(Elm,R)->$clpset_add(Elm,S);
     $clpset_is_out(Elm,S)->$clpset_add(Elm,R);
     true).

/*
     clpset_union_in_either(Elm,R,S),
     clpset_union_in_either(Elm,S,R)).

clpset_union_in_either(X,R,S),
    $set(RP,RA,_,SetR)=R,
    {dom(RP,Y)}
    =>
    (X==Y->$clpset_add(X,S);true).
*/
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%clpset_complement
clpset_complement(R,S):-
    $set(RP,RA,CardR,SetR)=R,
    $set(SP,SA,CardS,SetS)=S :
    b_DM_MIN_MAX_cff(RP,MinR,MaxR),
    b_DM_MIN_MAX_cff(SP,MinS,MaxS),
    clpset_shrink_universe(R,MinS,MaxS),
    clpset_shrink_universe(S,MinR,MaxR),
    b_DM_MIN_MAX_cff(RP,Min,Max),
    First is Min+1,
    Last is Max-1,    
    ((dvar_bv(RP);dvar_bv(RA))->
	clpset_complement_consistency(First,Last,R,S);
	true
    ),
    ((dvar_bv(SP);dvar_bv(SA))->
	clpset_complement_consistency(First,Last,S,R);
	true
    ),
    clpset_complement_propagate_a(R,S),
    clpset_complement_propagate_a(S,R),
    clpset_complement_propagate_p(R,S),
    clpset_complement_propagate_p(S,R),
    clpset_propagate_ins_to_ins(R,S),
    clpset_propagate_ins_to_ins(S,R).
clpset_complement(R,S):-
    clpset_check_domain(R,R1),
    clpset_check_domain(S,S1),!,
    clpset_complement(R1,S1).
clpset_complement(R,S):-
    handle_exception(illegal_arguments,clpset_complement).

%remove(R+,S),add(R-,S)
clpset_complement_consistency(N0,N,R,S):-N0>N : true.
clpset_complement_consistency(N0,N,R,S):-
    ($clpset_is_out(N0,R) -> $clpset_add(N0,S);true),
    ($clpset_is_in(N0,R)-> $clpset_remove(N0,S);true),
    N1 is N0+1,
    clpset_complement_consistency(N1,N,R,S).

% add(x,R) -> remove(x,S)
clpset_complement_propagate_a(R,S),
    $set(RP,RA,CardR,SetR)=R,
    {dom(RA,Elm)}
    =>
    $clpset_remove(Elm,S).

% remove(x,R) -> add(x,S)
clpset_complement_propagate_p(R,S),
    $set(RP,RA,CardR,SetR)=R,
    {dom(RP,Elm)}
    =>
    $clpset_add(Elm,S).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%clpset_disjoint
clpset_disjoint(R,S):-
     $set(RP,RA,CardR,SetR)=R :
     $set(SP,SA,CardS,SetS)=S :
     clpset_disjoint_consistency(R,S),
     clpset_disjoint_propagate(R,S),
     clpset_disjoint_propagate(S,R).
clpset_disjoint(R,S):-
    clpset_check_domain(R,R1),
    clpset_check_domain(S,S1),!,
    clpset_disjoint(R1,S1).
clpset_disjoint(R,S):-
    handle_exception(illegal_arguments,clpset_disjoint).

% for each x, if x in R then x notin S
clpset_disjoint_consistency(R,S):-
    $set(RP,RA,_,_)=R,
    $set(SP,SA,_,_)=S :
    b_DM_MIN_MAX_cff(RP,MinR,MaxR),
    b_DM_MIN_MAX_cff(SP,MinS,MaxS),
    $maximum2(MinR,MinS,Min),
    $minimum2(MaxR,MaxS,Max),
    First is Min+1,
    Last is Max-1,
    (dvar_bv(RA) -> clpset_in_notin(First,Last,R,S);true),
    (dvar_bv(SA) -> clpset_in_notin(First,Last,S,R);true).

clpset_in_notin(N0,N,R,S):-N0>N : true.
clpset_in_notin(N0,N,R,S):-true :
    $clpset_is_in(N0,R),
    $clpset_remove(N0,S),
    N1 is N0+1,
    clpset_in_notin(N1,N,R,S).

% add(x,R) => remove(x,S)
clpset_disjoint_propagate(R,S),
    $set(RP,RA,_,_)=R,
    {dom(RA,X)}
    =>
    $clpset_remove(X,S).
    
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
clpset_difference(R,S,T):-
    clpset_complement(S,S1),
    clpset_intersection(R,S1,T).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
clpset_is_out(X,S):-
    integer(X),
    $set(SP,SA,_,SetS)=S :
    $clpset_is_out(X,S).
clpset_is_out(X,S):-true :
    handle_exception(illegal_arguments,clpset_is_out(X,S)).

$clpset_is_out(X,S):-
    $set(SP,SA,_,SetS)=S ?
    b_DM_MIN_MAX_cff(SP,Min,Max),
    X>Min,X<Max,
    b_DM_TRUE_cc(SP,X),!,fail.
$clpset_is_out(X,S):-true : true.

%%
clpset_is_in(X,S):-
    integer(X),		       
    $set(SP,SA,_,SetS)=S :
    $clpset_is_in(X,S).
clpset_is_in(X,S):-true :
    handle_exception(illegal_arguments,clpset_is_in(X,S)).

$clpset_is_in(X,S):-
    $set(SP,SA,_,SetS)=S ?
    b_DM_MIN_MAX_cff(SP,Min,Max),
    X>Min,X<Max,
    fd_false(SA,X).

%%
clpset_remove(X,S):-
    integer(X),
    $set(SP,SA,Card,SetS)=S :
    $clpset_remove(X,S).
clpset_remove(X,S):-true :
    handle_exception(illegal_arguments,clpset_remove(X,S)).

$clpset_remove(S,L,U):-L>=U : true.
$clpset_remove(S,L,U):-
    $clpset_remove(L,S),
    L1 is L+1,
    $clpset_remove(S,L1,U).

$clpset_remove(X,S):-
    $set(SP,SA,Card,SetS)=S,
    b_DM_MIN_MAX_cff(SP,Min,Max),
    X>Min,X<Max :
    b_DM_TRUE_cc(SA,X),
    domain_set_false(SP,X),
    $clpset_u_card(SP,Ucard),
    domain_region_max(Card,Ucard),
    ((integer(Card),Card=:=Ucard) -> 
        b_DM_NEXT_ccf(SP,Min,FirstElm),
        $clpset_in_if_potential(SP,SA,FirstElm,Max),
        $clpset_indomain_pickup(S);
        true).
$clpset_remove(X,S):-true : true.

%%
clpset_add(X,S):-
    integer(X),
    $set(SP,SA,_,SetS)=S :
    $clpset_add(X,S).
clpset_add(X,S):-true :
    handle_exception(illegal_arguments,clpset_add(X,S)).

$clpset_add(X,S):-
    $set(SP,SA,Card,SetS)=S :
    b_DM_MIN_MAX_cff(SP,Min,Max),
    X>Min,X<Max,
    b_DM_TRUE_cc(SP,X),
    domain_set_false(SA,X),
    $clpset_l_card(SA,Min,Max,L),
    domain_region_min(Card,L),
    ((integer(Card),Card=:=L) -> 
       b_DM_NEXT_ccf(SP,Min,FirstElm),
       $clpset_notin_if_notin(SP,SA,FirstElm,Max),
       $clpset_indomain_pickup(S);
       true).

%%
$clpset_u_card(SP,Ucard):-
    b_DM_COUNT_cf(SP,NoPosElms),
    Ucard is NoPosElms-2.

$clpset_l_card(SA,Min,Max,Lcard):-
    b_DM_COUNT_cf(SA,Size),
    Lcard is Max-Min+1-Size.

%% for each X in SP, if X is not yet added to the set, do so.
$clpset_in_if_potential(SP,SA,X,Max):-X>=Max : true.
$clpset_in_if_potential(SP,SA,X,Max):-true :
    b_DM_NEXT_ccf(SP,X,NextX),
    domain_set_false(SA,X),
    $clpset_in_if_potential(SP,SA,NextX,Max).
    
%% for each X in SP, if X is not included in the set, then exclude it from SP
$clpset_notin_if_notin(SP,SA,X,Max):-X>=Max : true.
$clpset_notin_if_notin(SP,SA,X,Max):-true :
    b_DM_NEXT_ccf(SP,X,NextX),
    (fd_true(SA,X)->
    domain_set_false(SP,X)
    ;
    true),
    $clpset_notin_if_notin(SP,SA,NextX,Max).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% cardinality constraint
clpset_card(S,Card1):-
    $set(SP,SA,Card,SetS)=S :
    Card #= Card1.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%labeling set-domain variables
clpset_labeling([]):-true : true.
clpset_labeling([X|Xs]):-true :
	clpset_labeling(X),
	clpset_labeling(Xs).
clpset_labeling(X):-
	$set(_,_,_,_)=X : clpset_indomain(X).
clpset_labeling(X):-
	true :
	handle_exception(illegal_argument,clpset_indomain(X)).

clpset_labeling_ff([]):-true : true.
clpset_labeling_ff([X|Xs]):-
	$set(_,_,_,Set)=X,
        nonvar(Set) : 
        clpset_labeling_ff(Xs).
clpset_labeling_ff(Xs):-
        [_|_]=Xs :
        clpset_select_ff(Xs,X),
        clpset_indomain(X),
        clpset_labeling_ff(Xs).
clpset_labeling_ff(X):-
	$set(_,_,_,_)=X : clpset_indomain(X).
clpset_labeling_ff(X):-
	true :
	handle_exception(illegal_argument,clpset_indomain(X)).

clpset_select_ff([S|Ss],X):-
    $set(SP,SA,_,_)=S : 
    b_DM_COUNT_cf(SP,Size), % Size means the number of elements that haven't been added into the set
    clpset_select_ff(Ss,S,Size,X).

clpset_select_ff([],S0,Size0,X):-true : X=S0.
clpset_select_ff([S|Ss],S0,Size0,X):-
    $set(SP,SA,_,Set)=S,
    nonvar(Set) : 
    b_DM_COUNT_cf(SP,Size), 
    (Size<Size0 -> Size1=Size,S1=S;
     Size1=Size0,S1=S0),
    clpset_select_ff(Ss,S1,Size1,X).
clpset_select_ff([S|Ss],S0,Size0,X):-true :
    clpset_select_ff(Ss,S0,Size0,X).

clpset_indomain(S):-
    $set(SP,SA,Card,Set)=S,
    var(Set) :
    b_DM_MIN_MAX_cff(SP,Min,Max),
    b_DM_NEXT_ccf(SP,Min,X),
    clpset_indomain(S,SP,SA,X,Max).
clpset_indomain(S):-
    $set(SP,SA,Card,Set)=S : true.
clpset_indomain(S):-
    true : 
    handle_exception(illegal_argument,clpset_indomain(S)).

clpset_indomain(S,SP,SA,X,Max):-
    X<Max :
    b_DM_NEXT_ccf(SP,X,NextX),
    ($clpset_add(X,S);
%     increment_backtrack_nos,
     $clpset_remove(X,S)), 
    clpset_indomain(S,SP,SA,NextX,Max).
clpset_indomain(S,SP,SA,X,Max):-true : true.

$clpset_indomain_pickup(S):-
    $set(SP,SA,Card,Set)=S : 
    b_DM_MIN_MAX_cff(SP,Min,Max),
    b_DM_NEXT_ccf(SP,Min,X),
    $clpset_indomain_pickup(SP,X,Max,List),
    Set=List.

$clpset_indomain_pickup(SP,X,Max,List):-X>=Max : List=[].
$clpset_indomain_pickup(SP,X,Max,List):-
    List=[X|ListR],
    b_DM_NEXT_ccf(SP,X,NextX),
    $clpset_indomain_pickup(SP,NextX,Max,ListR).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%clpset_unify
clpset_unify(T1,T2):-
    [_|_]=T1 :
    (integer_list(T1)-> clpset_create_constant_domain(T1,Var);
     handle_exception(illegal_set_constant,clpset_unify(T1,T2))),
    clpset_unify(Var,T2).
clpset_unify(T1,T2):-
    [_|_]=T2 :
    (integer_list(T2)-> clpset_create_constant_domain(T2,Var);
     handle_exception(illegal_set_constant,clpset_unify(T1,T2))),
    clpset_unify(T1,Var).
clpset_unify(T1,T2):-
    var(T1) :
    T1=T2,
    clpset_domain(T1).
clpset_unify(T1,T2):-
    var(T2) :
    T1=T2,
    clpset_domain(T2).
clpset_unify(T1,T2):-
    $set(_,_,C1,Set1)=T1,
    $set(_,_,C2,Set2)=T2 :
    C1=C2,
    Set1=Set2,
    clpset_inclusion(T1,T2),
    clpset_inclusion(T2,T1),
    clpset_propagate_ins_to_ins(T1,T2),
    clpset_propagate_ins_to_ins(T2,T1).
clpset_unify(T1,T2):-true :
    handle_exception(illegal_arguments,clpset_unify(T1,T2)).

clpset_create_constant_domain([],S):-true : 
    $set(SP,SA,0,[])=S,
    domain(SP,0,1),
    domain(SA,0,1).
clpset_create_constant_domain(List,S):-
    list_min_max(List,Min,Max),
    clpset_domain(S,Min,Max),
    clpset_list_to_set(List,S).

list_min_max([X|List],Min,Max):-true :
    list_min_max(List,X,Min,X,Max).

list_min_max([],Min0,Min,Max0,Max):-true : Min=Min0,Max=Max0.
list_min_max([X|Xs],Min0,Min,Max0,Max):-
    X>Max0 :
    list_min_max(Xs,Min0,Min,X,Max).
list_min_max([X|Xs],Min0,Min,Max0,Max):-
    X<Min0 :
    list_min_max(Xs,X,Min,Max0,Max).
list_min_max([X|Xs],Min0,Min,Max0,Max):-
    true :
    list_min_max(Xs,Min0,Min,Max0,Max).

clpset_list_to_set([],S):-true : 
    clpset_indomain(S).
clpset_list_to_set([X|Xs],S):-
    clpset_add(X,S),
    clpset_list_to_set(Xs,S).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%utilities
clpset_propagate_ins_ins_to_ins(R,S,T),
    $set(RP,RA,_,SetR)=R,
    $set(SP,SA,_,SetS)=S,
    var(SetR),
    {ins(SetR),ins(SetS)}
    => 
    true.
clpset_propagate_ins_ins_to_ins(R,S,T),
    $set(SP,SA,_,SetS)=S,
    var(SetS),
    {ins(SetS)}
    => true.
clpset_propagate_ins_ins_to_ins(R,S,T) =>
    clpset_indomain(T).
	
clpset_propagate_ins_to_ins(R,S),
    $set(RP,RA,_,SetR)=R,
    var(SetR),
    {ins(SetR)}
    =>
    true.
clpset_propagate_ins_to_ins(R,S) =>
    clpset_indomain(S).

clpset_check_domain(R,NewR):-var(R) : clpset_domain(R),NewR=R.
clpset_check_domain(R,NewR):-$set(Possible,Allowed,Card,Value)=R : NewR=R.
clpset_check_domain(R,NewR):-[_|_]=R : 
    (integer_list(R)-> clpset_create_constant_domain(R,NewR);
     handle_exception(illegal_set_constant,R)).

clpset_domain(R):-
    fd_vector_min_max(L,U),
    Min is L+2,
    Max is U-2,
    clpset_domain(R,Min,Max).
		       
clpset_domain(R,L,U):-
    R=$set(Possible,Allowed,Card,Value),!,
    L1 is L-1,
    U1 is U+1,
    domain(Possible,L1,U1),
    domain(Allowed,L1,U1),
    Size is U-L+1,
    domain(Card,0,Size).
clpset_domain([R|Rs],L,U):-true :
    clpset_domain(R,L,U),
    clpset_domain(Rs,L,U).
clpset_domain([],L,U):-true : true.

clpset_shrink_universe(S,Min,Max):- $set(SP,SA,C,_)=S, dvar_bv(SP) : true.
clpset_shrink_universe(S,Min,Max):- $set(SP,SA,C,_)=S, dvar_bv(SA) :  true.
clpset_shrink_universe(S,Min,Max):- 
    $set(SP,SA,C,_)=S :
    domain_region(SP,Min,Max),
    domain_region(SA,Min,Max),
    b_DM_MIN_MAX_cff(SP,L,U),
    Size is U-L-1,
    C #=< Size.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
clpset_domain_var($set(_Sp,_Sa,_Card,_)):-true : true.

clpset_value($set(_Sp,_Sa,_Card,Set),Value):-true : Value=Set.
clpset_value(Set,Value):-true :
	handle_exception(illegal_arguments,clpset_value).

clpset_writeln(X):-
       clpset_write(X),nl.

clpset_write($set(_Sp,_Sa,_Card,Set)):-true : write(Set).
clpset_write(T):-var(T) : write(T).
clpset_write(T):-atomic(T) : write(T).
clpset_write([X|Xs]):-true :
	write('['),
	clpset_write_list(X,Xs),
	write(']').
clpset_write(T):-true :
        functor(T,F,N),
        write(F),write('('),
        clpset_write_args(T,1,N),write(')').

clpset_write_args(T,N,N):-true : arg(N,T,A), clpset_write(A).
clpset_write_args(T,N0,N):-true : arg(N0,T,A), clpset_write(A),write(','),N1 is N0+1,clpset_write_args(T,N1,N).

clpset_write_list(X,[Y|Ys]):-true : 
       clpset_write(X),write(','),clpset_write_list(Y,Ys).
clpset_write_list(X,[]):-true : clpset_write(X).
clpset_write_list(X,Y):-true : clpset_write(X),write('|'),clpset_write(Y).

$maximum3(A,B,C,Min):-A>B :
    $maximum2(A,C,Min).
$maximum3(A,B,C,Min):-true :
    $maximum2(B,C,Min).
   
$maximum2(A,B,Min):-A>B : Min=A.
$maximum2(A,B,Min):-true : Min=B.

$minimum3(A,B,C,Min):-A<B :
    $minimum2(A,C,Min).
$minimum3(A,B,C,Min):-true :
    $minimum2(B,C,Min).
   
$minimum2(A,B,Min):-A<B : Min=A.
$minimum2(A,B,Min):-true : Min=B.

fd_false(X,E):-
    dvar(X),
    b_DM_TRUE_cc(X,E) : fail.
fd_false(X,E):-
    dvar(X) : true.
fd_false(X,E):-
    integer(X) : X \= E.
fd_false(X,E):-true : handle_exception(illegal_arguments,fd_false(X,E)).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
increment_backtrack_nos:-
    (retract(backtracks(B));B=0),!,
    B1 is B+1,
    assert(backtracks(B1)).