trans_set(b(Expr,Type,_Infos),Env,Pred) :- % format(user_output,' set --> ~w~n',[Expr]),
(is_set(Type,BaseType)
-> ( Expr = identifier(ID) -> NExpr=identifier(ID,BaseType)
; Expr = comprehension_set(TIds,Body) -> NExpr = comprehension_set(TIds,BaseType,Body)
; NExpr = Expr)
; add_b2asp_error('Type of expression is not a set: ',Type), fail
),
!,
trans_set(NExpr,Env,Pred).
trans_set(empty_set,Env,Pred) :- !,
DummyArg = 0, % Clingo does not like unbound variables in head??
gensym_if_necessary(empty,Pred),
gen_clingo_clause(Pred,[DummyArg],Env, 1=2 ).
trans_set(bool_set,Env,Pred) :- !,
trans_set(set_extension([pred_false,pred_true]),Env,Pred).
trans_set(value(V),Env,Pred) :- V==[], !, trans_set(empty_set,Env,Pred).
trans_set(value(AVL),Env,Pred) :-
custom_explicit_sets:expand_custom_set_to_list_now(AVL,L),!, % this creates Value list not set_extension list ! TODO
trans_set(set_extension(L),Env,Pred).
trans_set(sequence_extension(L),Env,Pred) :- !,
add_indices(L,1,Set),
trans_set(set_extension(Set),Env,Pred).
trans_set(set_extension(L),Env,Pred) :- !,
gensym_if_necessary(set_ext,Pred),
maplist(trans_scalar4map(Env,Pred),L).
trans_set(union(A,B),Env,Pred) :- !,
trans_set(A,Env,P1),
trans_set(B,Env,P2),
clingo_format_comment('% union of sets~n',[]),
gen_clingo_pred_clause(union,Pred,[X],Env, (ecall(P1,[X],Env)) ),
gen_clingo_clause(Pred,[X],Env, (ecall(P2,[X],Env)) ).
trans_set(clingo_union([P1|T]),Env,Pred) :- !, % a union of a list of already translated sets; used for partition
clingo_format_comment('% union of clingo sets~n',[]),
gen_clingo_pred_clause(unions,Pred,[X],Env, (ecall(P1,[X],Env)) ),
(member(P2,T),
gen_clingo_clause(Pred,[X],Env, (ecall(P2,[X],Env)) ),
fail ; true).
trans_set(clingo_set(P),_Env,Pred) :- !, Pred=P. % already translated set
trans_set(intersection(A,B),Env,Pred) :- !,
trans_set(A,Env,P1),
trans_set(B,Env,P2),
clingo_format_comment('% intersection of sets~n',[]),
gen_clingo_pred_clause(inter,Pred,[X],Env, (ecall(P1,[X],Env),ecall(P2,[X],Env)) ).
trans_set(set_subtraction(A,B),Env,Pred) :- !, % difference set in B
trans_set(A,Env,P1),
trans_set(B,Env,P2),
clingo_format_comment('% difference of sets~n',[]),
gen_clingo_pred_clause(diff,Pred,[X],Env,
(ecall(P1,[X],Env),not(ecall(P2,[X],Env))) ). % Pred(X) :- P1(X), not P2(X).
trans_set(cartesian_product(A,B),Env,Pred) :- !,
trans_set(A,Env,P1),
trans_set(B,Env,P2),
clingo_format_comment('% Cartesian product~n',[]),
gen_clingo_pred_clause(cart,Pred,[(X,Y)],Env, (ecall(P1,[X],Env),ecall(P2,[Y],Env)) ). % Pred((X,Y)) :- P1(X), P2(Y).
trans_set(domain(A),Env,Pred) :- !,
trans_set(A,Env,P1),
clingo_format_comment('% domain of relation~n',[]),
gen_clingo_pred_clause(domain,Pred,[X],Env, ecall(P1,[(X,_)],Env) ). % Pred(X) :- P1((X,_)).
trans_set(range(A),Env,Pred) :- !,
trans_set(A,Env,P1),
clingo_format_comment('% range of relation~n',[]),
gen_clingo_pred_clause(range,Pred,[X],Env, ecall(P1,[(_,X)],Env) ). % Pred(X) :- P1((_,X)).
trans_set(image(Rel,Set),Env,Pred) :- !, % relational image B operator
trans_set(Rel,Env,P1),
trans_set(Set,Env,P2),
clingo_format_comment('% relational image~n',[]),
gen_clingo_pred_clause(image,Pred,[Y],Env,
(ecall(P2,[X],Env),ecall(P1,[(X,Y)],Env)) ). % Pred(Y) :- P1(X), P2((X,Y)).
trans_set(domain_restriction(Set,Rel),Env,Pred) :- !, % domain restriction B operator Set <| Rel
trans_set(Set,Env,P1),
trans_set(Rel,Env,P2),
clingo_format_comment('% domain restriction of relation~n',[]),
gen_clingo_pred_clause(dres,Pred,[(X,Y)],Env,
(ecall(P1,[X],Env),ecall(P2,[(X,Y)],Env)) ). % Pred((X,Y)) :- P1(X), P2((X,Y)).
trans_set(domain_subtraction(Set,Rel),Env,Pred) :- !, % domain subtraction B operator Set <<| Rel
trans_set(Set,Env,P1),
trans_set(Rel,Env,P2),
clingo_format_comment('% domain subtraction of relation~n',[]),
gen_clingo_pred_clause(dsub,Pred,[(X,Y)],Env,
(ecall(P2,[(X,Y)],Env),not(ecall(P1,[X],Env))) ). % Pred((X,Y)) :- P2((X,Y)), not P(X).
trans_set(range_restriction(Rel,Set),Env,Pred) :- !, % range restriction B operator Rel |> Set
trans_set(Set,Env,P1),
trans_set(Rel,Env,P2),
clingo_format_comment('% range restriction of relation~n',[]),
gen_clingo_pred_clause(rres,Pred,[(X,Y)],Env,
(ecall(P1,[Y],Env),ecall(P2,[(X,Y)],Env)) ). % Pred((X,Y)) :- P1(Y), P2((X,Y)).
trans_set(range_subtraction(Rel,Set),Env,Pred) :- !, % range subtraction B operator Rel |>> Set
trans_set(Set,Env,P1),
trans_set(Rel,Env,P2),
clingo_format_comment('% range subtraction of relation~n',[]),
gen_clingo_pred_clause(rsub,Pred,[(X,Y)],Env,
(ecall(P2,[(X,Y)],Env), not(ecall(P1,[Y],Env))) ). % Pred((X,Y)) :- P2((X,Y)), not P1(Y).
trans_set(composition(A,B),Env,Pred) :- !, % relational composition operator
trans_set(A,Env,P1),
trans_set(B,Env,P2),
clingo_format_comment('% relational composition~n',[]),
gen_clingo_pred_clause(comp,Pred,[(X,Z)],Env,
(ecall(P1,[(X,Y)],Env),ecall(P2,[(Y,Z)],Env)) ). % Pred((X,Z)) :- P1((X,Y)), P2((Y,Z)).
trans_set(closure(A),Env,Pred) :- !, % closure1 transitive operator
trans_set(A,Env,P1),
clingo_format_comment('% transitive closure of relation~n',[]),
gen_clingo_pred_clause(closure1,Pred,[(X,Y)],Env, ecall(P1,[(X,Y)],Env) ), % Pred((X,Y)) :- P1((X,Y)).
gen_clingo_clause(Pred,[(X,Z)],Env,
( ecall(P1,[(X,Y)],Env) , ecall(Pred,[(Y,Z)],Env)) ). % Pred((X,Z)) :- P1((X,Y)), Pred((Y,Z)).
trans_set(overwrite(A,B),Env,Pred) :- !, % relational override operator
trans_set(A,Env,P1),
trans_set(B,Env,P2),
trans_set(domain(B),Env,P3), % we need to create a separate domain encoding to be able to use it inside the "not" below
clingo_format_comment('% relational override~n',[]),
gen_clingo_pred_clause(overwr,Pred,[(X,Y)],Env, ecall(P2,[(X,Y)],Env) ), % Pred((X,Y)) :- P2((X,Y)).
gen_clingo_clause(Pred,[(X,Y)],Env,
(ecall(P1,[(X,Y)],Env),not(ecall(P3,[X],Env))) ). % Pred((X,Y)) :- P1((X,Y)), not P3(X).
trans_set(identity(A),Env,Pred) :- !, % identity operator
trans_set(A,Env,P1),
clingo_format_comment('% identity relation~n',[]),
gen_clingo_pred_clause(id,Pred,[(X,X)],Env, ecall(P1,[X],Env) ). % Pred((X,X)) :- P1(X).
trans_set(reverse(A),Env,Pred) :- !, % reverse B operator r~
trans_set(A,Env,P1),
clingo_format_comment('% relational inverse~n',[]),
gen_clingo_pred_clause(rev,Pred,[(Y,X)],Env, (ecall(P1,[(X,Y)],Env))). % Pred((Y,X)) :- P1((X,Y)).
trans_set(interval(A,B),Env,Pred) :- !,
translate_scalar(A,Env,X1,C1),
translate_scalar(B,Env,X2,C2),
clingo_format_comment('% interval~n',[]),
gen_clingo_pred_clause(interval,Pred,[X],Env, (C1,C2,'='(X,'..'(X1,X2))) ).
trans_set(global(ID),Env,Pred) :- % B value for entire global enumerated/deferred set ID
b_get_fd_type_bounds(ID,Low,Up),!,
trans_set(interval(Low,Up),Env,Pred).
trans_set(identifier(ID,global(ID)),Env,Pred) :- % TODO: proper checking of scoping
b_get_fd_type_bounds(ID,Low,Up),!,
trans_set(interval(Low,Up),Env,Pred).
trans_set(identifier(ID,_BaseType1),Env,Pred) :- clingo_local_id(ID,Env,_BaseType2,_Var), !,
add_b2asp_warning('Local identifier used as set (probably not supported):',ID),
Pred = fail.
trans_set(identifier(ID,BaseType),_Env,Pred) :- !,
gen_clingo_set_identifier(ID,BaseType,Pred).
trans_set(comprehension_set(TIds,BaseType,Body),Env,Pred) :- !,
check_empty_env(Env,TIds),
gensym(comprehension_set,CompID),
gen_clingo_set_identifier(CompID,BaseType,Pred), % create a new identifier to represent the set
create_couple(TIds,Couple),
trans_not_pred(conjunct( % state that the set contains exactly the solutions to Body
forall(TIds,member(Couple,clingo_set(Pred)), Body),
forall(TIds,Body, member(Couple,clingo_set(Pred)))), Env, ICProp),
gen_clingo_ic_constraint( ICProp ).
trans_set(X,_Env,Pred) :- %write(user_error,X),nl(user_error),
add_b2asp_error('Unsupported set: ',X), Pred=fail.