1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556(* This code is extracted from Msat ( https://github.com/Gbury/mSAT ). *)(** {1 Imperative Heaps} *)moduletypeRANKED=sigtypetvalidx:t->int(** Index in heap. return -1 if never set *)valset_idx:t->int->unit(** Update index in heap *)vallt:t->t->bool(** [cmp a b] is true iff [a < b] *)endmoduletypeS=sigtypeelt(** Type of elements *)typet(** Heap of {!elt}, whose priority is increased or decreased
incrementally (see {!decrease} for instance) *)valcreate:unit->t(** Create a heap *)valdecrease:t->elt->unit(** [decrease h x] decreases the value associated to [x] within [h] *)valincrease:t->elt->unit(** [increase h x] increases the value associated to [x] within [h] *)valin_heap:elt->boolvalsize:t->int(** Number of integers within the heap *)valis_empty:t->boolvalclear:t->unit(** Clear the content of the heap *)valinsert:t->elt->unit(** Insert a new element into the heap *)(*val update : (int -> int -> bool) -> t -> int -> unit*)valremove_min:t->elt(** Remove and return the integer that has the lowest value from the heap
@raise Not_found if the heap is empty *)valfilter:t->(elt->bool)->unit(** Filter out values that don't satisfy the predicate *)end