refactor: Rrplace Veci and Vec_float with polymorphic Vec

Author: c-cube

src/checker/drup_check.ml

@@ -53,7 +53,7 @@ end
 
     Each event is checked by reverse-unit propagation on previous events. *)
 module Fwd_check : sig
-  type error = [ `Bad_steps of Veci.t | `No_empty_clause ]
+  type error = [ `Bad_steps of int Vec.t | `No_empty_clause ]
 
   val pp_error : Trace.t -> error Fmt.printer
 
@@ -62,10 +62,10 @@ module Fwd_check : sig
       success. In case of error it returns [Error idxs] where [idxs] are the
       indexes in the trace of the steps that failed. *)
 end = struct
-  type t = { checker: Checker.t; errors: Veci.t }
+  type t = { checker: Checker.t; errors: int Vec.t }
 
   let create cstore : t =
-    { checker = Checker.create cstore; errors = Veci.create () }
+    { checker = Checker.create cstore; errors = Vec.create () }
 
   (* check event, return [true] if it's valid *)
   let check_op (self : t) i (op : Trace.op) : bool =
@@ -85,15 +85,15 @@ end = struct
       Checker.del_clause self.checker c;
       true
 
-  type error = [ `Bad_steps of Veci.t | `No_empty_clause ]
+  type error = [ `Bad_steps of int Vec.t | `No_empty_clause ]
 
   let pp_error trace out = function
     | `No_empty_clause -> Fmt.string out "no empty clause found"
     | `Bad_steps bad ->
-      let n0 = Veci.get bad 0 in
+      let n0 = Vec.get bad 0 in
       Fmt.fprintf out
         "@[<v>checking failed on %d ops.@ @[<2>First failure is op[%d]:@ %a@]@]"
-        (Veci.size bad) n0 Trace.pp_op (Trace.get trace n0)
+        (Vec.size bad) n0 Trace.pp_op (Trace.get trace n0)
 
   let check trace : _ result =
     let self = create (Trace.cstore trace) in
@@ -114,13 +114,13 @@ end = struct
         ) else (
           Log.debugf 10 (fun k ->
               k "(@[check.proof_rule.fail@ :idx %d@ :op %a@])" i Trace.pp_op op);
-          Veci.push self.errors i
+          Vec.push self.errors i
         ));
 
-    Log.debugf 10 (fun k -> k "found %d errors" (Veci.size self.errors));
+    Log.debugf 10 (fun k -> k "found %d errors" (Vec.size self.errors));
     if not !has_false then
       Error `No_empty_clause
-    else if Veci.size self.errors > 0 then
+    else if Vec.size self.errors > 0 then
       Error (`Bad_steps self.errors)
     else
       Ok ()

src/main/show_trace.ml

@@ -10,7 +10,7 @@ type state = {
   p_reader: Proof.Trace_reader.t;
 }
 
-let show_sat (self : state) ~tag v : unit =
+let show_sat (_self : state) ~tag v : unit =
   match tag with
   | "AssCSat" ->
     (match

src/sat/heap.ml

@@ -4,10 +4,10 @@ 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: Veci.t (* vec of elements *) }
+  type t = { store: elt_store; heap: int Vec.t (* vec of elements *) }
 
   let _absent_index = -1
-  let create store : t = { store; heap = Veci.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 *)
@@ -16,17 +16,17 @@ module Make (Elt : RANKED) = struct
 
   (*
   let rec heap_property cmp ({heap=heap} as s) i =
-    i >= (Veci.size heap)  ||
+    i >= (Vec.size heap)  ||
       ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i))))
        && heap_property cmp s (left i) && heap_property cmp s (right i))
 
   let heap_property cmp s = heap_property cmp s 1
   *)
 
-  let[@inline] get_elt_ self i = Elt.of_int_unsafe (Veci.get self.heap i)
+  let[@inline] get_elt_ self i = Elt.of_int_unsafe (Vec.get self.heap i)
 
   let[@inline] set_elt_ self i elt =
