Merge branch 'master' of https://github.com/CopperCableIsolator/goblint-sparsification

Author: CopperCableIsolator

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -29,7 +29,7 @@ struct
       m
     else (
       Array.modifyi (+) ch.dim;
-      let m' = if not del then let m = copy m in Array.fold_left (fun y x -> reduce_col_with y x; y) m ch.dim else m in
+      let m' = if not del then let m = copy m in Array.fold_left (fun y x -> reduce_col y x) m ch.dim else m in
       remove_zero_rows @@ del_cols m' ch.dim)
 
   let dim_remove ch m ~del = VectorMatrix.timing_wrap "dim remove" (fun del -> dim_remove ch m ~del:del) del
@@ -59,7 +59,7 @@ struct
     let open Apron.Texpr1 in
     let exception NotLinear in
     let zero_vec = Vector.zero_vec @@ Environment.size t.env + 1 in
-    let neg v = Vector.map_with Mpqf.neg v; v in
+    let neg v = Vector.map Mpqf.neg v in
     let is_const_vec v = Vector.compare_length_with (Vector.filteri (fun i x -> (*Inefficient*)
         Vector.compare_length_with v (i + 1) > 0 && x <>: Mpqf.zero) v) 1 = 0
     in
@@ -75,13 +75,13 @@ struct
         Vector.set_val zero_vec ((Vector.length zero_vec) - 1) (of_union x)
       | Var x ->
         let zero_vec_cp = Vector.copy zero_vec in
-        let entry_only v = Vector.set_val_with v (Environment.dim_of_var t.env x) Mpqf.one; v in
+        let entry_only v = Vector.set_val v (Environment.dim_of_var t.env x) Mpqf.one in
         begin match t.d with
           | Some m ->
             let row = Matrix.find_opt (fun r -> Vector.nth r (Environment.dim_of_var t.env x) =: Mpqf.one) m in
             begin match row with
               | Some v when is_const_vec v ->
-                Vector.set_val_with zero_vec_cp ((Vector.length zero_vec) - 1) (Vector.nth v (Vector.length v - 1)); zero_vec_cp
+                Vector.set_val zero_vec_cp ((Vector.length zero_vec) - 1) (Vector.nth v (Vector.length v - 1))
               | _ -> entry_only zero_vec_cp
             end
           | None -> entry_only zero_vec_cp end
@@ -91,17 +91,17 @@ struct
       | Binop (Add, e1, e2, _, _) ->
         let v1 = convert_texpr e1 in
         let v2 = convert_texpr e2 in
-        Vector.map2_with (+:) v1 v2; v1
+        Vector.map2 (+:) v1 v2
       | Binop (Sub, e1, e2, _, _) ->
         let v1 = convert_texpr e1 in
         let v2 = convert_texpr e2 in
-        Vector.map2_with (+:) v1 (neg @@ v2); v1
+        Vector.map2 (+:) v1 (neg @@ v2)
       | Binop (Mul, e1, e2, _, _) ->
         let v1 = convert_texpr e1 in
         let v2 = convert_texpr e2 in
         begin match to_constant_opt v1, to_constant_opt v2 with
-          | _, Some c -> Vector.apply_with_c_with ( *:) c v1; v1
-          | Some c, _ -> Vector.apply_with_c_with ( *:) c v2; v2
+          | _, Some c -> Vector.apply_with_c ( *:) c v1
+          | Some c, _ -> Vector.apply_with_c ( *:) c v2
           | _, _ -> raise NotLinear
         end
       | Binop _ -> raise NotLinear
@@ -294,18 +294,17 @@ struct
             (a, b, max)
           else
             (
-              Vector.rev_with col_a;
-              Vector.rev_with col_b;
+              let col_a = Vector.rev col_a in
+              let col_b = Vector.rev col_b in
               let i = Vector.find2i (<>:) col_a col_b in
               let (x, y) = Vector.nth col_a i, Vector.nth col_b i in
               let r, diff = Vector.length col_a - (i + 1), x -: y  in
               let a_r, b_r = Matrix.get_row a r, Matrix.get_row b r in
-              Vector.map2_with (-:) col_a col_b;
-              Vector.rev_with col_a;
+              let col_a = Vector.map2 (-:) col_a col_b in
+              let col_a = Vector.rev col_a in
               let multiply_by_t m t =
-                Matrix.map2i_with (fun i' x c -> if i' <= max then (let beta = c /: diff in
-                                                                    Vector.map2_with (fun u j -> u -: (beta *: j)) x t); x) m col_a;
-                m
+                Matrix.map2i (fun i' x c -> if i' <= max then (let beta = c /: diff in Vector.map2 (fun u j -> u -: (beta *: j)) x t) else x) m col_a;
+
               in
               Matrix.remove_row (multiply_by_t a a_r) r, Matrix.remove_row (multiply_by_t b b_r) r, (max - 1)
             )

src/cdomains/vectorMatrix.ml

@@ -83,6 +83,8 @@ sig
 
   val map_with: (num -> num) -> t -> unit
 
+  val map: (num -> num) -> t -> t
+
   val compare_length_with: t -> int -> int
 
   val of_list: num list -> t
@@ -99,6 +101,8 @@ sig
 
   val rev_with: t -> unit
 
+  val rev: t -> t
+
   val map2i: (int -> num -> num -> num) -> t -> t -> t
 
   val map2i_with: (int -> num -> num -> num) -> t -> t -> unit
@@ -107,6 +111,8 @@ sig
 
   val mapi_with: (int -> num -> num) -> t -> unit
 
+  val mapi: (int -> num -> num) -> t -> t
+
   val find2i: (num -> num -> bool) -> t -> t -> int
 
   val to_array: t -> num array
@@ -180,6 +186,8 @@ sig
 
   val map2_with: (vec -> num -> vec) -> t -> vec -> unit
 
+  val map2: (vec -> num -> vec) -> t -> vec -> t
+
   val map2i: (int -> vec-> num -> vec) -> t -> vec -> t
 
   val map2i_with: (int -> vec -> num -> vec) -> t -> vec -> unit
@@ -270,14 +278,26 @@ module ArrayVector: AbstractVector =
 
     let rev_with v = Array.rev_in_place v
 
+    let rev v = Array.rev v
+
     let map_with f v = Array.modify f v
 
+    let map f v = Array.map f v
+
     let map2_with f v1 v2 = Array.iter2i (fun i x y -> v1.(i) <- f x y) v1 v2
 
+    let map2 f v1 v2 =
+      let copy_v1 = copy v1 in
+      map2_with f copy_v1 v2; copy_v1
+
     let copy v = Array.copy v
 
     let mapi_with f v = Array.iteri (fun i x -> v.(i) <- f i x) v
 
+    let mapi f v =
+      let copy = copy v in
+      mapi_with f copy; copy
+
     let of_sparse_list ls col_count =
       let vec = Array.make col_count A.zero in
       List.iter (fun (idx, value) -> vec.(idx) <- value) ls;
@@ -788,8 +808,8 @@ module SparseMatrix: AbstractMatrix =
 
     let is_empty m =
       num_rows m = 0
-      (*This should be different if the implimentation is sound*)
-      (*m.column_count = 0*)
+    (*This should be different if the implimentation is sound*)
+    (*m.column_count = 0*)
 
     let num_cols m =
       m.column_count
@@ -807,14 +827,14 @@ module SparseMatrix: AbstractMatrix =
         match  cols with
         | x::xs -> 
           if x < idx 
-            then 
-              let (h,t) = list_of_all_before_index idx xs in
-              (x::h, t)
-            else ([],x::xs)
+          then 
+            let (h,t) = list_of_all_before_index idx xs in
+            (x::h, t)
+          else ([],x::xs)
         | [] -> ([],[])
       in
       (*This could easily be abstracted into the above functions, but its nice to have 
-      it here for readability and debugging*)
+        it here for readability and debugging*)
       let rec make_empty_entries_for_idxs idxs =
         match idxs with
         | x::xs -> (x, emptyT)::(make_empty_entries_for_idxs xs) 
@@ -872,7 +892,18 @@ module SparseMatrix: AbstractMatrix =
     let set_col_with m new_col n = timing_wrap "set_col" (set_col_with m new_col) n
 
     let set_col m new_col n = 
-      failwith "TODO"
+      let rec set_col_in_row row value =
+        match row with
+        | [] -> if value =: A.zero then [] else [(n, value)]
+        | (col_idx, v)::cs when col_idx > n -> if value =: A.zero then (col_idx, v)::cs else (n, value)::(col_idx, v)::cs
+        | (col_idx, v)::cs when col_idx = n -> if value =: A.zero then cs else (n, value)::cs 
+        | (col_idx, v)::cs -> (col_idx, v)::(set_col_in_row cs value)
+      in
+      let new_entries = List.mapi (fun row_idx row -> 
+          let value = V.nth new_col row_idx in
+          set_col_in_row row value
+        ) m.entries in
+      {entries = new_entries; column_count = m.column_count}
 
     let append_matrices m1 m2  =
       failwith "TODO"