kodkod_translate

add_var_to_environment(Id,Ref,kenv(Typemap,Idmap,VarmapIn),kenv(Typemap,Idmap,VarmapOut)) :-
    avl_store(Id,VarmapIn,Ref,VarmapOut).

all_disjunct(Sets,K) :-
    all_disjunct2(Sets,Dis,[]),
    kodkod_conjunction(Dis,K).

all_disjunct2([]) --> !.

all_disjunct2([S|Rest]) -->
    all_disjunct3(Rest,S),
    all_disjunct2(Rest).

all_disjunct3([],_) --> !.

all_disjunct3([B|Rest],A) -->
    [no(intersection(A,B))],
    all_disjunct3(Rest,A).

check_side_condition(none,_Expr,_).

check_side_condition(cond(_,_),Expr,Info) :-
    kodkod_short(Expr,_,cond(Msg,Condition)),
    ( call(Condition) -> true
    ;
    translate_bexpression(Expr,PPExpr),
    throw(kodkod(side_condition(Msg,PPExpr,Info)))).

create_empty_set([Type],R) :- !,R=empty:rel([Type]).

create_empty_set([Type|Rest],product(empty:rel([Type]),R)) :-
    create_empty_set(Rest,R).

create_environment(Typemap,Idmap,kenv(Typemap,Idmap,Varmap)) :-
    empty_avl(Varmap).

enumerate(0,_,[]) :- !.

enumerate(N,S,[S|Rest]) :- N2 is N-1, S2 is S+1, enumerate(N2,S2,Rest).

find_in(Formula,Id,Expression,NewFormula) :-
    disassemble_conjunction(Formula,Parts),
    find_in2(Parts,Id,Expression,Rest),
    kodkod_conjunction(Rest,NewFormula).

find_in2([in(varref(Id),Expr)|Rest], Id, Expr, Rest) :- !.

find_in2([Pred|Rest], Id, Expr, [Pred|Result]) :-
    find_in2(Rest,Id,Expr,Result).

is_binary_relation(Type,_) :- type_arity(Type,2),!.

is_binary_relation(Type,Info) :-
    pretty_type(Type,PType),
    throw(kodkod(side_condition('Functions are only supported for binary relations',PType,Info))).

k_is_bijective(F,R,Type,and(Inj,Surj)) :-
    k_is_injective(F,Inj), k_is_surjective(F,R,Type,Surj).

k_is_injective(F,in(join(F,transpose(F)),iden)).

k_is_surjective(F,R,set(Type),in(R,Range)) :-
    kodkod_range(F,Type,Range).

kodkod_declaration(integer,_KId,_Analysis,_Env,KCond,KCond,Mult,Expr) :-
    % TODO: we have to make a decision whether a quantified integer
    % variable should be the bit-representation of the value
    % (for variables that can take large values)
    % or a the item of the integer relation.
    % currently we do only the latter:
    !,Mult = one,
    intset_relation_kodkod_name(IntsetRelation),
    Expr = relref(IntsetRelation).

kodkod_declaration(Type,KId,_Analysis,Env,KCond,NewKCond,Mult,Expr) :-
    (Type=set(_) -> Mult=set; Mult=one),
    ( find_in(KCond,KId,Expr,NewKCond) ->
    true
    ;
    % here we have to insert a possible choice for
    % integer variables. That possible choice should be returned
    % as a variable and later its value determine the outcome
    % of the choice.
    kodkod_type(Type,Env,Expr),
    NewKCond = KCond).

kodkod_declarations1([],SubEnv,SubEnv,[]).

kodkod_declarations1([TExpr|IRest],
    Env,Env2,
    [provdecl(KId,Type,Analysis)|DRest]) :-
    get_texpr_id(TExpr,Id),
    get_texpr_type(TExpr,Type),
    get_texpr_info(TExpr,Info),
    (memberchk(analysis(Analysis),Info) -> true ; Analysis=[]),
    unique_identifier(v,Id,KId),
    add_var_to_environment(Id,KId,Env,SubEnv),
    kodkod_declarations1(IRest,SubEnv,Env2,DRest).

