Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…

…nt-sparsification

src/cdomains/affineEquality/arrayImplementation/arrayVector.ml

@@ -114,13 +114,13 @@ module ArrayVector: AbstractVector =
     let find_opt f v =
       failwith "TODO"
 
-    let map_f_preserve_zero f v = failwith "TODO"
-    let map2_f_preserve_zero f v1 v2 = failwith "TODO"
+    let map_f_preserves_zero f v = failwith "TODO"
+    let map2_f_preserves_zero f v1 v2 = failwith "TODO"
 
-    let fold_left_f_preserve_zero f acc v =
+    let fold_left_f_preserves_zero f acc v =
       failwith "TODO"
 
-    let fold_left2_f_preserve_zero f acc v v' =
+    let fold_left2_f_preserves_zero f acc v v' =
       failwith "TODO"
 
     let findi_val_opt f v =

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

@@ -78,16 +78,16 @@ module ListMatrix: AbstractMatrix =
     let equal m1 m2 = Timing.wrap "equal" (equal m1) m2
 
     let sub_rows (minu : V.t) (subt : V.t) : V.t =
-      V.map2_f_preserve_zero (-:) minu subt
+      V.map2_f_preserves_zero (-:) minu subt
 
     let div_row (row : V.t) (pivot : A.t) : V.t =
-      V.map_f_preserve_zero (fun a -> a /: pivot) row
+      V.map_f_preserves_zero (fun a -> a /: pivot) row
 
     let swap_rows m j k =
       List.mapi (fun i row -> if i = j then List.nth m k else if i = k then List.nth m j else row) m
 
     let sub_scaled_row row1 row2 s =
-      V.map2_f_preserve_zero (fun x y -> x -: s *: y) row1 row2
+      V.map2_f_preserves_zero (fun x y -> x -: s *: y) row1 row2
 
     let reduce_col m j = 
       let () = Printf.printf "We are reducing matrix m:\n%s with %i\n" (show m) j in
@@ -120,7 +120,7 @@ module ListMatrix: AbstractMatrix =
           let row_value = V.nth row j in 
           if row_value = A.zero then row
           else (let s = row_value /: pivot_element in
-                V.map2_f_preserve_zero (fun x y -> x -: s *: y) row v)            
+                V.map2_f_preserves_zero (fun x y -> x -: s *: y) row v)            
         ) m
 
     let del_col m j =
@@ -152,10 +152,10 @@ module ListMatrix: AbstractMatrix =
       List.mapi (fun i row -> V.findi (fun z -> z =: A.one) row) m
 
     let sub_rows (minu : V.t) (subt : V.t) : V.t =
-      V.map2_f_preserve_zero (-:) minu subt
+      V.map2_f_preserves_zero (-:) minu subt
 
     let div_row (row : V.t) (pivot : A.t) : V.t =
-      V.map_f_preserve_zero (fun a -> a /: pivot) row
+      V.map_f_preserves_zero (fun a -> a /: pivot) row
 
     let swap_rows m j k =
       List.mapi (fun i row -> if i = j then List.nth m k else if i = k then List.nth m j else row) m
@@ -235,7 +235,7 @@ module ListMatrix: AbstractMatrix =
         match pivot_opt with
         | None -> false (* When we found no pivot, the vector is already A.zero. *)
         | Some (pivot_id, pivot) ->
-          let new_v = V.map2_f_preserve_zero (fun v1 v2 -> v1 -: (pivot *: v2)) v x in
+          let new_v = V.map2_f_preserves_zero (fun v1 v2 -> v1 -: (pivot *: v2)) v x in
           is_linearly_independent_rref new_v xs
 
     let is_covered_by m1 m2 =

src/cdomains/affineEquality/sparseImplementation/sparseVector.ml

@@ -108,14 +108,14 @@ module SparseVector: AbstractVector =
           ) [] (List.rev v.entries) in
         {entries = List.sort (fun (i, _) (j, _) -> Int.compare i j) entries'; len = v.len + 1}
 
-    let map_f_preserve_zero f v = (* map for functions f such that f 0 = 0 since f won't be applied to zero values. See also map *)
+    let map_f_preserves_zero f v = (* map for functions f such that f 0 = 0 since f won't be applied to zero values. See also map *)
       let entries' = List.filter_map (
           fun (idx, value) -> let new_val = f value in 
             if new_val = A.zero then None else Some (idx, new_val)) v.entries in 
       {entries = entries'; len = v.len}
 
     (* map for functions f such that f 0 0 = 0 since f won't be applied to if both values are zero. See also map *)
-    let map2_f_preserve_zero f v1 v2 =
+    let map2_f_preserves_zero f v1 v2 =
       let f_rem_zero acc idx e1 e2 =
         let r = f e1 e2 in 
         if r =: A.zero then acc else (idx, r)::acc
@@ -135,11 +135,23 @@ module SparseVector: AbstractVector =
         to_vector (List.rev (aux [] v1.entries v2.entries)) v1.len
 
 
-    let fold_left_f_preserve_zero f acc v =
+    let fold_left_f_preserves_zero f acc v =
       List.fold_left (fun acc (_, value) -> f acc value) acc v.entries
 
-    let fold_left2_f_preserve_zero f acc v v' =
-      List.fold_left2 (fun acc (_, value) (_, value') -> f acc value value') acc v.entries v'.entries
+    let fold_left2_f_preserves_zero f acc v v' =  
+      let rec aux acc v1 v2 =
+        match v1, v2 with 
+        | [], [] -> acc 
+        | [], (yidx, yval)::ys -> aux (f acc A.zero yval) [] ys
+        | (xidx, xval)::xs, [] -> aux (f acc xval A.zero) xs []
+        | (xidx, xval)::xs, (yidx, yval)::ys -> 
+          match xidx - yidx with
+          | d when d < 0 -> aux (f acc xval A.zero) xs v2
+          | d when d > 0 -> aux (f acc A.zero yval) v1 ys
+          | _            -> aux (f acc xval yval) xs ys
+      in
+      if v.len <> v'.len then raise (Invalid_argument "Unequal lengths") else 
+        (aux acc v.entries v'.entries)
 
     let apply_with_c f c v =
       let entries' = List.map (fun (idx, value) -> (idx, f value c)) v.entries in

src/cdomains/affineEquality/vector.ml

@@ -20,13 +20,13 @@ sig
 
   val insert_val_at: int -> num ->  t ->  t
 
-  val map_f_preserve_zero: (num -> num) -> t -> t
+  val map_f_preserves_zero: (num -> num) -> t -> t
 
-  val map2_f_preserve_zero: (num -> num -> num) -> t ->  t -> t
+  val map2_f_preserves_zero: (num -> num -> num) -> t ->  t -> t
 
-  val fold_left_f_preserve_zero: ('acc -> num -> 'acc) -> 'acc -> t -> 'acc
+  val fold_left_f_preserves_zero: ('acc -> num -> 'acc) -> 'acc -> t -> 'acc
 
-  val fold_left2_f_preserve_zero: ('acc -> num -> num -> 'acc) -> 'acc -> t -> t -> 'acc
+  val fold_left2_f_preserves_zero: ('acc -> num -> num -> 'acc) -> 'acc -> t -> t -> 'acc
 
   val apply_with_c: (num -> num -> num) -> num ->  t ->  t