rename a Vec function

`grow_to_by_double` becomes `grow_to_at_least` so that it doesn't
specify its own implementation's strategy

src/core/internal.ml

@@ -783,9 +783,9 @@ module Make
     if not (Stack.is_empty env.clauses_to_add) then begin
       let nbv = St.nb_elt () in
       let nbc = env.nb_init_clauses + Stack.length env.clauses_to_add in
-      Iheap.grow_to_by_double env.order nbv;
+      Iheap.grow_to_at_least env.order nbv;
-      Vec.grow_to_by_double env.clauses_hyps nbc;
+      Vec.grow_to_at_least env.clauses_hyps nbc;
-      Vec.grow_to_by_double env.clauses_learnt nbc;
+      Vec.grow_to_at_least env.clauses_learnt nbc;
       env.nb_init_clauses <- nbc;
       while not (Stack.is_empty env.clauses_to_add) do
         let c = Stack.pop env.clauses_to_add in
@@ -898,7 +898,7 @@ module Make
 
   let slice_propagate f lvl =
     let a = atom f in
-    Iheap.grow_to_by_double env.order (St.nb_elt ());
+    Iheap.grow_to_at_least env.order (St.nb_elt ());
     enqueue_bool a lvl (Semantic lvl)
 
   let current_slice (): (_,_,_) Plugin_intf.slice = {
@@ -935,7 +935,7 @@ module Make
       | Plugin_intf.Unsat (l, p) ->
         (* conflict *)
         let l = List.rev_map new_atom l in
-        Iheap.grow_to_by_double env.order (St.nb_elt ());
+        Iheap.grow_to_at_least env.order (St.nb_elt ());
         List.iter (fun a -> insert_var_order (elt_of_var a.var)) l;
         let c = St.make_clause (St.fresh_tname ()) l (Lemma p) in
         Some c
@@ -1175,7 +1175,7 @@ module Make
         end else begin
           (* Grow the heap, because when the lit is backtracked,
              it will be added to the heap. *)
-          Iheap.grow_to_by_double env.order (St.nb_elt ());
+          Iheap.grow_to_at_least env.order (St.nb_elt ());
           (* make a decision, propagate *)
           let level = decision_level() in
           enqueue_bool a ~level (Bcp c);

src/util/iheap.ml

@@ -111,9 +111,9 @@ let insert cmp s n =
       percolate_up cmp s (V.get s.indices n)
     end
 
-let grow_to_by_double s sz =
+let grow_to_at_least s sz =
   V.resize s.indices sz;
-  Vec.grow_to_by_double s.heap sz
+  Vec.grow_to_at_least s.heap sz
 
 (*
 let update cmp s n =

src/util/iheap.mli

@@ -40,7 +40,7 @@ val clear : t -> unit
 val insert : (int -> int -> bool) -> t -> int -> unit
 (** Insert a new integer into the heap, according to the given comparison *)
 
-val grow_to_by_double: t -> int -> unit
+val grow_to_at_least: t -> int -> unit
 (** Hint: augment the internal capacity of the heap until it reaches at
     least the given integer *)
 

src/util/vec.ml

@@ -57,22 +57,19 @@ let size t = t.sz
 
 let is_empty t = t.sz = 0
 
-let grow_to t new_capa =
+let grow_to_exact t new_capa =
   assert (new_capa >= Array.length t.data);
   let new_data = Array.make new_capa t.dummy in
   assert (t.sz <= new_capa);
-  let old = t.data in
+  Array.blit t.data 0 new_data 0 t.sz;
-  for i = 0 to t.sz - 1 do
-    Array.unsafe_set new_data i (Array.unsafe_get old i)
-  done;
   t.data <- new_data
 
 let grow_to_double_size t =
   if Array.length t.data = Sys.max_array_length then _size_too_big();
   let size = min Sys.max_array_length (2* Array.length t.data + 1) in
-  grow_to t size
+  grow_to_exact t size
 
-let grow_to_by_double t new_capa =
+let grow_to_at_least t new_capa =
   assert (new_capa >= 0);
   if new_capa > Sys.max_array_length then _size_too_big ();
   let data = t.data in
@@ -80,7 +77,7 @@ let grow_to_by_double t new_capa =
   while !capa < new_capa do
     capa := min (2 * !capa + 1) Sys.max_array_length;
   done;
-  grow_to t !capa
+  grow_to_exact t !capa
 
 let is_full t = Array.length t.data = t.sz
 

src/util/vec.mli

@@ -49,11 +49,13 @@ val size : 'a t -> int
 
 val is_empty : 'a t -> bool
 
-val grow_to : 'a t -> int -> unit
+val grow_to_exact : 'a t -> int -> unit
 
 val grow_to_double_size : 'a t -> unit
 
-val grow_to_by_double : 'a t -> int -> unit
+val grow_to_at_least : 'a t -> int -> unit
+(** [grow_to_at_least vec n] ensures that [capacity vec >= n] in
+    the most efficient way *)
 
 val is_full : 'a t -> bool
 (** Is the capacity of the vector equal to the number of its elements? *)