-    Veci.set self.heap i (elt : Elt.t :> int)
+    Vec.set self.heap i (elt : Elt.t :> int)
 
   (* [elt] is above or at its expected position. Move it up the heap
      (towards high indices) to restore the heap property *)
@@ -43,7 +43,7 @@ module Make (Elt : RANKED) = struct
     Elt.set_heap_idx self.store elt !i
 
   let percolate_down (self : t) (elt : Elt.t) : unit =
-    let sz = Veci.size self.heap in
+    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
@@ -83,7 +83,7 @@ module Make (Elt : RANKED) = struct
 
   let filter (self : t) filt : unit =
     let j = ref 0 in
-    let lim = Veci.size self.heap in
+    let lim = Vec.size self.heap in
     for i = 0 to lim - 1 do
       if filt (get_elt_ self i) then (
         set_elt_ self !j (get_elt_ self i);
@@ -92,24 +92,24 @@ module Make (Elt : RANKED) = struct
       ) else
         Elt.set_heap_idx self.store (get_elt_ self i) _absent_index
     done;
-    Veci.shrink self.heap (lim - !j);
+    Vec.shrink self.heap (lim - !j);
     for i = (lim / 2) - 1 downto 0 do
       percolate_down self (get_elt_ self i)
     done
 
-  let[@inline] size s = Veci.size s.heap
-  let[@inline] is_empty s = Veci.is_empty s.heap
+  let[@inline] size s = Vec.size s.heap
+  let[@inline] is_empty s = Vec.is_empty s.heap
 
   let clear self : unit =
-    Veci.iter self.heap ~f:(fun e ->
+    Vec.iter self.heap ~f:(fun e ->
         Elt.set_heap_idx self.store (Elt.of_int_unsafe e) _absent_index);
-    Veci.clear self.heap;
+    Vec.clear self.heap;
     ()
 
   let insert self elt =
     if not (in_heap self elt) then (
-      Elt.set_heap_idx self.store elt (Veci.size self.heap);
-      Veci.push self.heap (elt : Elt.t :> int);
+      Elt.set_heap_idx self.store elt (Vec.size self.heap);
+      Vec.push self.heap (elt : Elt.t :> int);
       percolate_up self elt
     )
 
@@ -128,21 +128,21 @@ module Make (Elt : RANKED) = struct
   *)
 
   let remove_min self =
-    match Veci.size self.heap with
+    match Vec.size self.heap with
     | 0 -> raise Not_found
     | 1 ->
-      let x = Elt.of_int_unsafe (Veci.pop self.heap) in
+      let x = Elt.of_int_unsafe (Vec.pop_exn self.heap) in
       Elt.set_heap_idx self.store x _absent_index;
       x
     | _ ->
       let x = get_elt_ self 0 in
-      let new_hd = Elt.of_int_unsafe (Veci.pop self.heap) in
+      let new_hd = Elt.of_int_unsafe (Vec.pop_exn self.heap) in
       (* heap.last() *)
       set_elt_ self 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 Veci.size self.heap > 1 then percolate_down self new_hd;
+      if Vec.size self.heap > 1 then percolate_down self new_hd;
       x
 end
 [@@inline]

src/sat/solver.ml

@@ -13,7 +13,7 @@ module Atom = Store.Atom
 module Var = Store.Var
 module Clause = Store.Clause
 
