wip: refactor(sat): use struct-of-array for atom/var

src/sat/Heap.ml

@@ -4,16 +4,19 @@ module type RANKED = Heap_intf.RANKED
 module type S = Heap_intf.S
 
 module Make(Elt : RANKED) = struct
+  type elt_store = Elt.store
   type elt = Elt.t
 
   type t = {
+    store : elt_store;
     heap : elt Vec.t;
-  } [@@unboxed]
+  }
 
   let _absent_index = -1
 
-  let create () =
-    { heap = Vec.create(); }
+  let create store : t =
+    { store;
+      heap = Vec.create(); }
 
   let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
   let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *)
@@ -30,83 +33,83 @@ module Make(Elt : RANKED) = struct
 
   (* [elt] is above or at its expected position. Move it up the heap
      (towards high indices) to restore the heap property *)
-  let percolate_up {heap} (elt:Elt.t) : unit =
-    let pi = ref (parent (Elt.idx elt)) in
-    let i = ref (Elt.idx elt) in
-    while !i <> 0 && Elt.cmp elt (Vec.get heap !pi) do
-      Vec.set heap !i (Vec.get heap !pi);
-      Elt.set_idx (Vec.get heap !i) !i;
+  let percolate_up (self:t) (elt:Elt.t) : unit =
+    let pi = ref (parent (Elt.heap_idx self.store elt)) in
+    let i = ref (Elt.heap_idx self.store elt) in
+    while !i <> 0 && Elt.cmp self.store elt (Vec.get self.heap !pi) do
+      Vec.set self.heap !i (Vec.get self.heap !pi);
+      Elt.set_heap_idx self.store (Vec.get self.heap !i) !i;
       i  := !pi;
       pi := parent !i
     done;
-    Vec.set heap !i elt;
-    Elt.set_idx elt !i
+    Vec.set self.heap !i elt;
+    Elt.set_heap_idx self.store elt !i
 
-  let percolate_down {heap} (elt:Elt.t): unit =
-    let sz = Vec.size heap in
-    let li = ref (left (Elt.idx elt)) in
-    let ri = ref (right (Elt.idx elt)) in
-    let i = ref (Elt.idx elt) in
+  let percolate_down (self:t) (elt:Elt.t): unit =
+    let sz = Vec.size self.heap in
+    let li = ref (left (Elt.heap_idx self.store elt)) in
+    let ri = ref (right (Elt.heap_idx self.store elt)) in
+    let i = ref (Elt.heap_idx self.store elt) in
     begin
       try
         while !li < sz do
           let child =
-            if !ri < sz && Elt.cmp (Vec.get heap !ri) (Vec.get heap !li)
+            if !ri < sz && Elt.cmp self.store (Vec.get self.heap !ri) (Vec.get self.heap !li)
             then !ri
             else !li
           in
-          if not (Elt.cmp (Vec.get heap child) elt) then raise Exit;
-          Vec.set heap !i (Vec.get heap child);
-          Elt.set_idx (Vec.get heap !i) !i;
+          if not (Elt.cmp self.store (Vec.get self.heap child) elt) then raise_notrace Exit;
+          Vec.set self.heap !i (Vec.get self.heap child);
+          Elt.set_heap_idx self.store (Vec.get self.heap !i) !i;
           i  := child;
           li := left !i;
           ri := right !i
         done;
       with Exit -> ()
     end;
-    Vec.set heap !i elt;
-    Elt.set_idx elt !i
+    Vec.set self.heap !i elt;
+    Elt.set_heap_idx self.store elt !i
 
-  let[@inline] in_heap x = Elt.idx x >= 0
+  let[@inline] in_heap self x = Elt.heap_idx self.store x >= 0
 
-  let[@inline] decrease s x = assert (in_heap x); percolate_up s x
+  let[@inline] decrease self x = assert (in_heap self x); percolate_up self x
 
   (*
   let increase cmp s n =
     assert (in_heap s n); percolate_down cmp s (V.get s.indices n)
   *)
 
-  let filter s filt =
+  let filter (self:t) filt : unit =
     let j = ref 0 in
-    let lim = Vec.size s.heap in
+    let lim = Vec.size self.heap in
     for i = 0 to lim - 1 do