kodkod_declarations2([],_,KCond,KCond,[]).

kodkod_declarations2([provdecl(KId,Type,Analysis)|PRest],
    Env,KCond,KCond2,
    [decl(KId,Arity,Mult,Expr)|DRest]) :-
    type_arity(Type,Arity),
    kodkod_declaration(Type,KId,Analysis,Env,KCond,NewKCond,Mult,Expr),
    kodkod_declarations2(PRest,Env,NewKCond,KCond2,DRest).

kodkod_domain(KRel,BType,prj(Positions,KRel)) :-
    remove_optional_set(BType,couple(DType,_RType)),
    type_arity(DType,Arity),enumerate(Arity,0,Positions).

kodkod_extension_set([],none) :- !.

kodkod_extension_set([Elem],Elem) :- !.

kodkod_extension_set([Elem|Rest],union(Elem,Ext)) :-
    kodkod_extension_set(Rest,Ext).

kodkod_function_application(BFun,BArg,Env,K) :-
    kodkod_translate1(BFun,Env,KFun),
    kodkod_translate1(BArg,Env,KArg),
    get_texpr_type(BArg,ArgType), type_arity(ArgType,ArgArity),
    get_texpr_type(BFun,FunType), type_arity(FunType,FunArity),
    kodkod_function_application_aux(ArgArity,FunArity,KFun,KArg,K).

kodkod_function_application_aux(1,_,KFun,KArg,K) :- !,
    K = join(KArg,KFun).

kodkod_function_application_aux(ArgArity,FunArity,KFun,KArg,K) :-
    % We translate f(x) resp. f[{x}] to
    % prj( nx..(nf-1), { e : f | prj( 0..(nx-1), e ) = x } )
    % with nf resp. nx being the arity of f resp. x
    K = prj(RightPos,CompSet),
    CompSet = comp([decl(KId,FunArity,one,KFun)],equals(prj(LeftPos,varref(KId)),KArg)),
    % LeftPos is 0..(nx-1) (contains ArgArity elements starting with 0)
    enumerate(ArgArity,0,LeftPos),
    % RightPos is nx..(nf-1) (contains FunArity-ArgArity elements starting with nx)
    RemainingPos is FunArity-ArgArity,
    enumerate(RemainingPos,ArgArity,RightPos),
    % e is some unique identifier
    unique_identifier(KId).

kodkod_range(KRel,BType,prj(Positions,KRel)) :-
    remove_optional_set(BType,couple(DType,RType)),
    type_arity(DType,Start),type_arity(RType,Arity),
    enumerate(Arity,Start,Positions).

kodkod_reverse(BArg,Env,K) :-
    kodkod_translate1(BArg,Env,KArg),
    get_texpr_type(BArg,ArgType), type_arity(ArgType,ArgArity),
    kodkod_reverse_aux(ArgArity,KArg,K).

kodkod_reverse_aux(2,KArg,transpose(KArg)) :- !.

kodkod_reverse_aux(Arity,KArg,prj(Rev,KArg)) :-
    enumerate(Arity,0,Positions),
    reverse(Positions,Rev).

kodkod_short(truth,true).

kodkod_short(falsity,false).

kodkod_short(negation(A),not(A)).

kodkod_short(conjunct(A,B),and(A,B)).

kodkod_short(disjunct(A,B), or(A,B)).

kodkod_short(implication(A,B),implies(A,B)).

kodkod_short(equivalence(A,B), iff(A,B)).

kodkod_short(equal(A,B),equals(A,B)).

kodkod_short(member(A,B),in(A,B)).

kodkod_short(subset(A,B),K) :- kodkod_short(member(A,B),K).

kodkod_short(not_subset(A,B),not(K)) :- kodkod_short(subset(A,B),K).

kodkod_short(subset_strict(A,B),and(in(A,B),not(equals(A,B)))).

kodkod_short(not_subset_strict(A,B),or(not(in(A,B)),equals(A,B))).

kodkod_short(cartesian_product(A,B),product(A,B)).

kodkod_short(intersection(A,B),intersection(A,B)).

kodkod_short(union(A,B),union(A,B)).

