123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221(* 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)inbegintrywhile!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!idone;withExit->()end;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;)else(Elt.set_idx(Vec.gets.heapi)_absent_index;);done;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>1then(percolate_downsnew_hd;);xend[@@inline](*$inject
type elt = {
x: string;
mutable rank: int;
mutable idx: int;
}
module Elt = struct
type t = elt
let idx x = x.idx
let set_idx x i = x.idx <- i
let lt a b =
if a.rank = b.rank then a.x < b.x else a.rank < b.rank
end
module H = CCMutHeap.Make(Elt)
*)(*$R
let h = H.create() in
let x1 = {x="a"; rank=10; idx= -1} in
let x2 = {x="b"; rank=10; idx= -1} in
let x3 = {x="c"; rank=10; idx= -1} in
H.insert h x1;
assert (H.in_heap x1);
assert (not (H.in_heap x2));
assert (not (H.in_heap x3));
H.insert h x2;
H.insert h x3;
assert (Elt.lt x1 x2);
assert (Elt.lt x2 x3);
let x = H.remove_min h in
assert (x == x1);
let x = H.remove_min h in
assert (x == x2);
let x = H.remove_min h in
assert (x == x3);
assert (try ignore (H.remove_min h); false with Not_found -> true);
*)(*$R
let h = H.create() in
let x1 = {x="a"; rank=10; idx= -1} in
let x2 = {x="b"; rank=10; idx= -1} in
let x3 = {x="c"; rank=10; idx= -1} in
H.insert h x1;
H.insert h x2;
H.insert h x3;
x3.rank <- 2;
H.decrease h x3;
assert (Elt.lt x3 x1);
assert (Elt.lt x3 x2);
let x = H.remove_min h in
assert (x == x3);
x1.rank <- 20;
H.increase h x1;
let x = H.remove_min h in
assert (x == x2);
let x = H.remove_min h in
assert (x == x1);
assert (try ignore (H.remove_min h); false with Not_found -> true);
*)