From 4411280f9fe552bc361cc3471d2ec34ff8f6b4f2 Mon Sep 17 00:00:00 2001 From: Kevin Adameit Date: Thu, 19 Dec 2024 15:37:19 +0100 Subject: [PATCH] Implement zero preserving Array Vector functions by calling normal functions --- .../arrayImplementation/arrayMatrix.ml | 3 ++- .../arrayImplementation/arrayVector.ml | 20 +++++++++++++------ 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml index ac21c08fbe..af849eef0c 100644 --- a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml +++ b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml @@ -318,7 +318,8 @@ module ArrayMatrix: AbstractMatrix = let is_covered_by m1 m2 = (*Performs a partial rref reduction to check if concatenating both matrices and afterwards normalizing them would yield a matrix <> m2 *) (*Both input matrices must be in rref form!*) - let () = Printf.printf "Is m1 covered by m2?\n m1:\n%sm2:\n%s" (show m1) (show m2) in + let () = Printf.printf "is_covered_by m1: \n%s " (show m1) in + let () = Printf.printf "is_covered_by m2 \n%s " (show m2) in if num_rows m1 > num_rows m2 then false else let p2 = lazy (get_pivot_positions m2) in try ( diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml b/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml index 911e96fd4b..e90a5afbce 100644 --- a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml +++ b/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml @@ -57,7 +57,9 @@ module ArrayVector: AbstractVector = let is_zero_vec v = not (Array.exists (fun x -> x <>: A.zero) v) - let is_const_vec v = failwith "Never implemented!" + let is_const_vec v = + compare_length_with (filteri (fun i x -> (*Inefficient*) + compare_length_with v (i + 1) > 0 && x <>: A.zero) v) 1 = 0 let nth = Array.get @@ -108,11 +110,17 @@ module ArrayVector: AbstractVector = let find_opt f v = failwith "Never implemented!" - let map_f_preserves_zero f v = failwith "Never implemented!" - let map2_f_preserves_zero f v1 v2 = failwith "Never implemented!" + let map_f_preserves_zero f v = + map f v - let mapi_f_preserves_zero f v = failwith "Never implemented!" - let map2i_f_preserves_zero f v v' = failwith "Never implemented!" + let map2_f_preserves_zero f v1 v2 = + map2 f v1 v2 + + let mapi_f_preserves_zero f v = + mapi f v + + let map2i_f_preserves_zero f v v' = + map2i f v v' let fold_left_f_preserves_zero f acc v = failwith "Never implemented!" @@ -133,5 +141,5 @@ module ArrayVector: AbstractVector = failwith "Never implemented!" let apply_with_c_f_preserves_zero f c v = - failwith "Never implemented!" + apply_with_c f c v end \ No newline at end of file