set_rewriter

avl_list_to_list_of_asts(_, [], Acc, Acc).

avl_list_to_list_of_asts(InType, [Val-_|T], Acc, L) :-
    avl_list_to_list_of_asts(InType, T, [b(value(Val),InType,[])|Acc], L).

check_limit(FI, TI, Info, Options) :-
    Card is TI - FI,
    ( ( memberchk(instantiate_sets_limit(SetLimit), Options) -> true
    ; memberchk(instantiate_quantifier_limit(SetLimit), Options)
    )
    -> ( Card =< SetLimit
    -> true
    ; perfmessage(quantifier,not_expanding_interval_in_quantifier(FI,TI,limit(SetLimit)),Info),
    fail
    )
    ; true
).

constant_interval_as_list(FI,TI,[]) :-
    FI > TI.

constant_interval_as_list(FI,FI,[BI]) :-
    !, %safe_create_texpr(integer(FI), integer, [], BI).
    BI = b(value(int(FI)),integer,[]).

constant_interval_as_list(FI,TI,[BI|BIs]) :-
    %safe_create_texpr(integer(FI), integer, [], BI),
    BI = b(value(int(FI)),integer,[]),
    NFI is FI + 1,
    constant_interval_as_list(NFI,TI,BIs).

create_all_different(Asts, AllDiffAst) :-
    create_all_different(Asts, [], InEqs),
    conjunct_predicates(InEqs, AllDiffAst).

create_all_different([], Acc, Acc).

create_all_different([A|T], Acc, InEqs) :-
    create_all_different_fixed(A, T, Acc, NAcc),
    create_all_different(T, NAcc, InEqs).

create_all_different_fixed(_, [], Acc, Acc).

create_all_different_fixed(A, [B|T], Acc, InEqs) :-
    safe_create_texpr(not_equal(A,B), pred, [], InEq),
    NAcc = [InEq|Acc],
    create_all_different_fixed(A, T, NAcc, InEqs).

create_all_same_fixed(_, [], Acc, Acc).

create_all_same_fixed(A, [B|T], Acc, InEqs) :-
    safe_create_texpr(equal(A,B), pred, [], InEq),
    NAcc = [InEq|Acc],
    create_all_same_fixed(A, T, NAcc, InEqs).

create_at_least_one_eq(L, AtLeastOneEq) :-
    create_at_least_one_eq(L, [], Eqs),
    disjunct_predicates(Eqs, AtLeastOneEq).

create_at_least_one_eq([], Acc, Acc).

create_at_least_one_eq([A|T], Acc, List) :-
    create_all_same_fixed(A, T, Acc, NAcc),
    create_at_least_one_eq(T, NAcc, List).

get_integer_constant(Ast, IntConst) :-
    get_integer(Ast, IntConst).

get_integer_constant(b(min_int,integer,_), MinInt) :-
    get_preference(minint, MinInt).

get_integer_constant(b(max_int,integer,_), MaxInt) :-
    get_preference(maxint, MaxInt).

rewrite_finite_card(less(Card,Integer), Res, card_to_at_least_one_eq) :-
    % card({a1,..,ak}) < k --> at least one eq (has n*log(n) disjuncts)
    rewrite_finite_card_k_less_k(Card, Integer, Res).

rewrite_finite_card(greater(Integer,Card), Res, card_to_at_least_one_eq) :-
    % k > card({a1,..,ak}) --> at least one eq (has n*log(n) disjuncts)
    rewrite_finite_card_k_less_k(Card, Integer, Res).

rewrite_finite_card(less_equal(Card,Integer), Res, card_to_at_least_one_eq) :-
    % card({a1,..,ak}) <= k - 1 --> at least one eq (has n*log(n) disjuncts)
    rewrite_finite_card_k_leq_k_minus_1(Card, Integer, Res).

rewrite_finite_card(greater_equal(Integer,Card), Res, card_to_at_least_one_eq) :-
    % k - 1 >= card({a1,..,ak}) --> at least one eq (has n*log(n) disjuncts)
    rewrite_finite_card_k_leq_k_minus_1(Card, Integer, Res).

rewrite_finite_card(less_equal(Card,Integer), Res, card_to_truth_leq_k) :-
    % card({a1,..,ak}) <= k --> truth
    rewrite_finite_card_k_leq_k(Card, Integer, Res).

rewrite_finite_card(greater_equal(Integer,Card), Res, card_to_truth_leq_k) :-
    % k >= card({a1,..,ak}) --> truth
    rewrite_finite_card_k_leq_k(Card, Integer, Res).

rewrite_finite_card(less(Card,Integer), Res, card_to_truth_leq_k1) :-
    % card({a1,..,ak}) < k + 1 --> truth
    rewrite_finite_card_k_leq_k_plus_1(Card, Integer, Res).

rewrite_finite_card(greater(Integer,Card), Res, card_to_truth_leq_k1) :-
    % k + 1 > card({a1,..,ak}) --> truth
    rewrite_finite_card_k_leq_k_plus_1(Card, Integer, Res).