-module H = Heap.Make [@specialise] (struct
+module H = Heap.Make (struct
   type store = Store.t
   type t = var
 
@@ -262,7 +262,7 @@ type t = {
      store them here. *)
   trail: AVec.t;
   (* decision stack + propagated elements (atoms or assignments). *)
-  var_levels: Veci.t; (* decision levels in [trail]  *)
+  var_levels: int Vec.t; (* decision levels in [trail]  *)
   assumptions: AVec.t; (* current assumptions *)
   mutable th_head: int;
   (* Start offset in the queue {!trail} of
@@ -328,7 +328,7 @@ let create_ ~store ~tracer ~stat ~max_clauses_learnt (plugin : plugin) : t =
     th_head = 0;
     elt_head = 0;
     trail = AVec.create ();
-    var_levels = Veci.create ();
+    var_levels = Vec.create ();
     assumptions = AVec.create ();
     order = H.create store;
     var_incr = 1.;
@@ -357,7 +357,7 @@ let iter_clauses_learnt_ (self : t) ~f : unit =
   Vec.iter ~f:iter_pool self.clause_pools;
   ()
 
-let[@inline] decision_level st = Veci.size st.var_levels
+let[@inline] decision_level st = Vec.size st.var_levels
 let[@inline] nb_clauses st = CVec.size st.clauses_hyps
 let stat self = self.stat
 
@@ -578,7 +578,7 @@ let preprocess_clause_ (self : t) (c : Clause.t) : Clause.t =
 let new_decision_level (self : t) =
   assert (self.th_head = AVec.size self.trail);
   assert (self.elt_head = AVec.size self.trail);
-  Veci.push self.var_levels (AVec.size self.trail);
+  Vec.push self.var_levels (AVec.size self.trail);
   let (module P) = self.plugin in
   P.push_level ();
   ()
@@ -613,7 +613,7 @@ let cancel_until (self : t) lvl =
   else (
     Log.debugf 5 (fun k -> k "(@[sat.cancel-until %d@])" lvl);
     (* We set the head of the solver and theory queue to what it was. *)
-    let head = ref (Veci.get self.var_levels lvl) in
+    let head = ref (Vec.get self.var_levels lvl) in
     self.elt_head <- !head;
     self.th_head <- !head;
     (* Now we need to cleanup the vars that are not valid anymore
@@ -646,7 +646,7 @@ let cancel_until (self : t) lvl =
     assert (n > 0);
     (* Resize the vectors according to their new size. *)
     AVec.shrink self.trail !head;
-    Veci.shrink self.var_levels lvl;
+    Vec.shrink self.var_levels lvl;
     let (module P) = self.plugin in
     P.pop_levels n;
     Delayed_actions.clear_on_backtrack self.delayed_actions;

src/sat/store.ml

@@ -5,8 +5,8 @@ module Lit_tbl = Hashtbl.Make (Lit)
 
 type cstore = {
   c_lits: atom array Vec.t; (* storage for clause content *)
-  c_activity: Vec_float.t;
-  c_recycle_idx: Veci.t; (* recycle clause numbers that were GC'd *)
+  c_activity: float Vec.t;
+  c_recycle_idx: int Vec.t; (* recycle clause numbers that were GC'd *)
   c_proof: Step_vec.t; (* clause -> proof_rule for its proof *)
   c_attached: Bitvec.t;
   c_marked: Bitvec.t;
@@ -19,7 +19,7 @@ type t = {
   v_of_lit: var Lit_tbl.t; (* lit -> var *)
   v_level: int Vec.t; (* decision/assignment level, or -1 *)
   v_heap_idx: int Vec.t; (* index in priority heap *)
-  v_weight: Vec_float.t; (* heuristic activity *)
+  v_weight: float Vec.t; (* heuristic activity *)
   v_reason: var_reason option Vec.t; (* reason for assignment *)
   v_seen: Bitvec.t; (* generic temporary marker *)
   v_default_polarity: Bitvec.t; (* default polarity in decisions *)
@@ -52,7 +52,7 @@ let create ?(size = `Big) ~stat () : t =
     v_of_lit = Lit_tbl.create size_map;
     v_level = Vec.create ();
     v_heap_idx = Vec.create ();
-    v_weight = Vec_float.create ();
+    v_weight = Vec.create ();
     v_reason = Vec.create ();
     v_seen = Bitvec.create ();
     v_default_polarity = Bitvec.create ();
@@ -67,8 +67,8 @@ let create ?(size = `Big) ~stat () : t =
     c_store =
       {
         c_lits = Vec.create ();
-        c_activity = Vec_float.create ();
-        c_recycle_idx = Veci.create ~cap:0 ();
+        c_activity = Vec.create ();
+        c_recycle_idx = Vec.create ();
         c_proof = Step_vec.create ~cap:0 ();
         c_dead = Bitvec.create ();
         c_attached = Bitvec.create ();
@@ -88,10 +88,10 @@ module Var = struct
   let[@inline] set_level self v l = Vec.set self.v_level (v : var :> int) l
   let[@inline] reason self v = Vec.get self.v_reason (v : var :> int)
   let[@inline] set_reason self v r = Vec.set self.v_reason (v : var :> int) r
-  let[@inline] weight self v = Vec_float.get self.v_weight (v : var :> int)
+  let[@inline] weight self v = Vec.get self.v_weight (v : var :> int)
 
   let[@inline] set_weight self v w =
-    Vec_float.set self.v_weight (v : var :> int) w
+    Vec.set self.v_weight (v : var :> int) w
 
   let[@inline] mark self v = Bitvec.set self.v_seen (v : var :> int) true
   let[@inline] unmark self v = Bitvec.set self.v_seen (v : var :> int) false
@@ -208,16 +208,16 @@ module Clause = struct
     in
     (* allocate new ID *)
     let cid =
-      if Veci.is_empty c_recycle_idx then
+      if Vec.is_empty c_recycle_idx then
         Vec.size c_lits
       else
-        Veci.pop c_recycle_idx
+        Vec.pop_exn c_recycle_idx
     in
 
     (* allocate space *)
     (let new_len = cid + 1 in
      Vec.ensure_size c_lits ~elt:[||] new_len;
-     Vec_float.ensure_size c_activity new_len;
+     Vec.ensure_size c_activity ~elt:0. new_len;
      Step_vec.ensure_size c_proof new_len;
      Bitvec.ensure_size c_attached new_len;
      Bitvec.ensure_size c_dead new_len;
@@ -298,17 +298,17 @@ module Clause = struct
     Bitvec.set c_removable cid false;
     Bitvec.set c_marked cid false;
     Vec.set c_lits cid [||];
-    Vec_float.set c_activity cid 0.;
+    Vec.set c_activity cid 0.;
 
-    Veci.push c_recycle_idx cid;
+    Vec.push c_recycle_idx cid;
     (* recycle idx *)
     ()
 
   let[@inline] activity store c =
-    Vec_float.get store.c_store.c_activity (c : t :> int)
+    Vec.get store.c_store.c_activity (c : t :> int)
 
   let[@inline] set_activity store c f =
-    Vec_float.set store.c_store.c_activity (c : t :> int) f
+    Vec.set store.c_store.c_activity (c : t :> int) f
 
   let[@inline] atoms_a store c : atom array =
     Vec.get store.c_store.c_lits (c : t :> int)
@@ -372,7 +372,7 @@ let alloc_var_uncached_ ?default_pol:(pol = true) self (form : Lit.t) : var =
   Vec.push v_level (-1);
   Vec.push v_heap_idx (-1);
   Vec.push v_reason None;
-  Vec_float.push v_weight 0.;
+  Vec.push v_weight 0.;
   Bitvec.ensure_size v_seen v_idx;
   Bitvec.ensure_size v_default_polarity v_idx;
   Bitvec.set v_default_polarity v_idx pol;

src/util/Vec.ml

@@ -1,7 +1,9 @@
 type 'a t = { mutable data: 'a array; mutable sz: int }
 
 let make n x = { data = Array.make n x; sz = 0 }
+
 let[@inline] create () = { data = [||]; sz = 0 }
+
 let[@inline] clear s = s.sz <- 0
 
 let[@inline] shrink t i =