kodkod2

add_global_type_relation(GType,RelationPrefix,Size,Id,In,Out) :-
    unique_identifier(RelationPrefix,GType,Id),
    add_standard_relation(global(GType),Id,Id,Size,In,Out).

add_standard_relation(BType,KType,Id,Size,In,Out) :-
    create_relation_for_type(Id,KType,Relspec),
    avl_store(BType,In,relation(Id,Size,Relspec),Out).

add_type_relation(Type,RelationName,Size,Relspec,In,Out) :-
    avl_store(Type,In,relation(RelationName,Size,Relspec),Out).

assign_element_to_atom(Elem,Type,Index,In,Out) :-
    unique_identifier(e,Elem,Id),
    create_element_relation(Id,Type,Index,Rel),
    avl_store(Elem,In,Rel,Out).

assign_elements_to_atoms(Elements,Type,IdMapIn,IdMapOut) :-
    assign_elements_to_atoms2(Elements,Type,0,IdMapIn,IdMapOut).

assign_elements_to_atoms2([],_Type,_Index,IdMap,IdMap).

assign_elements_to_atoms2([Elem|Erest],Type,Index,IdMapIn,IdMapOut) :-
    assign_element_to_atom(Elem,Type,Index,IdMapIn,IdMap),
    Index2 is Index+1,
    assign_elements_to_atoms2(Erest,Type,Index2,IdMap,IdMapOut).

assign_value_to_atom(BValue,Type,Index,VMin,VMout) :-
    avl_store(Type:BValue,VMin,Index,VMout).

assign_values_to_atoms(BValues,Type,VMin,VMout) :-
    assign_values_to_atoms2(BValues,Type,0,VMin,VMout).

assign_values_to_atoms2([],_Type,_Index,ValueMap,ValueMap).

assign_values_to_atoms2([BValue|BVrest],Type,Index,VMin,VMout) :-
    assign_value_to_atom(BValue,Type,Index,VMin,VM),
    Index2 is Index+1,
    assign_values_to_atoms2(BVrest,Type,Index2,VM,VMout).

basic_type(boolean).

basic_type(global(_)).

create_atoms_for_integers(none,Map,Map).

create_atoms_for_integers(irange(A,B),MapIn,MapOut) :-
    pow2integer_relation_kodkod_name(Relname),
    add_type_relation('__pow2integer',Relname,unknown,pow2rel(Relname,A,B),MapIn,MapOut).

create_atoms_for_intsets(none,Map,Map).

create_atoms_for_intsets(irange(A,B),MapIn,MapOut) :-
    Size is B-A+1,
    intset_relation_kodkod_name(Relname),
    add_type_relation(integer,Relname,Size,intsetrel(Relname,A,B),MapIn,MapOut).

create_atoms_for_type(boolean,TMIn,IdIn,VMIn,TMOut,IdOut,VMOut) :-
    add_standard_relation(boolean,bool,bool,2,TMIn,TMOut),
    lookup_constant_value(boolean_true,boolean,VTrue),
    lookup_constant_value(boolean_false,boolean,VFalse),
    assign_values_to_atoms([VTrue,VFalse],boolean,VMIn,VMOut),
    assign_elements_to_atoms(['__kodkod__true','__kodkod__false'],bool,IdIn,IdOut).

create_atoms_for_type(global(G),TMIn,IdIn,VMIn,TMOut,IdOut,VMOut) :-
    all_elements_of_type(G,ABValues),
    sort(ABValues,BValues), % in case of random enumeration there are problems; see test 1666
    % Note: all_elements_of_type now provides elements in sorted order; so sort/2 call is in principle not necessary anymore
    length(BValues,Size),
    add_global_type_relation(G,g,Size,RelId,TMIn,TMOut),
    assign_values_to_atoms(BValues,global(G),VMIn,VMOut),
    findall(E, is_b_global_constant(G,_,E), Elements),
    assign_elements_to_atoms(Elements,RelId,IdIn,IdOut).

create_atoms_for_types(Types,IntegerRange,IntsetRange,Typemap,Idmap,Valuemap) :-
    empty_avl(EmptyMap),
    create_atoms_for_intsets(IntsetRange,EmptyMap,TM1),
    create_atoms_for_integers(IntegerRange,TM1,TM2),
    create_atoms_for_types2(Types,TM2,EmptyMap,EmptyMap,Typemap,Idmap,Valuemap).

create_atoms_for_types2([],TypeMap,IdMap,ValueMap,TypeMap,IdMap,ValueMap).

