123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140(* This code is extracted from Msat ( https://github.com/Gbury/mSAT ).
As such it is under the Apache 2 License.
*)moduletypeRANKED=CCMutHeap_intf.RANKEDmoduletypeS=CCMutHeap_intf.SmoduleMake(Elt:RANKED)=structmoduleVec=CCVectortypeelt=Elt.ttypet={heap:eltVec.vector}[@@unboxed]let_absent_index=-1letcreate()={heap=Vec.create()}let[@inline]lefti=(ilsl1)+1(* i*2 + 1 *)let[@inline]righti=(i+1)lsl1(* (i+1)*2 *)let[@inline]parenti=(i-1)asr1(* (i-1) / 2 *)(*
let rec heap_property ({heap=heap} as s) i =
i >= (Vec.size heap) ||
((i = 0 || not(cmp (Vec.get heap i) (Vec.get heap (parent i))))
&& heap_property s (left i) && heap_property s (right i))
let heap_property s = heap_property s 1
*)(* [elt] is above or at its expected position. Move it up the heap
(towards high indices) to restore the heap property *)letpercolate_up{heap}(elt:Elt.t):unit=letpi=ref(parent(Elt.idxelt))inleti=ref(Elt.idxelt)inwhile!i<>0&&Elt.ltelt(Vec.getheap!pi)doVec.setheap!i(Vec.getheap!pi);Elt.set_idx(Vec.getheap!i)!i;i:=!pi;pi:=parent!idone;Vec.setheap!ielt;Elt.set_idxelt!iletpercolate_down{heap}(elt:Elt.t):unit=letsz=Vec.sizeheapinletli=ref(left(Elt.idxelt))inletri=ref(right(Elt.idxelt))inleti=ref(Elt.idxelt)in(trywhile!li<szdoletchild=if!ri<sz&&Elt.lt(Vec.getheap!ri)(Vec.getheap!li)then!rielse!liinifnot(Elt.lt(Vec.getheapchild)elt)thenraiseExit;Vec.setheap!i(Vec.getheapchild);Elt.set_idx(Vec.getheap!i)!i;i:=child;li:=left!i;ri:=right!idonewithExit->());Vec.setheap!ielt;Elt.set_idxelt!ilet[@inline]in_heapx=Elt.idxx>=0let[@inline]decreasesx=assert(in_heapx);percolate_upsxlet[@inline]increasesx=assert(in_heapx);percolate_downsxletfiltersfilt=letj=ref0inletlim=Vec.sizes.heapinfori=0tolim-1doiffilt(Vec.gets.heapi)then(Vec.sets.heap!j(Vec.gets.heapi);Elt.set_idx(Vec.gets.heapi)!j;incrj)elseElt.set_idx(Vec.gets.heapi)_absent_indexdone;Vec.truncates.heap(lim-!j);fori=(lim/2)-1downto0dopercolate_downs(Vec.gets.heapi)doneletsizes=Vec.sizes.heapletis_emptys=Vec.is_emptys.heapletclear{heap}=Vec.iter(fune->Elt.set_idxe_absent_index)heap;Vec.clearheap;()letinsertselt=ifnot(in_heapelt)then(Elt.set_idxelt(Vec.sizes.heap);Vec.pushs.heapelt;percolate_upselt)(*
let update cmp s n =
assert (heap_property cmp s);
begin
if in_heap s n then
begin
percolate_up cmp s (Vec.get s.indices n);
percolate_down cmp s (Vec.get s.indices n)
end
else insert cmp s n
end;
assert (heap_property cmp s)
*)letremove_min({heap}ass)=matchVec.sizeheapwith|0->raiseNot_found|1->letx=Vec.pop_exnheapinElt.set_idxx_absent_index;x|_->letx=Vec.getheap0inletnew_hd=Vec.pop_exnheapin(* heap.last() *)Vec.setheap0new_hd;Elt.set_idxx_absent_index;Elt.set_idxnew_hd0;(* enforce heap property again *)ifVec.sizeheap>1thenpercolate_downsnew_hd;xend[@@inline]