kodkod_short(closure(E),closure(E)).

kodkod_short(set_subtraction(A,B),difference(A,B)).

kodkod_short(overwrite(A,B),overwrite(A,B)).

kodkod_short(couple(A,B),product(A,B)).

kodkod_short(card(X),card(X)).

kodkod_short(size(X),card(X)).

kodkod_short(greater(A,B),gt(A,B)).

kodkod_short(greater_equal(A,B),gte(A,B)).

kodkod_short(less(A,B),lt(A,B)).

kodkod_short(less_equal(A,B),lte(A,B)).

kodkod_short(add(A,B),add(A,B)).

kodkod_short(minus(A,B),sub(A,B)).

kodkod_short(multiplication(A,B),mul(A,B)).

kodkod_short(div(A,B),div(A,B)).

kodkod_short(floored_div(A,B),div(A,B)) :-
    add_warning(kodkod_translate,'Translating floored division as truncated division: ',div(A,B)).

kodkod_short(modulo(A,B),mod(A,B)).

kodkod_short(unary_minus(A),sub(int(0),A)).

kodkod_short(B,K,none) :- kodkod_short(B,K),!.

kodkod_short(B,K,cond(Msg,Cond)) :- kodkod_short(B,K,Msg,Cond).

kodkod_short(identity(A),intersection(product(A,A),iden),
    'Identity is supported only on unary sets',
    side_condition_type_arity(A,1)).

kodkod_short(reflexive_closure(A),closure(union(intersection(product(All,All),iden),A)),
    'Reflexive closure is supported only on binary relations on unary sets',
    side_condition_type_arity(A,2)) :- All=union(prj([0],A),prj([1],A)).

kodkod_translate(TExpr,Typemap,Idmap,KExpr) :-
    create_environment(Typemap,Idmap,KEnv),
    kodkod_translate1(TExpr,KEnv,KExpr).

kodkod_translate1(TExpr,Env,KExpr) :-
    get_texpr_expr(TExpr,Expr),
    get_texpr_type(TExpr,Type1), remove_seq_type(Type1,Type),
    get_texpr_info(TExpr,Info),
    kodkod_translate2(Expr,Type,Info,Env,KExpr1),
    % enforce the use of integer atoms for integers used in sets
    ( Type = set(integer), KExpr1 \= _:_ ->
    KExpr = KExpr1:rel([IntAtoms]),
    intset_relation_kodkod_name(IntAtoms)
    ;
    KExpr = KExpr1).

kodkod_translate2(member(BElem,BSet),pred,Info,Env,K) :-
    get_texpr_expr(BSet,BFun),
    BFun =.. [FunFunctor,BDom,BRange],
    KFun =.. [FunFunctor,KDom,KRange],
    get_texpr_type(BSet,Type),
    kodkod_translate_binary_membership(KFun,KElem,Type,Info,K),!,
    kodkod_translate1(BElem,Env,KElem),
    kodkod_translate1(BDom,Env,KDom),
    kodkod_translate1(BRange,Env,KRange).

kodkod_translate2(not_member(BElem,BSet),pred,Info,Env,not(K)) :-
    !,kodkod_translate2(member(BElem,BSet),pred,Info,Env,K).

kodkod_translate2(domain_restriction(Dom,Rel),set(couple(_,RhType)),_,Env,
    intersection(product(KDom,relref(KRhRel)),KRel)) :-
    !,kodkod_translate1(Dom,Env,KDom),
    kodkod_translate1(Rel,Env,KRel),
    lookup_type_relation(RhType,Env,KRhRel).

kodkod_translate2(domain_subtraction(Dom,Rel),set(couple(_,RhType)),_,Env,
    intersection(product(difference(univ,KDom),relref(KRhRel)),KRel)) :-
    !,kodkod_translate1(Dom,Env,KDom),
    kodkod_translate1(Rel,Env,KRel),
    lookup_type_relation(RhType,Env,KRhRel).

