diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml b/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml index a95e764f16..911e96fd4b 100644 --- a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml +++ b/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!" diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml index 6589296884..0640e31a86 100644 --- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml +++ b/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')) diff --git a/src/cdomains/affineEquality/vector.ml b/src/cdomains/affineEquality/vector.ml index 61a18ff7c2..956c6aa1ea 100644 --- a/src/cdomains/affineEquality/vector.ml +++ b/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 diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 15fc35fa59..2e9676382f 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/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 ()