create_atoms_for_types2([Type|Trest],TMin,IDMin,VMin,TMout,IDMout,VMout) :-
    create_atoms_for_type(Type,TMin,IDMin,VMin,TM,IDM,VM),
    create_atoms_for_types2(Trest,TM,IDM,VM,TMout,IDMout,VMout).

create_element_relation(Id,Type,Index,Rel) :-
    create_generic_relation(Id,[Type],set,exact,[tuple([Index])],Rel).

create_generic_relation(Id,Types,SetOrSingle,ExactOrSubset,TupleSet,reldef(Id,Types,SetOrSingle,ExactOrSubset,TupleSet)).

create_identifier_relation(Typemap,Bits,TId,Id,Rel) :-
    get_texpr_id(TId,Id),
    get_texpr_type(TId,Type),
    get_texpr_info(TId,Info),
    unique_identifier(id,Id,RelId),
    is_set_or_single(Type,SetOrSingle,RestType),
    create_identifier_relation2(RestType,SetOrSingle,RelId,Info,Bits,Typemap,Rel).

create_identifier_relation2(integer,set,RelId,_Info,_Bits,_Typemap,Rel) :-
    !,intset_relation_kodkod_name(Type),
    create_generic_relation(RelId,[Type],set,subset,full,Rel).

create_identifier_relation2(integer,single,RelId,Info,Bits,_Typemap,Rel) :-
    !,
    % if the type does not fit into the bitset range, the choice is clear:
    % we have to use the pow2 representation
    (in_bitrange(Info,Bits) -> intset_relation_kodkod_name(Type) ; pow2integer_relation_kodkod_name(Type)),
    create_generic_relation(RelId,[Type],single,subset,full,Rel).

create_identifier_relation2(RestType,SetOrSingle,RelId,_Info,_Bits,Typemap,Rel) :-
    extract_ktypes(RestType,Typemap,Types),
    create_generic_relation(RelId,Types,SetOrSingle,subset,full,Rel).

create_identifier_relations(TIds,Typemap,Bits,IdMapIn,IdMapOut) :-
    maplist(create_identifier_relation(Typemap,Bits),TIds,Ids,Rels),
    foldl(store_in_avl,Ids,Rels,IdMapIn,IdMapOut).

create_relation_for_type(Id,Type,Rel) :-
    create_generic_relation(Id,[Type],set,exact,full,Rel).

extract_integer_as_set(TExpr,IntRangeI,IntRangeO) :-
    extract_finite_integer_range(TExpr,[],IntRange),
    merge_integer_info(IntRangeI,IntRange,IntRangeO).

extract_ktypes(couple(A,B),Typemap,Types) :- !,
    extract_ktypes(A,Typemap,ATypes),
    append(ATypes,BTypes,Types),
    extract_ktypes(B,Typemap,BTypes).

extract_ktypes(Type,Typemap,[Name]) :-
    avl_fetch(Type,Typemap,Relation),
    Relation = relation(Name,_Size,_Relspec).

extract_type_information(Type,TExpr,Names,UsedTypesA,IntRangeA,BitRangeA) :-
    extract_type_information2(Type,TExpr,Names,[],UsedTypesA,IntRangeA,BitRangeA).

extract_type_information2(T,_,_,_,[T],none,none) :-
    basic_type(T).

extract_type_information2(integer,TExpr,_,Scope,[],IntRange,none) :-
    extract_finite_integer_range(TExpr,Scope,IntRange).

extract_type_information2(set(Type),TExpr,_,Scope,UsedTypes,IntRange,BitRange) :-
    extract_type_information_set(Type,TExpr,[elem|Scope],UsedTypes,IntRange,BitRange).

extract_type_information2(seq(Type),TExpr,_,Scope,UsedTypes,IntRange,BitRange) :-
    extract_type_information2(set(couple(integer,Type)),TExpr,[],Scope,UsedTypes,IntRange,BitRange).

extract_type_information2(couple(A,B),TExpr,_,Scope,UsedTypes,IntRange,BitRange) :-
    extract_type_information2(A,TExpr,[],[left|Scope],TypesA,IntRangeA,BitRangeA),
    extract_type_information2(B,TExpr,[],[right|Scope],TypesB,IntRangeB,BitRangeB),
    merge_integer_info(IntRangeA,IntRangeB,IntRange),
    merge_integer_info(BitRangeA,BitRangeB,BitRange),
    ord_union(TypesA,TypesB,UsedTypes).

extract_type_information2(pred,_Expr,Names,_Scope,Types,IntRange,BitRange) :-
    treat_quantified_integers_as_sets(Names,Types,IntRange,BitRange).