kodkod_translate2(range_restriction(Rel,Dom),set(couple(LhType,_)),_,Env,
    intersection(KRel,product(relref(KLhRel),KDom))) :-
    !,kodkod_translate1(Dom,Env,KDom),
    kodkod_translate1(Rel,Env,KRel),
    lookup_type_relation(LhType,Env,KLhRel).

kodkod_translate2(range_subtraction(Rel,Dom),set(couple(LhType,_)),_,Env,
    intersection(KRel,product(relref(KLhRel),difference(univ,KDom)))) :-
    !,kodkod_translate1(Dom,Env,KDom),
    kodkod_translate1(Rel,Env,KRel),
    lookup_type_relation(LhType,Env,KLhRel).

kodkod_translate2(identifier(Id),_BType,_Info,Env,Ref) :- !,
    ( lookup_var(Id,Env,Varname) ->
    Ref = varref(Varname)
    ; lookup_id_relation(Id,Env,Relname,_KTypes) ->
    Ref = relref(Relname)
    ; lookup_type_relation(global(Id),Env,Relname) ->
    Ref = relref(Relname)).

kodkod_translate2(set_extension([]),BType,Info,Env,Result) :-
    !, % normally should not happen, unless AST constructed by hand
    kodkod_translate2(empty_set,BType,Info,Env,Result).

kodkod_translate2(set_extension(List),_BType,_,Env,Result) :-
    !, kodkod_translate_l(List,Env,KList),
    kodkod_extension_set(KList,Result).

kodkod_translate2(forall(BIds,_,_),pred,_,_Env,true) :-
    % If there is an identifier without possible solution, the result is always true
    somechk(is_inconsistent_expression,BIds),!.

kodkod_translate2(forall(BIds, Condition, Predicate),pred,_,Env,
    forall(Decls,Result)) :-
    !,kodkod_declarations1(BIds,Env,Subenv,ProvDecls),
    kodkod_translate1(Condition,Subenv,KCond),
    kodkod_translate1(Predicate,Subenv,KPred),
    kodkod_declarations2(ProvDecls,Env,KCond,NewKCond,Decls),
    kodkod_implication(NewKCond,KPred,Result).

kodkod_translate2(exists(BIds,_),pred,_,_Env,false) :-
    % If there is an identifier without possible solution, the result is always false
    somechk(is_inconsistent_expression,BIds),!.

kodkod_translate2(exists([BId], Membership),pred,_,Env,some(KSet)) :-
    % translate #e.e:M to some(M)
    get_texpr_expr(Membership,member(Elem,Set)),
    get_texpr_id(BId,Id),get_texpr_id(Elem,Id),!,
    kodkod_translate1(Set,Env,KSet).

kodkod_translate2(exists(BIds, Predicate),pred,_,Env,exists(Decls,Result)) :-
    !,kodkod_declarations1(BIds,Env,Subenv,ProvDecls),
    kodkod_translate1(Predicate,Subenv,KPred),
    kodkod_declarations2(ProvDecls,Env,KPred,Result,Decls).

kodkod_translate2(comprehension_set(BIds,_),BType,Info,Env,KEmptySet) :-
    % If there is an identifier without possible solution, the result is always empty
    somechk(is_inconsistent_expression,BIds),!,
    kodkod_translate2(empty_set,BType,Info,Env,KEmptySet).

kodkod_translate2(comprehension_set(BIds,Predicate),set(_BType),_,Env,
    comp(Decls,Result)) :-
    !,kodkod_declarations1(BIds,Env,Subenv,ProvDecls),
    kodkod_translate1(Predicate,Subenv,KPred),
    kodkod_declarations2(ProvDecls,Env,KPred,Result,Decls).

kodkod_translate2(domain(Rel),_,_,Env,K) :-
    !,get_texpr_type(Rel,RelType),
    kodkod_domain(KRel,RelType,K),
    kodkod_translate1(Rel,Env,KRel).

kodkod_translate2(range(Rel),_,_,Env,K) :-
    !,get_texpr_type(Rel,RelType),
    kodkod_range(KRel,RelType,K),
    kodkod_translate1(Rel,Env,KRel).

kodkod_translate2(first_of_pair(Couple),Type,Info,Env,K) :-
    !,kodkod_translate2(domain(Couple),Type,Info,Env,K).

