:- module bitmap. :- use_module array, bool, builtin, exception, int, private_builtin, require. :- type (bitmap:bitmap) == (array:array(int)). bitmap:num_bits(BM_3) = HeadVar__2_2 :- V_4 = 0, HeadVar__2_2 = array:elem(V_4, BM_3). bitmap:get(BM_4, I_5) = HeadVar__3_3 :- (if bitmap:is_clear(BM_4, I_5) then HeadVar__3_3 = bool:no else HeadVar__3_3 = bool:yes ). bitmap:unsafe_get(BM_4, I_5) = HeadVar__3_3 :- (if bitmap:unsafe_is_clear(BM_4, I_5) then HeadVar__3_3 = bool:no else HeadVar__3_3 = bool:yes ). bitmap:copy(BM_3) = HeadVar__2_2 :- HeadVar__2_2 = array:copy(BM_3). :- pragma termination_info(bitmap:new((builtin:in), (builtin:in)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:num_bits((bitmap:bitmap_ui)) = (builtin:out), infinite, can_loop). :- pragma termination_info(bitmap:num_bits((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(bitmap:set((bitmap:bitmap_di), (builtin:in)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:clear((bitmap:bitmap_di), (builtin:in)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:flip((bitmap:bitmap_di), (builtin:in)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:unsafe_set((bitmap:bitmap_di), (builtin:in)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:unsafe_clear((bitmap:bitmap_di), (builtin:in)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:unsafe_flip((bitmap:bitmap_di), (builtin:in)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:is_set((bitmap:bitmap_ui), (builtin:in)), finite(0, [no, no]), can_loop). :- pragma termination_info(bitmap:is_set((builtin:in), (builtin:in)), finite(0, [no, no]), can_loop). :- pragma termination_info(bitmap:is_clear((bitmap:bitmap_ui), (builtin:in)), finite(0, [no, no]), can_loop). :- pragma termination_info(bitmap:is_clear((builtin:in), (builtin:in)), finite(0, [no, no]), can_loop). :- pragma termination_info(bitmap:unsafe_is_set((bitmap:bitmap_ui), (builtin:in)), finite(0, [no, no]), can_loop). :- pragma termination_info(bitmap:unsafe_is_set((builtin:in), (builtin:in)), finite(0, [no, no]), can_loop). :- pragma termination_info(bitmap:unsafe_is_clear((bitmap:bitmap_ui), (builtin:in)), finite(0, [no, no]), can_loop). :- pragma termination_info(bitmap:unsafe_is_clear((builtin:in), (builtin:in)), finite(0, [no, no]), can_loop). :- pragma termination_info(bitmap:get((bitmap:bitmap_ui), (builtin:in)) = (builtin:out), finite(0, [no, no, no]), can_loop). :- pragma termination_info(bitmap:get((builtin:in), (builtin:in)) = (builtin:out), finite(0, [no, no, no]), can_loop). :- pragma termination_info(bitmap:unsafe_get((bitmap:bitmap_ui), (builtin:in)) = (builtin:out), finite(0, [no, no, no]), can_loop). :- pragma termination_info(bitmap:unsafe_get((builtin:in), (builtin:in)) = (builtin:out), finite(0, [no, no, no]), can_loop). :- pragma termination_info(bitmap:copy((bitmap:bitmap_ui)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:complement((bitmap:bitmap_di)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:union((bitmap:bitmap_ui), (bitmap:bitmap_di)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:intersect((bitmap:bitmap_ui), (bitmap:bitmap_di)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:difference((bitmap:bitmap_ui), (bitmap:bitmap_di)) = (bitmap:bitmap_uo), infinite, can_loop). :- pragma termination_info(bitmap:resize((bitmap:bitmap_di), (builtin:in), (builtin:in)) = (bitmap:bitmap_uo), infinite, can_loop).