rewrite_finite_card(greater_equal(Card,Integer), Res, card_to_all_different_greater_eq) :-
    % card({a1,..,ak}) >= k --> all_different
    rewrite_finite_card_k_eq_k(Card, Integer, Res).

rewrite_finite_card(less_equal(Integer,Card), Res, card_to_all_different_greater_eq) :-
    % k <= card({a1,..,ak}) --> all_different
    rewrite_finite_card_k_eq_k(Card, Integer, Res).

rewrite_finite_card(greater(Card,Integer), Res, card_to_falsity) :-
    % card({a1,..,ak}) > n --> falsity if n>=k
    rewrite_finite_card_greater_less_k(Card, Integer, Res).

rewrite_finite_card(less(Integer,Card), Res, card_to_falsity) :-
    % n < card({a1,..,ak}) --> falsity if n>=k
    rewrite_finite_card_greater_less_k(Card, Integer, Res).

rewrite_finite_card(greater_equal(Card,Integer), Res, card_to_falsity) :-
    % card({a1,..,ak}) >= n --> falsity if n>k
    rewrite_finite_card_greatereq_lesseq_n(Card, Integer, Res).

rewrite_finite_card(less_equal(Integer,Card), Res, card_to_falsity) :-
    % n <= card({a1,..,ak}) --> falsity if n>k
    rewrite_finite_card_greatereq_lesseq_n(Card, Integer, Res).

rewrite_finite_card(greater(Card,Integer), Res, card_to_all_different_greater) :-
    % card({a1,..,ak}) > k - 1 --> all different
    rewrite_finite_card_greater_less_k1(Card, Integer, Res).

rewrite_finite_card(less(Integer,Card), Res, card_to_all_different_greater) :-
    % k - 1 < card({a1,..,ak}) --> all different
    rewrite_finite_card_greater_less_k1(Card, Integer, Res).

rewrite_finite_card(greater_equal(Card,Integer1), Res, card_to_truth) :-
    % card({a1,..,ak}) >= 1 --> truth
    rewrite_finite_card_geq_leq_1(Card, Integer1, Res).

rewrite_finite_card(less_equal(Integer1,Card), Res, card_to_truth) :-
    % 1 <= card({a1,..,ak}) --> truth
    rewrite_finite_card_geq_leq_1(Card, Integer1, Res).

rewrite_finite_card(equal(Card,Integer), Res, card_to_single_equality) :-
    % card({a1,a2}) = 1 --> a1=a2
    rewrite_finite_card_2_eq_1(Card, Integer, Res).

rewrite_finite_card(equal(Integer,Card), Res, card_to_single_equality) :-
    % 1 = card({a1,a2}) --> a1=a2
    rewrite_finite_card_2_eq_1(Card, Integer, Res).

rewrite_finite_card(not_equal(Card,Integer), Res, card_to_single_non_equality) :-
    % card({a1,a2}) /= 1 --> a1/=a2
    rewrite_finite_card_2_neq_1(Card, Integer, Res).

rewrite_finite_card(not_equal(Integer,Card), Res, card_to_single_non_equality) :-
    % 1 /= card({a1,a2}) --> a1/=a2
    rewrite_finite_card_2_neq_1(Card, Integer, Res).

rewrite_finite_card(equal(Card,Integer), Res, card_to_falsity_nonempty_eq_zero) :-
    % card({a1,..,ak}) = 0 --> falsity
    rewrite_finite_card_eq_0(Card, Integer, Res).

rewrite_finite_card(equal(Integer,Card), Res, card_to_falsity_nonempty_eq_zero) :-
    % card({a1,..,ak}) = 0 --> falsity
    rewrite_finite_card_eq_0(Card, Integer, Res).

rewrite_finite_card(equal(Card,Integer), Res, card_to_all_different_eq_k) :-
    % card({a1,..,ak}) = k --> all different
    rewrite_finite_card_k_eq_k(Card, Integer, Res).

rewrite_finite_card(equal(Integer,Card), Res, card_to_all_different_eq_k) :-
    % k = card({a1,..,ak}) --> all different
    rewrite_finite_card_k_eq_k(Card, Integer, Res).

rewrite_finite_card(greater_equal(Card,Integer), Res, card_to_all_different_geq_k) :-
    % card({a1,..,ak}) >= k --> all different
    rewrite_finite_card_k_eq_k(Card, Integer, Res).

rewrite_finite_card(less_equal(Integer,Card), Res, card_to_all_different_geq_k) :-
    % k >= card({a1,..,ak}) --> all different
    rewrite_finite_card_k_eq_k(Card, Integer, Res).

rewrite_finite_card_2_eq_1(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(1),integer,_); Integer = b(value(int(1)),integer,_)),
    SetExtension = b(set_extension([A1,A2]),_,_),
    !,
    Res = equal(A1,A2).

rewrite_finite_card_2_neq_1(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(1),integer,_); Integer = b(value(int(1)),integer,_)),
    SetExtension = b(set_extension([A1,A2]),_,_),
    !,
    Res = not_equal(A1,A2).

