From 315dac61fa1e11bb934194d74698849f44b9a834 Mon Sep 17 00:00:00 2001 From: Charlotte Brandt Date: Tue, 10 Dec 2024 13:54:07 +0100 Subject: [PATCH] appending and normalizing in is_covered_by - all tests pass --- .../arrayImplementation/arrayMatrix.ml | 6 +-- .../sparseImplementation/listMatrix.ml | 39 ++++++++++--------- 2 files changed, 23 insertions(+), 22 deletions(-) diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml index 7d640a7bdc..4e2d0f6e5e 100644 --- a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml +++ b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml @@ -57,14 +57,12 @@ module ArrayMatrix: AbstractMatrix = let add_empty_columns m cols = Timing.wrap "add_empty_cols" (add_empty_columns m) cols let append_row m row = - let () = Printf.printf "Before append_row m:\n%s\n" (show m) in let size = num_rows m in let new_matrix = Array.make_matrix (size + 1) (num_cols m) A.zero in for i = 0 to size - 1 do new_matrix.(i) <- m.(i) done; new_matrix.(size) <- V.to_array row; - let () = Printf.printf "After append_row m:\n%s\n" (show new_matrix) in new_matrix let get_row m n = @@ -319,12 +317,12 @@ 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 if num_rows m1 > num_rows m2 then false else - let m1' = copy m1 in - let m2' = copy m2 in let p2 = lazy (get_pivot_positions m2) in try ( for i = 0 to num_rows m1 - 1 do + (* check if there are rows in m1 and m2 that aren't equal *) if Array.exists2 (<>:) m1.(i) m2.(i) then let m1_i = Array.copy m1.(i) in for j = 0 to Array.length m1_i - 2 do diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml index 6264dce9d6..5b12192a4c 100644 --- a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml +++ b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml @@ -87,8 +87,6 @@ module ListMatrix: AbstractMatrix = Timing.wrap "add_empty_cols" (add_empty_columns m) cols let append_row m row = - let () = Printf.printf "Before append_row m:\n%s\n" (show m) in - let () = Printf.printf "After append_row m:\n%s\n" (show ( m @ [row])) in m @ [row] let get_row m n = @@ -305,23 +303,28 @@ module ListMatrix: AbstractMatrix = is_linearly_independent_rref new_v xs let is_covered_by m1 m2 = + Printf.printf "Is m1 covered by m2?\n m1:\n%sm2:\n%s" (show m1) (show m2); + match normalize @@ append_matrices m2 m1 with + | None -> false + | Some m -> let m2' = remove_zero_rows m in List.for_all2 (fun x y -> V.equal x y) m2 m2' + (*let () = Printf.printf "Is m1 covered by m2?\n m1:\n%sm2:\n%s" (show m1) (show m2) in if num_rows m1 > num_rows m2 then false else - let rec is_covered_by_helper m1 m2 = - match m1 with - | [] -> true - | v1::vs1 -> - let first_non_zero = V.findi_val_opt ((<>:) A.zero) v1 in - match first_non_zero with - | None -> true (* vs1 must also be zero-vectors because of rref *) - | Some (idx, _) -> - let m' = List.drop_while (fun v2 -> - match V.findi_val_opt ((<>:) A.zero) v2 with - | None -> true (* In this case, m2 only has zero rows after that *) - | Some (idx', _) -> idx' < idx - ) m2 in (* Only consider the part of m2 where the pivot is at a position useful for deleting first_non_zero of v1*) - let linearly_indep = is_linearly_independent_rref v1 m' in - if linearly_indep then false else is_covered_by_helper vs1 m' - in is_covered_by_helper m1 m2 + let rec is_covered_by_helper m1 m2 = + match m1 with + | [] -> true + | v1::vs1 -> + let first_non_zero = V.findi_val_opt ((<>:) A.zero) v1 in + match first_non_zero with + | None -> true (* vs1 must also be zero-vectors because of rref *) + | Some (idx, _) -> + let m' = List.drop_while (fun v2 -> + match V.findi_val_opt ((<>:) A.zero) v2 with + | None -> true (* In this case, m2 only has zero rows after that *) + | Some (idx', _) -> idx' < idx + ) m2 in (* Only consider the part of m2 where the pivot is at a position useful for deleting first_non_zero of v1*) + let linearly_indep = is_linearly_independent_rref v1 m' in + if linearly_indep then false else is_covered_by_helper vs1 m' + in is_covered_by_helper m1 m2*) let is_covered_by m1 m2 = Timing.wrap "is_covered_by" (is_covered_by m1) m2