cleanup: Make Vec.shrink take the new length (#1029)

This is the documented behavior, and avoids doing a weird dance of
computing `size - (size - i)` rather than just using `i` everywhere.

src/lib/reasoners/satml.ml

@@ -637,14 +637,14 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
         env.lazy_cnf <- Vec.get env.lazy_cnf_queue lvl;
         env.relevants <- Vec.get env.relevants_queue lvl;
       end;
-      Vec.shrink env.trail ((Vec.size env.trail) - env.qhead);
-      Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl);
-      Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl);
+      Vec.shrink env.trail env.qhead;
+      Vec.shrink env.trail_lim lvl;
+      Vec.shrink env.tenv_queue lvl;
       if Options.get_cdcl_tableaux () then begin
         Vec.shrink
-          env.lazy_cnf_queue ((Vec.size env.lazy_cnf_queue) - lvl);
+          env.lazy_cnf_queue lvl;
         Vec.shrink env.relevants_queue
-          ((Vec.size env.relevants_queue) - lvl)
+          lvl
         [@ocaml.ppwarning "TODO: try to disable 'fill_with_dummy'"]
       end;
       (try
@@ -806,8 +806,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
           ) watched;
       with Conflict c -> assert (!res == C_none); res := C_bool c
     end;
-    let dead_part = Vec.size watched - !new_sz_w in
-    Vec.shrink watched dead_part
+    Vec.shrink watched !new_sz_w
 
 
   let do_case_split env origin =
@@ -1119,21 +1118,20 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
   else
   begin Vec.set env.learnts !j c; incr j end
   done;
-  Vec.shrink env.learnts (lim2 - !j) true
+  Vec.shrink env.learnts !j true
 *)
 
   let remove_satisfied env vec =
     let j = ref 0 in
-    let k = Vec.size vec - 1 in
-    for i = 0 to k do
+    for i = 0 to Vec.size vec - 1 do
       let c = Vec.get vec i in
       if satisfied c then remove_clause env c
       else begin
         Vec.set vec !j (Vec.get vec i);
         incr j
       end
     done;
-    Vec.shrink vec (k + 1 - !j)
+    Vec.shrink vec !j
 
 
   module HUC = Hashtbl.Make

src/lib/util/heap.ml

@@ -131,7 +131,7 @@ module Make(Rank : RankedType) = struct
       end
       else Rank.set_index elt absent;
     done;
-    Vec.shrink heap (lim - !j);
+    Vec.shrink heap !j;
     for i = (lim / 2) - 1 downto 0 do
       percolate_down s (Vec.get heap i)
     done

src/lib/util/vec.ml

@@ -49,10 +49,10 @@ let[@inline] clear vec =
 let[@inline] shrink vec i =
   assert (i >= 0);
   assert (i <= vec.sz);
-  for j = vec.sz - i to vec.sz - 1 do
+  for j = i to vec.sz - 1 do
     Array.unsafe_set vec.data j vec.dummy
   done;
-  vec.sz <- vec.sz - i
+  vec.sz <- i
 
 let[@inline] pop vec =
   assert (vec.sz > 0);