From 859ec26b7fbc661e0586ea96205e467abd02f852 Mon Sep 17 00:00:00 2001 From: Charlotte Brandt Date: Thu, 5 Dec 2024 16:50:53 +0100 Subject: [PATCH] normalize bug fix --- .../sparseImplementation/listMatrix.ml | 28 +++++++++++++++---- .../sparseImplementation/sparseVector.ml | 14 +++++----- 2 files changed, 29 insertions(+), 13 deletions(-) diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml index b580aad2af..6fabd9295d 100644 --- a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml +++ b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml @@ -77,6 +77,18 @@ 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 + + let div_row (row : V.t) (pivot : A.t) : V.t = + V.map_f_preserve_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 + let reduce_col m j = if is_empty m then m else @@ -97,7 +109,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 in - V.map2_f_preserve_zero (fun x y -> x -: s *: y) row pivot_row) + sub_scaled_row row pivot_row s) ) m let reduce_col_with_vec m j v = @@ -153,17 +165,18 @@ module ListMatrix: AbstractMatrix = List.filteri_map (fun i row -> if i < row_idx then None else Some (V.starting_from_nth col_idx row)) m in (* Function for finding first pivot in an extracted part of the matrix (row_idx and col_idx indicate which part of the original matrix) *) - let find_first_pivot m row_idx col_idx = + let find_first_pivot m' row_idx col_idx = if col_idx >= col_count then None else (* Finding pivot by extracting the minimum column index of the first non zero value of each row*) let (piv_row, piv_col, piv_val) = List.fold_lefti (fun (cur_row, cur_col, cur_val) i row -> let row_first_non_zero = V.findi_val_opt ((<>:) A.zero) row in match row_first_non_zero with | None -> (cur_row, cur_col, cur_val) - | Some (col_idx, value) -> if col_idx < cur_col then (row_idx + i, col_idx, value) else (cur_row, cur_col, cur_val) - ) (num_rows m, num_cols m, A.zero) m (* Initializing with max, so num_cols m indicates that pivot is not found *) + | Some (idx, value) -> let () = Printf.printf "We found first non-zero at index %i in row %i\n" idx i in + if idx < cur_col then (row_idx + i, idx, value) else (cur_row, cur_col, cur_val) + ) (num_rows m', num_cols m', A.zero) m' (* Initializing with max, so num_cols m indicates that pivot is not found *) in - if piv_col = (num_cols m) then None else Some (piv_row, piv_col, piv_val) + if piv_col = (num_cols m') then None else Some (piv_row, piv_col + col_idx, piv_val) in let affeq_rows_are_valid m = (* Check if the semantics of an rref-affeq matrix are correct *) let col_count = num_cols m in @@ -179,10 +192,13 @@ module ListMatrix: AbstractMatrix = match find_first_pivot m' row_idx col_idx with | None -> m (* No pivot found means already normalized*) | Some (piv_row_idx, piv_col_idx, piv_val) -> ( + let () = Printf.printf "The current matrix is: \n%s and the pivot is (%i, %i, %s)\n" (show m) piv_row_idx piv_col_idx (A.to_string piv_val) in let m = if piv_row_idx <> row_idx then swap_rows m row_idx piv_row_idx else m in let normalized_m = List.mapi (fun idx row -> if idx = row_idx then div_row row piv_val else row) m in let piv_row = (List.nth normalized_m row_idx) in - let subtracted_m = List.mapi (fun idx row -> if idx <> row_idx then sub_rows row piv_row else row) normalized_m in + let subtracted_m = List.mapi (fun idx row -> if idx <> row_idx then + let scale = V.nth row piv_col_idx in + sub_scaled_row row piv_row scale else row) normalized_m in let m' = dec_mat_2D m (row_idx + 1) (piv_col_idx + 1) in main_loop subtracted_m m' (row_idx + 1) (piv_col_idx + 1)) (* We start at piv_col_idx + 1 because every other col before that is zero at the bottom*) in diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml index 47d63ca87d..6f51f01d3c 100644 --- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml +++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml @@ -132,7 +132,7 @@ module SparseVector: AbstractVector = | _ -> aux (f_rem_zero acc xidx xval yval) xs ys in if v1.len <> v2.len then raise (Invalid_argument "Unequal lengths") else - to_vector (List.rev (aux [] v1.entries v2.entries)) v1.len + to_vector (List.rev (aux [] v1.entries v2.entries)) v1.len let fold_left_f_preserve_zero f acc v = @@ -191,12 +191,12 @@ module SparseVector: AbstractVector = (* Returns optional of (index * value) where f value evaluated to true *) let findi_val_opt f v = let rec find_zero_or_val vec last_col_idx = - match vec, last_col_idx with - | [], _ -> if v.len <> last_col_idx + 1 && f A.zero then Some (last_col_idx + 1, A.zero) else None - | (idx, value) :: xs, i -> - if idx <> last_col_idx + 1 && f A.zero then Some (last_col_idx + 1, A.zero) - else if f value then Some (idx, value) - else find_zero_or_val xs idx + match vec, last_col_idx with + | [], _ -> if v.len <> last_col_idx + 1 && f A.zero then Some (last_col_idx + 1, A.zero) else None + | (idx, value) :: xs, i -> + if idx <> last_col_idx + 1 && f A.zero then Some (last_col_idx + 1, A.zero) + else if f value then Some (idx, value) + else find_zero_or_val xs idx in find_zero_or_val v.entries (-1) let map f v =