kodkod_translate2(second_of_pair(Couple),Type,Info,Env,K) :-
    !,kodkod_translate2(range(Couple),Type,Info,Env,K).

kodkod_translate2(composition(A,B),_BType,_,Env,join(KA,KB)) :-
    get_texpr_set_type(A,couple(_,IType)),
    type_arity(IType,1),!,
    kodkod_translate1(A,Env,KA),
    kodkod_translate1(B,Env,KB).

kodkod_translate2(function(BFun,BArg),_BType,_,Env,Res) :-
    !, kodkod_function_application(BFun,BArg,Env,Res).

kodkod_translate2(image(BRel,BArg),_BType,_,Env,Res) :-
    !, kodkod_function_application(BRel,BArg,Env,Res).

kodkod_translate2(reverse(BRel),_BType,_,Env,Res) :-
    !, kodkod_reverse(BRel,Env,Res).

kodkod_translate2(integer(I),integer,_,_Env,int(I)) :- !.

kodkod_translate2(unary_minus(TExpr),integer,_,_Env,int(N)) :-
    % Expressions of the form "-(1)" are translated to "-1"
    % there is another rule below for other forms of unary minus (translating "-x" to "0-x")
    get_texpr_expr(TExpr,integer(P)),!,N is -P.

kodkod_translate2(general_sum([TId],TPred,Expr),integer,_,Env,sum(KSet)) :-
    % we support only a restricted sort of the general sum:
    % SIGMA (x).(x:S|x)
    % The rewriting rules (see kodkod2.pl) convert the more general form "SIGMA (x).(P|x)"
    % into this form by "SIGMA (x).(x:{x|P}|x)"
    % The expression must only contain the quantified variable:
    get_texpr_id(TId,Id), get_texpr_id(Expr,Id),!,
    % Simple form: the predicate is of the form x:S
    get_texpr_expr(TPred,member(TElem,TSet)),get_texpr_id(TElem,Id),
    kodkod_translate1(TSet,Env,KSet).

kodkod_translate2(boolean_true,boolean,_,Env,relref(Relname)) :- !,
    lookup_id_relation('__kodkod__true',Env,Relname,_KTypes).

kodkod_translate2(boolean_false,boolean,_,Env,relref(Relname)) :- !,
    lookup_id_relation('__kodkod__false',Env,Relname,_KTypes).

kodkod_translate2(bool_set,set(boolean),_,Env,relref(Relname)) :- !,
    lookup_type_relation(boolean,Env,Relname).

kodkod_translate2(empty_set,set(T),_,Env,Empty) :- !,
    kodkod_type_as_list(T,Env,Typelist),
    create_empty_set(Typelist,Empty).

kodkod_translate2(partition(Set,Subsets),_,_,Env,and(KEquals,KDisjunct)) :- !,
    kodkod_translate_l([Set|Subsets],Env,[KSet|KSubsets]),
    kodkod_extension_set(KSubsets,KUnion),
    KEquals = equals(KSet,KUnion),
    all_disjunct(KSubsets,KDisjunct).

kodkod_translate2(convert_bool(BCond),boolean,_,Env,if(KCond,KTrue,KFalse)) :- !,
    kodkod_translate1(BCond,Env,KCond),
    kodkod_translate2(boolean_true,boolean,[],Env,KTrue),
    kodkod_translate2(boolean_false,boolean,[],Env,KFalse).

kodkod_translate2(concat(BA,BB),_,_,Env,union(KA,join(Adder,KB))) :- !,
    % To compute A^B, we use a form A \/ Adder[B]
    kodkod_translate1(BA,Env,KA),
    kodkod_translate1(BB,Env,KB),
    intset_relation_kodkod_name(I),
    % Adder is a set of the form {a,b | a=b+card(A)}
    Adder = comp([decl(lhr,1,one,relref(I)),decl(rhr,1,one,relref(I))],
    equals(sum(varref(lhr)),add(sum(varref(rhr)),card(KA)))).

