:- module sparse_bitset. :- use_module builtin, enum, int, list, private_builtin, require, std_util, term. :- type (sparse_bitset:sparse_bitset(T)) ---> sparse_bitset((list:list((sparse_bitset:bitset_elem)))) . :- type (sparse_bitset:fold_direction) ---> low_to_high ; high_to_low . :- type (sparse_bitset:bitset_impl) == (list:list((sparse_bitset:bitset_elem))). :- type (sparse_bitset:bitset_elem) ---> bitset_elem((sparse_bitset:offset) :: int, (sparse_bitset:bits) :: int) . :- func sparse_bitset:foldl_2((func(T_1, U_2) = U_2), (list:list((sparse_bitset:bitset_elem))), U_2) = U_2 <= (enum:enum(T_1)). :- mode sparse_bitset:foldl_2((builtin:in), (builtin:in), (builtin:in)) = (builtin:out) is det. :- pragma type_spec((sparse_bitset:foldl_2)/3, (T_1 = (term:var(V_3))), (sparse_bitset:'TypeSpecOf__pred_or_func__foldl_2__[T = var(V_2)]')). :- pragma type_spec((sparse_bitset:foldl_2)/3, (T_1 = int), (sparse_bitset:'TypeSpecOf__pred_or_func__foldl_2__[T = int]')). :- func sparse_bitset:foldr_2((func(T_1, U_2) = U_2), (list:list((sparse_bitset:bitset_elem))), U_2) = U_2 <= (enum:enum(T_1)). :- mode sparse_bitset:foldr_2((builtin:in), (builtin:in), (builtin:in)) = (builtin:out) is det. :- pragma type_spec((sparse_bitset:foldr_2)/3, (T_1 = (term:var(V_3))), (sparse_bitset:'TypeSpecOf__pred_or_func__foldr_2__[T = var(V_2)]')). :- pragma type_spec((sparse_bitset:foldr_2)/3, (T_1 = int), (sparse_bitset:'TypeSpecOf__pred_or_func__foldr_2__[T = int]')). :- func sparse_bitset:fold_bits((sparse_bitset:fold_direction), (func(T_1, U_2) = U_2), int, int, U_2) = U_2 <= (enum:enum(T_1)). :- mode sparse_bitset:fold_bits((builtin:in), (builtin:in), (builtin:in), (builtin:in), (builtin:in)) = (builtin:out) is det. :- pragma type_spec((sparse_bitset:fold_bits)/5, (T_1 = (term:var(V_3))), (sparse_bitset:'TypeSpecOf__pred_or_func__fold_bits__[T = var(V_2)]')). :- pragma type_spec((sparse_bitset:fold_bits)/5, (T_1 = int), (sparse_bitset:'TypeSpecOf__pred_or_func__fold_bits__[T = int]')). :- func sparse_bitset:fold_bits_2((sparse_bitset:fold_direction), (func(T_1, U_2) = U_2), int, int, int, U_2) = U_2 <= (enum:enum(T_1)). :- mode sparse_bitset:fold_bits_2((builtin:in), (builtin:in), (builtin:in), (builtin:in), (builtin:in), (builtin:in)) = (builtin:out) is det. :- pragma type_spec((sparse_bitset:fold_bits_2)/6, (T_1 = (term:var(V_3))), (sparse_bitset:'TypeSpecOf__pred_or_func__fold_bits_2__[T = var(V_2)]')). :- pragma type_spec((sparse_bitset:fold_bits_2)/6, (T_1 = int), (sparse_bitset:'TypeSpecOf__pred_or_func__fold_bits_2__[T = int]')). :- func sparse_bitset:insert_2((list:list((sparse_bitset:bitset_elem))), int) = (list:list((sparse_bitset:bitset_elem))). :- mode sparse_bitset:insert_2((builtin:in), (builtin:in)) = (builtin:out) is det. :- func sparse_bitset:list_to_set_2((list:list(T_1)), (list:list((sparse_bitset:bitset_elem)))) = (list:list((sparse_bitset:bitset_elem))) <= (enum:enum(T_1)). :- mode sparse_bitset:list_to_set_2((builtin:in), (builtin:in)) = (builtin:out) is det. :- pragma type_spec((sparse_bitset:list_to_set_2)/2, (T_1 = int), (sparse_bitset:'TypeSpecOf__pred_or_func__list_to_set_2__[T = int]')). :- pragma type_spec((sparse_bitset:list_to_set_2)/2, (T_1 = (term:var(V_2))), (sparse_bitset:'TypeSpecOf__pred_or_func__list_to_set_2__[T = var(V_2)]')). :- func sparse_bitset:sorted_list_to_set_2((list:list(T_1))) = (list:list((sparse_bitset:bitset_elem))) <= (enum:enum(T_1)). :- mode sparse_bitset:sorted_list_to_set_2((builtin:in)) = (builtin:out) is det. :- pragma type_spec((sparse_bitset:sorted_list_to_set_2)/1, (T_1 = int), (sparse_bitset:'TypeSpecOf__pred_or_func__sorted_list_to_set_2__[T = int]')). :- pragma type_spec((sparse_bitset:sorted_list_to_set_2)/1, (T_1 = (term:var(V_2))), (sparse_bitset:'TypeSpecOf__pred_or_func__sorted_list_to_set_2__[T = var(V_2)]')). :- pred sparse_bitset:contains_2((list:list((sparse_bitset:bitset_elem))), int). :- mode sparse_bitset:contains_2((builtin:in), (builtin:in)) is semidet. :- func sparse_bitset:union_2((list:list((sparse_bitset:bitset_elem))), (list:list((sparse_bitset:bitset_elem)))) = (list:list((sparse_bitset:bitset_elem))). :- mode sparse_bitset:union_2((builtin:in), (builtin:in)) = (builtin:out) is det. :- func sparse_bitset:intersect_2((list:list((sparse_bitset:bitset_elem))), (list:list((sparse_bitset:bitset_elem)))) = (list:list((sparse_bitset:bitset_elem))). :- mode sparse_bitset:intersect_2((builtin:in), (builtin:in)) = (builtin:out) is det. :- func sparse_bitset:difference_2((list:list((sparse_bitset:bitset_elem))), (list:list((sparse_bitset:bitset_elem)))) = (list:list((sparse_bitset:bitset_elem))). :- mode sparse_bitset:difference_2((builtin:in), (builtin:in)) = (builtin:out) is det. :- func sparse_bitset:mask(int) = int. :- mode sparse_bitset:mask((builtin:in)) = (builtin:out) is det. :- pragma inline((sparse_bitset:mask)/1). sparse_bitset:init = (sparse_bitset:sparse_bitset(V_2)) :- V_2 = list:[]. sparse_bitset:init(HeadVar__1_1) :- HeadVar__1_1 = sparse_bitset:init. sparse_bitset:empty(HeadVar__1_1) :- HeadVar__1_1 = sparse_bitset:init. sparse_bitset:equal(X_3, X_3). sparse_bitset:list_to_set(List_3) = (sparse_bitset:sparse_bitset(V_4)) :- V_4 = sparse_bitset:list_to_set_2(List_3, V_5), V_5 = list:[]. sparse_bitset:list_to_set(A_3, HeadVar__2_2) :- HeadVar__2_2 = sparse_bitset:list_to_set(A_3). sparse_bitset:sorted_list_to_set(L_3) = (sparse_bitset:sparse_bitset(V_4)) :- V_4 = sparse_bitset:sorted_list_to_set_2(L_3). sparse_bitset:sorted_list_to_set(A_3, HeadVar__2_2) :- HeadVar__2_2 = sparse_bitset:sorted_list_to_set(A_3). sparse_bitset:to_sorted_list(Set_3) = HeadVar__2_2 :- HeadVar__2_2 = sparse_bitset:foldr(V_6, Set_3, V_7), V_6 = (func(V_10::(builtin:in), V_9::(builtin:in)) = (V_8::(builtin:out)) is det :- some [] ( V_10 = Elem_11, V_9 = Acc0_12, V_8 = list:[Elem_11 | Acc0_12] ) ), V_7 = list:[]. sparse_bitset:to_sorted_list(A_3, HeadVar__2_2) :- HeadVar__2_2 = sparse_bitset:to_sorted_list(A_3). sparse_bitset:make_singleton_set(A_3) = HeadVar__2_2 :- HeadVar__2_2 = sparse_bitset:insert(V_4, A_3), V_4 = sparse_bitset:init. sparse_bitset:singleton_set(HeadVar__1_1, A_3) :- HeadVar__1_1 = sparse_bitset:make_singleton_set(A_3). sparse_bitset:subset(Subset_3, Set_4) :- V_5 = Subset_3, sparse_bitset:intersect(Set_4, Subset_3, V_5). sparse_bitset:superset(Superset_3, Set_4) :- sparse_bitset:subset(Set_4, Superset_3). sparse_bitset:contains((sparse_bitset:sparse_bitset(Set_3)), Elem_4) :- V_5 = enum:to_int(Elem_4), sparse_bitset:contains_2(Set_3, V_5). sparse_bitset:insert((sparse_bitset:sparse_bitset(Set_4)), Elem_5) = (sparse_bitset:sparse_bitset(V_6)) :- V_6 = sparse_bitset:insert_2(Set_4, V_7), V_7 = enum:to_int(Elem_5). sparse_bitset:insert(A_4, B_5, HeadVar__3_3) :- HeadVar__3_3 = sparse_bitset:insert(A_4, B_5). sparse_bitset:insert_list(Set_4, List_5) = HeadVar__3_3 :- HeadVar__3_3 = sparse_bitset:union(V_6, Set_4), V_6 = sparse_bitset:list_to_set(List_5). sparse_bitset:insert_list(A_4, B_5, HeadVar__3_3) :- HeadVar__3_3 = sparse_bitset:insert_list(A_4, B_5). sparse_bitset:delete(Set_4, Elem_5) = HeadVar__3_3 :- HeadVar__3_3 = sparse_bitset:difference(Set_4, V_6), V_6 = sparse_bitset:insert(V_7, Elem_5), V_7 = sparse_bitset:init. sparse_bitset:delete(A_4, B_5, HeadVar__3_3) :- HeadVar__3_3 = sparse_bitset:delete(A_4, B_5). sparse_bitset:delete_list(Set_4, List_5) = HeadVar__3_3 :- HeadVar__3_3 = sparse_bitset:difference(Set_4, V_6), V_6 = sparse_bitset:list_to_set(List_5). sparse_bitset:delete_list(A_4, B_5, HeadVar__3_3) :- HeadVar__3_3 = sparse_bitset:delete_list(A_4, B_5). sparse_bitset:remove(Set0_4, Elem_5) = Set_6 :- sparse_bitset:contains(Set0_4, Elem_5), Set_6 = sparse_bitset:delete(Set0_4, Elem_5). sparse_bitset:remove(A_4, B_5, HeadVar__3_3) :- HeadVar__3_3 = sparse_bitset:remove(A_4, B_5). sparse_bitset:remove_list(Set0_4, Elems_5) = Set_6 :- sparse_bitset:list_to_set(Elems_5, ElemsSet_7), sparse_bitset:subset(ElemsSet_7, Set0_4), Set_6 = sparse_bitset:difference(Set0_4, ElemsSet_7). sparse_bitset:remove_list(A_4, B_5, HeadVar__3_3) :- HeadVar__3_3 = sparse_bitset:remove_list(A_4, B_5). sparse_bitset:union((sparse_bitset:sparse_bitset(Set1_4)), (sparse_bitset:sparse_bitset(Set2_5))) = (sparse_bitset:sparse_bitset(V_6)) :- V_6 = sparse_bitset:union_2(Set1_4, Set2_5). sparse_bitset:union(A_4, B_5, HeadVar__3_3) :- HeadVar__3_3 = sparse_bitset:union(A_4, B_5). sparse_bitset:intersect((sparse_bitset:sparse_bitset(Set1_4)), (sparse_bitset:sparse_bitset(Set2_5))) = (sparse_bitset:sparse_bitset(V_6)) :- V_6 = sparse_bitset:intersect_2(Set1_4, Set2_5). sparse_bitset:intersect(A_4, B_5, HeadVar__3_3) :- HeadVar__3_3 = sparse_bitset:intersect(A_4, B_5). sparse_bitset:difference((sparse_bitset:sparse_bitset(Set1_4)), (sparse_bitset:sparse_bitset(Set2_5))) = (sparse_bitset:sparse_bitset(V_6)) :- V_6 = sparse_bitset:difference_2(Set1_4, Set2_5). sparse_bitset:difference(A_4, B_5, HeadVar__3_3) :- HeadVar__3_3 = sparse_bitset:difference(A_4, B_5). sparse_bitset:count(Set_3) = HeadVar__2_2 :- HeadVar__2_2 = sparse_bitset:foldl(V_6, Set_3, V_7), V_6 = (func(V_10::(builtin:in), V_9::(builtin:in)) = (V_8::(builtin:out)) is det :- some [] ( V_10 = V_12, V_9 = Acc_14, V_8 = int:(Acc_14 + V_11), V_11 = 1 ) ), V_7 = 0. sparse_bitset:foldl(F_5, (sparse_bitset:sparse_bitset(Set_6)), Acc0_7) = HeadVar__4_4 :- HeadVar__4_4 = sparse_bitset:foldl_2(F_5, Set_6, Acc0_7). sparse_bitset:foldr(F_5, (sparse_bitset:sparse_bitset(Set_6)), Acc0_7) = HeadVar__4_4 :- HeadVar__4_4 = sparse_bitset:foldr_2(F_5, Set_6, Acc0_7). sparse_bitset:foldl_2(V_5, (list:[]), Acc_6) = Acc_6. sparse_bitset:foldl_2(F_7, (list:[H_8 | T_9]), Acc0_10) = Acc_11 :- Acc1_12 = sparse_bitset:fold_bits(V_13, F_7, V_14, V_15, Acc0_10), V_13 = sparse_bitset:low_to_high, H_8 = sparse_bitset:bitset_elem(V_14, V_16), H_8 = sparse_bitset:bitset_elem(V_17, V_15), Acc_11 = sparse_bitset:foldl_2(F_7, T_9, Acc1_12). sparse_bitset:foldr_2(V_5, (list:[]), Acc_6) = Acc_6. sparse_bitset:foldr_2(F_7, (list:[H_8 | T_9]), Acc0_10) = Acc_11 :- Acc1_12 = sparse_bitset:foldr_2(F_7, T_9, Acc0_10), Acc_11 = sparse_bitset:fold_bits(V_13, F_7, V_14, V_15, Acc1_12), V_13 = sparse_bitset:high_to_low, H_8 = sparse_bitset:bitset_elem(V_14, V_16), H_8 = sparse_bitset:bitset_elem(V_17, V_15). sparse_bitset:fold_bits(Dir_7, F_8, Offset_9, Bits_10, Acc0_11) = Acc_12 :- Size_13 = int:bits_per_int, Acc_12 = sparse_bitset:fold_bits_2(Dir_7, F_8, Offset_9, Bits_10, Size_13, Acc0_11). sparse_bitset:fold_bits_2(Dir_8, F_9, Offset_10, Bits_11, Size_12, Acc0_13) = Acc_14 :- (if Bits_11 = 0 then Acc_14 = Acc0_13 else (if Size_12 = 1 then (if Elem_15 = enum:from_int(Offset_10) then Acc_14 = apply(F_9, Elem_15, Acc0_13) else V_21 = "sparse_bitset.m: `enum__from_int/1\' failed", require:error(V_21) ) else HalfSize_16 = int:unchecked_right_shift(Size_12, V_22), V_22 = 1, Mask_17 = sparse_bitset:mask(HalfSize_16), LowBits_18 = int:(Mask_17 /\ Bits_11), HighBits_19 = int:(Mask_17 /\ V_23), V_23 = int:unchecked_right_shift(Bits_11, HalfSize_16), ( % disjunction Dir_8 = sparse_bitset:low_to_high, Acc1_20 = sparse_bitset:fold_bits_2(Dir_8, F_9, Offset_10, LowBits_18, HalfSize_16, Acc0_13), Acc_14 = sparse_bitset:fold_bits_2(Dir_8, F_9, V_25, HighBits_19, HalfSize_16, Acc1_20), V_25 = int:(Offset_10 + HalfSize_16) ; Dir_8 = sparse_bitset:high_to_low, Acc1_26 = sparse_bitset:fold_bits_2(Dir_8, F_9, V_24, HighBits_19, HalfSize_16, Acc0_13), V_24 = int:(Offset_10 + HalfSize_16), Acc_14 = sparse_bitset:fold_bits_2(Dir_8, F_9, Offset_10, LowBits_18, HalfSize_16, Acc1_26) ) ) ). :- pragma inline((sparse_bitset:mask)/1). sparse_bitset:mask(N_3) = HeadVar__2_2 :- HeadVar__2_2 = int:(\ V_4), V_4 = int:unchecked_left_shift(V_5, N_3), V_5 = int:(\ V_6), V_6 = 0. :- pragma termination_info((sparse_bitset:init) = (builtin:out), finite(1, [no, no]), cannot_loop). :- pragma termination_info(sparse_bitset:init((builtin:out)), finite(1, [no, no]), cannot_loop). :- pragma termination_info(sparse_bitset:empty((builtin:in)), finite(0, [no, no]), cannot_loop). :- pragma termination_info(sparse_bitset:empty((builtin:out)), finite(1, [no, no]), cannot_loop). :- pragma termination_info(sparse_bitset:equal((builtin:in), (builtin:in)), finite(0, [no, no, no]), cannot_loop). :- pragma termination_info(sparse_bitset:list_to_set((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:list_to_set((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(sparse_bitset:sorted_list_to_set((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:sorted_list_to_set((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(sparse_bitset:to_sorted_list((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:to_sorted_list((builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(sparse_bitset:make_singleton_set((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:singleton_set((builtin:out), (builtin:in)), infinite, can_loop). :- pragma termination_info(sparse_bitset:subset((builtin:in), (builtin:in)), finite(0, [no, no, no]), cannot_loop). :- pragma termination_info(sparse_bitset:superset((builtin:in), (builtin:in)), finite(0, [no, no, no]), cannot_loop). :- pragma termination_info(sparse_bitset:contains((builtin:in), (builtin:in)), finite(0, [no, no, no]), can_loop). :- pragma termination_info(sparse_bitset:insert((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:insert((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(sparse_bitset:insert_list((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:insert_list((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(sparse_bitset:delete((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:delete((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(sparse_bitset:delete_list((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:delete_list((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(sparse_bitset:remove((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:remove((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(sparse_bitset:remove_list((builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:remove_list((builtin:in), (builtin:in), (builtin:out)), infinite, can_loop). :- pragma termination_info(sparse_bitset:remove_least((builtin:in), (builtin:out), (builtin:out)), infinite, can_loop). :- pragma termination_info(sparse_bitset:union((builtin:in), (builtin:in)) = (builtin:out), infinite, cannot_loop). :- pragma termination_info(sparse_bitset:union((builtin:in), (builtin:in), (builtin:out)), infinite, cannot_loop). :- pragma termination_info(sparse_bitset:intersect((builtin:in), (builtin:in)) = (builtin:out), infinite, cannot_loop). :- pragma termination_info(sparse_bitset:intersect((builtin:in), (builtin:in), (builtin:out)), infinite, cannot_loop). :- pragma termination_info(sparse_bitset:difference((builtin:in), (builtin:in)) = (builtin:out), infinite, cannot_loop). :- pragma termination_info(sparse_bitset:difference((builtin:in), (builtin:in), (builtin:out)), infinite, cannot_loop). :- pragma termination_info(sparse_bitset:count((builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:foldl((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop). :- pragma termination_info(sparse_bitset:foldr((builtin:in), (builtin:in), (builtin:in)) = (builtin:out), infinite, can_loop).