ein paar maps ausgetauscht

src/cdomains/affineEquality/arrayImplementation/arrayVector.ml

@@ -111,6 +111,9 @@ module ArrayVector: AbstractVector =
     let map_f_preserves_zero f v = failwith "Never implemented!"
     let map2_f_preserves_zero f v1 v2 = failwith "Never implemented!"
 
+    let mapi_f_preserves_zero f v = failwith "Never implemented!"
+    let map2i_f_preserves_zero f v v' = failwith "Never implemented!"
+
     let fold_left_f_preserves_zero f acc v =
       failwith "Never implemented!"
 

src/cdomains/affineEquality/sparseImplementation/sparseVector.ml

@@ -95,6 +95,9 @@ module SparseVector: AbstractVector =
           ) [] v.entries in
         {entries = entries'; len = v.len + 1}
 
+    let map f v = 
+      of_list (List.map f (to_list v))
+
     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 
@@ -103,6 +106,10 @@ module SparseVector: AbstractVector =
 
     let map_f_preserves_zero f v = Timing.wrap "map_f_preserves_zero" (map_f_preserves_zero f) v
 
+    let map2 f v v' = (* TODO: Optimize! *)
+      if v.len <> v'.len then failwith "Unequal vector length" else 
+        of_list (List.map2 f (to_list v) (to_list v'))
+
     (* 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_preserves_zero f v1 v2 =
       let f_rem_zero acc idx e1 e2 =
@@ -125,6 +132,20 @@ module SparseVector: AbstractVector =
 
     let map2_f_preserves_zero f v1 v2 = Timing.wrap "map2_f_preserves_zero" (map2_f_preserves_zero f v1) v2
 
+    let map2i f v v' = (* TODO: optimize! *)
+      of_list (List.map2i f (to_list v) (to_list v'))
+
+    let map2i_f_preserves_zero f v v' = failwith "TODO"
+
+    let mapi f v  = (* TODO: optimize! *)
+      of_list (List.mapi f (to_list v))
+
+    let mapi_f_preserves_zero f v =
+      let entries' = List.filter_map (
+          fun (idx, value) -> let new_val = f idx value in 
+            if new_val = A.zero then None else Some (idx, new_val)) v.entries in 
+      {entries = entries'; len = v.len}
+
     let fold_left_f_preserves_zero f acc v =
       List.fold_left (fun acc (_, value) -> f acc value) acc v.entries
 
@@ -168,10 +189,6 @@ module SparseVector: AbstractVector =
     let length v =
       v.len
 
-    let map2 f v v' = (* TODO: Optimize! *)
-      if v.len <> v'.len then failwith "Unequal vector length" else 
-        of_list (List.map2 f (to_list v) (to_list v'))
-
     let apply_with_c_f_preserves_zero f c v =
       let entries' = List.filter_map (fun (idx, value) -> let new_val = f value c in if new_val =: A.zero then None else Some (idx, new_val)) v.entries in
       {entries = entries'; len = v.len}
@@ -206,9 +223,6 @@ module SparseVector: AbstractVector =
 
     let find_first_non_zero v = Timing.wrap "find_first_non_zero" (find_first_non_zero) v
 
-    let map f v = 
-      of_list (List.map f (to_list v))
-
     let compare_length_with v n = 
       Int.compare v.len n
 
@@ -234,12 +248,6 @@ module SparseVector: AbstractVector =
       let entries' = List.rev @@ List.map (fun (idx, value) -> (v.len - 1 - idx, value)) v.entries in 
       {entries = entries'; len = v.len}
 
-    let map2i f v v' = (* TODO: optimize! *)
-      of_list (List.map2i f (to_list v) (to_list v'))
-
-    let mapi f v  = (* TODO: optimize! *)
-      of_list (List.mapi f (to_list v))
-
     let find2i f v v' = (* TODO: optimize! *)
       fst @@ List.findi (fun _ (val1, val2) -> (uncurry f) (val1, val2)) (List.combine (to_list v) (to_list v'))
 

src/cdomains/affineEquality/vector.ml

@@ -72,8 +72,12 @@ sig
 
   val map2i: (int -> num -> num -> num) -> t -> t -> t
 
+  val map2i_f_preserves_zero: (int -> num -> num -> num) -> t -> t -> t
+
   val mapi: (int -> num -> num) -> t -> t
 
+  val mapi_f_preserves_zero: (int -> num -> num) -> t -> t
+
   val mapi: (int -> num -> num) -> t -> t
 
   val find2i: (num -> num -> bool) -> t -> t -> int

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -286,7 +286,7 @@ struct
       if s >= Matrix.num_cols a then a else
         let case_two a r col_b =
           let a_r = Matrix.get_row a r in
-          let a = Matrix.map2i (fun i x y -> if i < r then Vector.map2 (fun u j -> u +: y *: j) x a_r else x) a col_b; in
+          let a = Matrix.map2i (fun i x y -> if i < r then Vector.map2_f_preserves_zero (fun u j -> u +: y *: j) x a_r else x) a col_b; in
           Matrix.remove_row a r
         in
         let case_three a b col_a col_b max =
@@ -397,7 +397,7 @@ struct
     let assign_invertible_rels x var b env = Timing.wrap "assign_invertible" (assign_invertible_rels x var b) env in
     let assign_uninvertible_rel x var b env =
       let b_length = Vector.length b in
-      let b = Vector.mapi (fun i z -> if i < b_length - 1 then Mpqf.neg z else z) b in
+      let b = Vector.mapi_f_preserves_zero (fun i z -> if i < b_length - 1 then Mpqf.neg z else z) b in
       let b = Vector.set_nth b (Environment.dim_of_var env var) Mpqf.one in
       match Matrix.rref_vec x b with
       | None -> bot ()