rewrite_finite_card_eq_0(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(0),integer,_); Integer = b(value(int(0)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    L \== [],
    !,
    Res = falsity.

rewrite_finite_card_geq_leq_1(Card, Integer1, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer1 = b(integer(1),integer,_); Integer1 = b(value(int(1)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    L \== [],
    !,
    get_texpr_type(SetExtension, SetType),
    % don't create simple truth to keep variables in scope, could be the only occurrence
    Res = not_equal(SetExtension,b(empty_set,SetType,[])).

rewrite_finite_card_geq_leq_k(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    length(L, Len),
    ICard > Len,
    !,
    Res = falsity.

rewrite_finite_card_greater_less_k(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    length(L, Len),
    ICard >= Len,
    !,
    Res = falsity.

rewrite_finite_card_greater_less_k1(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    length(L, Len),
    ICard =:= Len - 1,
    !,
    create_all_different(L, AllDiffAst),
    get_texpr_expr(AllDiffAst, Res).

rewrite_finite_card_greatereq_lesseq_n(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    length(L, Len),
    ICard > Len,
    !,
    Res = falsity.

rewrite_finite_card_k_eq_k(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    length(L, Len),
    ICard == Len,
    !,
    create_all_different(L, AllDiffAst),
    get_texpr_expr(AllDiffAst, Res).

rewrite_finite_card_k_leq_k(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    length(L, Len),
    ICard >= Len,
    !,
    get_texpr_type(SetExtension, SetType),
    % don't create simple truth to keep variables in scope, could be the only occurrence
    Res = not_equal(SetExtension,b(empty_set,SetType,[])).

rewrite_finite_card_k_leq_k_minus_1(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    length(L, Len),
    ICard =:= Len - 1,
    !,
    create_at_least_one_eq(L, AtLeastOneEqAst),
    get_texpr_expr(AtLeastOneEqAst, Res).

rewrite_finite_card_k_leq_k_plus_1(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    length(L, Len),
    ICard1 is ICard + 1,
    ICard1 >= Len,
    !,
    get_texpr_type(SetExtension, SetType),
    % don't create simple truth to keep variables in scope, could be the only occurrence
    Res = not_equal(SetExtension,b(empty_set,SetType,[])).

rewrite_finite_card_k_less_k(Card, Integer, Res) :-
    Card = b(card(SetExtension),integer,_),
    (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)),
    SetExtension = b(set_extension(L),_,_),
    length(L, Len),
    ICard =:= Len,
    !,
    create_at_least_one_eq(L, AtLeastOneEqAst),
    get_texpr_expr(AtLeastOneEqAst, Res).

rewrite_set_aux(identifier(EnumSet), set(global(EnumSet)), Info, ScopeIds, _, SetAsts) :-
    enumerated_set(EnumSet),
    \+ memberchk(EnumSet, ScopeIds),
    \+ memberchk(introduced_by(_), Info),
    all_elements_of_type(EnumSet, SetValues),
    !,
    findall(b(value(Val),global(EnumSet),[]), member(Val, SetValues), SetAsts).

rewrite_set_aux(boolean_set, _, _, _, _, L) :-
    !,
    L = [b(boolean_true,boolean,[]), b(boolean_false,boolean,[])].

rewrite_set_aux(interval(From,To), _, Info, _, Options, L) :-
    !,
    get_integer_constant(From, FI),
    get_integer_constant(To, TI),
    check_limit(FI, TI, Info, Options),
    !,
    constant_interval_as_list(FI, TI, L).

rewrite_set_aux(set_extension(L), _, _, _, _, R) :-
    !,
    R = L.

rewrite_set_aux(value(Value), Type, _, _, Options, L) :- nonvar(Value),
    !,
    rewrite_value(Value, Type, Options, L).

rewrite_set_aux(cartesian_product(A,B), set(Type), _, ScopeIds, Options, L) :- !,
    rewrite_set_to_list_of_asts(A, ScopeIds, Options, AL),
    rewrite_set_to_list_of_asts(B, ScopeIds, Options, BL),
    findall(b(couple(VA,VB),Type,[]), (member(VA,AL),member(VB,BL)), L).

rewrite_set_to_list_of_asts(b(E,Type,Info), ScopeIds, L) :-
    rewrite_set_aux(E, Type, Info, ScopeIds, [], L).

rewrite_set_to_list_of_asts(b(E,Type,Info), ScopeIds, Options, L) :-
    rewrite_set_aux(E, Type, Info, ScopeIds, Options, L).

rewrite_value(global_set(EnumSet), _, _, L) :-
    enumerated_set(EnumSet),
    all_elements_of_type(EnumSet, SetValues),
    !,
    findall(b(value(Val),global(EnumSet),[]), member(Val, SetValues), L).

rewrite_value(avl_set(AvlSet), Type, _, L) :-
    !,
    ( Type = set(InType)
    ; Type = seq(SeqType),
    InType = couple(integer,SeqType)
    ),
    avl_to_list(AvlSet, AvlList),
    avl_list_to_list_of_asts(InType, AvlList, [], L).

rewrite_value(closure(P,T,B), _Type, Options, L) :-
    custom_explicit_sets:is_interval_closure(P,T,B,FI,TI), integer(FI),integer(TI),
    check_limit(FI, TI, B, Options),
    !,
    constant_interval_as_list(FI, TI, L).