kodkod_translate2(value(V),Type,_Info,Env,K) :- ground(V), %print(try_translate_value(V)),nl,
    translate_value_to_kodkod(Type,Env,V,K),!.

kodkod_translate2(value(Val),Type,Infos,Env,K) :-
    was_identifier(Val,Infos,ID),!, % identifier was compiled to value; this is a bit dangerous; we should ensure that the identifier ID is used only once
    %print(kodkod_value_as_id(V,ID)),nl,
    kodkod_translate2(identifier(ID),Type,Infos,Env,K).

kodkod_translate2(event_b_identity,set(couple(Type,Type)),Info,Env,K) :- !,
    create_maximal_type_set(Type,TSet),
    kodkod_translate2(identity(TSet),set(couple(Type,Type)),Info,Env,K).

kodkod_translate2(external_pred_call('LEQ_SYM',_),Type,Info,Env,K) :- !,
    kodkod_translate2(truth,Type,Info,Env,K).

kodkod_translate2(external_pred_call('LEQ_SYM_BREAK',_),Type,Info,Env,K) :- !,
    kodkod_translate2(truth,Type,Info,Env,K).

kodkod_translate2(Expr,_,Info,Env,Result) :-
    functor(Expr,Functor,Arity),
    functor(Tmp,Functor,Arity),
    kodkod_short(Tmp,_,SC),!,
    check_side_condition(SC,Expr,Info),
    Expr =.. [Functor|Args],
    same_length(Args,TArgs),
    Lookup =.. [Functor|TArgs],
    kodkod_translate_l(Args,Env,TArgs),
    kodkod_short(Lookup,Result,_).

kodkod_translate2(E,T,I,_,_) :-
    create_texpr(E,T,I,TE),
    %print(expr(E,T)),nl,
    throw(kodkod(unsupported_expression(TE))).

kodkod_translate_binary_membership(partial_function(D,R),F,T,Info,pfunc(F,D,R)) :- is_binary_relation(T,Info).

kodkod_translate_binary_membership(total_function(D,R),F,T,Info,func(F,D,R)) :- is_binary_relation(T,Info).

kodkod_translate_binary_membership(partial_injection(D,R),F,T,Info,and(pfunc(F,D,R),Inj)) :-
    is_binary_relation(T,Info),k_is_injective(F,Inj).

kodkod_translate_binary_membership(total_injection(D,R),F,T,Info,and(func(F,D,R),Inj)) :-
    is_binary_relation(T,Info),k_is_injective(F,Inj).

kodkod_translate_binary_membership(partial_surjection(D,R),F,T,Info,and(pfunc(F,D,R),Surj)) :-
    is_binary_relation(T,Info),k_is_surjective(F,R,T,Surj).

kodkod_translate_binary_membership(total_surjection(D,R),F,T,Info,and(func(F,D,R),Surj)) :-
    is_binary_relation(T,Info),k_is_surjective(F,R,T,Surj).

kodkod_translate_binary_membership(partial_bijection(D,R),F,T,Info,and(pfunc(F,D,R),Bij)) :-
    is_binary_relation(T,Info),k_is_bijective(F,R,T,Bij).

kodkod_translate_binary_membership(total_bijection(D,R),F,T,Info,and(func(F,D,R),Bij)) :-
    is_binary_relation(T,Info),k_is_bijective(F,R,T,Bij).

kodkod_translate_binary_membership(total_relation(D,R),F,set(T),_Info,and(equals(Dom,D),in(Ran,R))) :-
    kodkod_domain(F,T,Dom), kodkod_range(F,T,Ran).

kodkod_translate_binary_membership(surjection_relation(D,R),F,set(T),_Info,and(in(Dom,D),equals(Ran,R))) :-
    kodkod_domain(F,T,Dom), kodkod_range(F,T,Ran).

kodkod_translate_l([],_,[]).

kodkod_translate_l([E|ERest],Env,[K|KRest]) :-
    kodkod_translate1(E,Env,K),
    kodkod_translate_l(ERest,Env,KRest).

kodkod_type(T,Env,K) :-
    remove_optional_set(T,T2),
    kodkod_type2(T2,T2,Env,K).

