diff --git a/src/core/Heap.ml b/src/core/Heap.ml index 12fa608c..ed9884bb 100644 --- a/src/core/Heap.ml +++ b/src/core/Heap.ml @@ -124,17 +124,22 @@ module Make(Elt : RANKED) = struct *) let remove_min ({heap} as s) = - if Vec.size heap=0 then raise Not_found; - let x = Vec.get heap 0 in - let new_hd = Vec.pop heap in (* new head *) - Vec.set heap 0 new_hd; - Elt.set_idx new_hd 0; - (* remove [x]. do it after [new_hd.idx<-0] in case [x==new_hd] *) - Elt.set_idx x _absent_index; - (* enforce heap property again *) - if Vec.size heap > 1 then ( - percolate_down s new_hd; - ); - x + match Vec.size heap with + | 0 -> raise Not_found + | 1 -> + let x = Vec.pop heap in + Elt.set_idx x _absent_index; + x + | _ -> + let x = Vec.get heap 0 in + let new_hd = Vec.pop heap in (* heap.last() *) + Vec.set heap 0 new_hd; + Elt.set_idx x _absent_index; + Elt.set_idx new_hd 0; + (* enforce heap property again *) + if Vec.size heap > 1 then ( + percolate_down s new_hd; + ); + x end [@@inline]