-      if filt (Vec.get s.heap i) then (
-        Vec.set s.heap !j (Vec.get s.heap i);
-        Elt.set_idx (Vec.get s.heap i) !j;
+      if filt (Vec.get self.heap i) then (
+        Vec.set self.heap !j (Vec.get self.heap i);
+        Elt.set_heap_idx self.store (Vec.get self.heap i) !j;
         incr j;
       ) else (
-        Elt.set_idx (Vec.get s.heap i) _absent_index;
+        Elt.set_heap_idx self.store (Vec.get self.heap i) _absent_index;
       );
     done;
-    Vec.shrink s.heap (lim - !j);
+    Vec.shrink self.heap (lim - !j);
     for i = (lim / 2) - 1 downto 0 do
-      percolate_down s (Vec.get s.heap i)
+      percolate_down self (Vec.get self.heap i)
     done
 
   let size s = Vec.size s.heap
 
   let is_empty s = Vec.is_empty s.heap
 
-  let clear {heap} =
-    Vec.iter (fun e -> Elt.set_idx e _absent_index) heap;
-    Vec.clear heap;
+  let clear self : unit =
+    Vec.iter (fun e -> Elt.set_heap_idx self.store e _absent_index) self.heap;
+    Vec.clear self.heap;
     ()
 
-  let insert s elt =
-    if not (in_heap elt) then (
-      Elt.set_idx elt (Vec.size s.heap);
-      Vec.push s.heap elt;
-      percolate_up s elt;
+  let insert self elt =
+    if not (in_heap self elt) then (
+      Elt.set_heap_idx self.store elt (Vec.size self.heap);
+      Vec.push self.heap elt;
+      percolate_up self elt;
     )
 
   (*
@@ -123,22 +126,22 @@ module Make(Elt : RANKED) = struct
     assert (heap_property cmp s)
   *)
 
-  let remove_min ({heap} as s) =
-    match Vec.size heap with
+  let remove_min self =
+    match Vec.size self.heap with
     | 0 -> raise Not_found
     | 1 ->
-      let x = Vec.pop heap in
-      Elt.set_idx x _absent_index;
+      let x = Vec.pop self.heap in
+      Elt.set_heap_idx self.store 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;
+      let x = Vec.get self.heap 0 in
+      let new_hd = Vec.pop self.heap in (* heap.last() *)
+      Vec.set self.heap 0 new_hd;
+      Elt.set_heap_idx self.store x _absent_index;
+      Elt.set_heap_idx self.store new_hd 0;
       (* enforce heap property again *)
-      if Vec.size heap > 1 then (
-        percolate_down s new_hd;
+      if Vec.size self.heap > 1 then (
+        percolate_down self new_hd;
       );
       x
 

src/sat/Heap.mli

@@ -2,4 +2,5 @@ module type RANKED = Heap_intf.RANKED
 
 module type S = Heap_intf.S
 
-module Make(X : RANKED) : S with type elt = X.t
+module Make(X : RANKED) :
+  S with type elt = X.t and type elt_store = X.store

src/sat/Heap_intf.ml

@@ -1,17 +1,20 @@
 
 module type RANKED = sig
+  type store
   type t
 
-  val idx: t -> int
+  val heap_idx : store -> t -> int
   (** Index in heap. return -1 if never set *)
 
-  val set_idx : t -> int -> unit
+  val set_heap_idx : store -> t -> int -> unit
   (** Update index in heap *)
 
-  val cmp : t -> t -> bool
+  val cmp : store -> t -> t -> bool
 end
 
 module type S = sig
+  type elt_store
+
   type elt
   (** Type of elements *)
 
@@ -19,13 +22,13 @@ module type S = sig
   (** Heap of {!elt}, whose priority is increased or decreased
       incrementally (see {!decrease} for instance) *)
 
-  val create : unit -> t
+  val create : elt_store -> t
   (** Create a heap *)
 
   val decrease : t -> elt -> unit
   (** [decrease h x] decreases the value associated to [x] within [h] *)
 
-  val in_heap : elt -> bool
+  val in_heap : t -> elt -> bool
 
   (*val increase : (int -> int -> bool) -> t -> int -> unit*)
 

src/sat/Solver_intf.ml

@@ -342,13 +342,13 @@ module type S = sig
 
   module Clause : sig
     type t = clause
-
-    val atoms : t -> atom array
-    val atoms_l : t -> atom list
     val equal : t -> t -> bool
 
+    val atoms : solver -> t -> atom array
+    val atoms_l : solver -> t -> atom list
+
+    val pp : solver -> t printer
     val short_name : t -> string
-    val pp : t printer
 
     module Tbl : Hashtbl.S with type key = t
   end