kodkod_type2(couple(A,B),_,Env,product(KA,KB)) :- !,
    kodkod_type2(A,A,Env,KA),
    kodkod_type2(B,B,Env,KB).

kodkod_type2(Type,_,Env,relref(Ref)) :-
    lookup_type_relation(Type,Env,Ref),!.

kodkod_type2(_,T,_Env,_Ref) :-
    throw(kodkod(unsupported_type(T))).

kodkod_type_as_list(T,Env,TypeList) :-
    remove_optional_set(T,T2),
    kodkod_type_as_list2(T2,Env,TypeList).

kodkod_type_as_list2(couple(A,B),Env,TypeList) :- !,
    kodkod_type_as_list2(A,Env,ATL),
    kodkod_type_as_list2(B,Env,BTL),
    append(ATL,BTL,TypeList).

kodkod_type_as_list2(BType,Env,[KType]) :-
    lookup_type_relation(BType,Env,KType).

lookup_id_relation(Id,kenv(_,Idmap,_),Relname,Types) :-
    avl_fetch(Id,Idmap,reldef(Relname,Types,_,_,_)).

lookup_type_relation(Type,kenv(Typemap,_,_),Relname) :-
    avl_fetch(Type,Typemap,V),
    V = relation(Relname,_Size,_Relspec).

lookup_var(Id,kenv(_,_,Varmap),Varname) :-
    avl_fetch(Id,Varmap,Varname).

remove_optional_set(set(A),B) :- !,A=B.

remove_optional_set(T,T).

remove_seq_type(seq(T),Set) :- !,Set=set(couple(integer,T)).

remove_seq_type(T,T).

side_condition_type_arity(Expr,Arity) :-
    get_texpr_type(Expr,Type),
    type_arity(Type,Arity).

translate_boolean(pred_true,Env,relref(Relname)) :-
    lookup_id_relation('__kodkod__true',Env,Relname,_KTypes).

translate_boolean(pred_false,Env,relref(Relname)) :-
    lookup_id_relation('__kodkod__false',Env,Relname,_KTypes).

translate_value_to_kodkod(integer,_Env,int(I),int(I)) :- !.

translate_value_to_kodkod(set(Type),Env,V,K) :- !,
    kodkod_type_as_list(Type,Env,Typelist),
    expand_custom_set_to_list(V,List),
    maplist(translate_value_to_kodkod1(Type,Env),List,KList),
    ( KList = [] -> create_empty_set(Typelist,K)
    ; KList = [H|T] -> foldl(union_kvalues,T,H,K)).

translate_value_to_kodkod(Type,Env,V,K) :-
    translate_value_to_kodkod1(Type,Env,V,K).

translate_value_to_kodkod1(integer,_Env,int(I),int(I):rel([IntAtoms])) :- !,
    intset_relation_kodkod_name(IntAtoms).

translate_value_to_kodkod1(couple(TA,TB),Env,(A,B),product(KA,KB)) :- !,
    translate_value_to_kodkod1(TA,Env,A,KA),
    translate_value_to_kodkod1(TB,Env,B,KB).

translate_value_to_kodkod1(global(GS),Env,fd(Nr,GS),Res) :- !,
    is_b_global_constant(GS,Nr,CstId),
    lookup_id_relation(CstId,Env,Relname,_KTypes), Res=relref(Relname).

translate_value_to_kodkod1(boolean,Env,Val,KodkodResult) :- !,
    translate_boolean(Val,Env,KodkodResult).

translate_value_to_kodkod1(Type,_,_,_) :-
    format('Cannot translate type in value/1 to kodkod: ~w~n',[Type]),fail.

type_arity(set(T),A) :- type_arity(T,A).

type_arity(integer,1).

type_arity(boolean,1).

type_arity(global(_),1).

type_arity(couple(A,B),Arity) :-
    type_arity(A,AA),type_arity(B,AB),Arity is AA+AB.

union_kvalues(A,B,union(A,B)).

was_identifier(_V,Infos,ID) :- member(was_identifier(ID),Infos).

was_identifier(Val,_,GS) :- nonvar(Val), Val=global_set(GS).