extract_type_information_set(T,_,_,[T],none,none) :-
    basic_type(T).

extract_type_information_set(integer,TExpr,Scope,[],BitRange,BitRange) :-
    extract_finite_integer_range(TExpr,Scope,BitRange).

extract_type_information_set(couple(A,B),TExpr,Scope,UsedTypes,IntRange,BitRange) :-
    extract_type_information_set(A,TExpr,[left|Scope],TypesA,IntRangeA,BitRangeA),
    extract_type_information_set(B,TExpr,[right|Scope],TypesB,IntRangeB,BitRangeB),
    merge_integer_info(IntRangeA,IntRangeB,IntRange),
    merge_integer_info(BitRangeA,BitRangeB,BitRange),
    ord_union(TypesA,TypesB,UsedTypes).

extract_used_types(TExpr,UsedTypes,IntegerRange,BitstringRange) :-
    % first adapt the output of the interval analysis to our needs
    % (see the comments in kodkod_integer_recalc for details)
    integer_recalc(TExpr,RExpr),
    % now extract the used types
    extract_used_types1(RExpr,UsedTypes,IntegerRange,BitstringRange).

extract_used_types1(TExpr,UsedTypes,IntegerRange,BitstringRange) :-
    syntaxtraversion(TExpr,Expr,Type,_,Subs1,Names),
    ( higher_order_exception(Expr,Subs) ->
    UsedTypesA=[],IntRangeA=none,BitRangeA=none
    ; extract_type_information(Type,TExpr,Names,UsedTypesA,IntRangeA,BitRangeA) ->
    Subs1 = Subs
    ;
    throw(kodkod(unsupported_type(Type)))),
    extract_used_types_l(Subs,UsedTypesA,IntRangeA,BitRangeA,
    UsedTypes,IntegerRange,BitstringRange).

extract_used_types_l([],Types,IntRange,BitRange,Types,IntRange,BitRange).

extract_used_types_l([Expr|Erest],TypesI,IntRangeI,BitRangeI,Types,IntRange,BitRange) :-
    extract_used_types1(Expr,TypesA,IntRangeA,BitRangeA),
    merge_integer_info(IntRangeI,IntRangeA,IntRangeB),
    merge_integer_info(BitRangeI,BitRangeA,BitRangeB),
    ord_union(TypesI,TypesA,TypesB),
    extract_used_types_l(Erest,TypesB,IntRangeB,BitRangeB,Types,IntRange,BitRange).

higher_order_exception(member(Elem,THOSet),[Elem|Subsets]) :-
    get_texpr_expr(THOSet,HOSet),
    higher_order_exception2(HOSet,Subsets).

higher_order_exception2(total_function(Dom,Ran),[Dom,Ran]).

higher_order_exception2(total_injection(Dom,Ran),[Dom,Ran]).

higher_order_exception2(total_surjection(Dom,Ran),[Dom,Ran]).

higher_order_exception2(total_bijection(Dom,Ran),[Dom,Ran]).

higher_order_exception2(partial_function(Dom,Ran),[Dom,Ran]).

higher_order_exception2(partial_injection(Dom,Ran),[Dom,Ran]).

higher_order_exception2(partial_surjection(Dom,Ran),[Dom,Ran]).

higher_order_exception2(partial_bijection(Dom,Ran),[Dom,Ran]).

higher_order_exception2(total_relation(Dom,Ran),[Dom,Ran]).

higher_order_exception2(surjection_relation(Dom,Ran),[Dom,Ran]).

in_bitrange(Info,irange(BLow,BUp)) :-
    integer_range(Info,Low,Up),
    BLow =< Low,
    Up =< BUp.

integer_range(Info,Lower,Upper) :-
    memberchk(analysis(A),Info),
    memberchk(interval:irange(Lower,Upper),A).

is_integer_expr(TExpr) :- get_texpr_type(TExpr,integer).

is_set_or_single(seq(T),set,couple(integer,T)) :- !.

is_set_or_single(set(T),set,T) :- !.

is_set_or_single(T,single,T).

lookup_constant_value(Expr,Type,Value) :-
    create_texpr(Expr,Type,[],TExpr),
    empty_state(Empty),
    b_compute_expression_nowf(TExpr,Empty,Empty,Value,'KODKOD constant',0).

store_in_avl(Id,Rel,In,Out) :-
    avl_store(Id,In,Rel,Out).

treat_quantified_integers_as_sets(Names,[],none,Range) :-
    include(is_integer_expr,Names,Integers),
    foldl(extract_integer_as_set,Integers,none,Range).