From 680e56ba3ba99a8226fa0d5857d58e35ae686e16 Mon Sep 17 00:00:00 2001 From: Kevin Adameit Date: Thu, 28 Nov 2024 16:43:01 +0100 Subject: [PATCH] Reimplemented normalize in SparseMatrix, some TODOs missing --- .../arrayImplementation/arrayMatrix.ml | 3 + src/cdomains/affineEquality/matrix.ml | 2 + .../sparseImplementation/sparseMatrix.ml | 97 ++++++++----------- src/cdomains/affineEquality/vector.ml | 2 + 4 files changed, 45 insertions(+), 59 deletions(-) diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml index dc24b7f641..9212cf501f 100644 --- a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml +++ b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml @@ -355,4 +355,7 @@ module ArrayMatrix: AbstractMatrix = map2i_with f m' v; m' + let swap_rows m j k = + failwith "TODO" + end \ No newline at end of file diff --git a/src/cdomains/affineEquality/matrix.ml b/src/cdomains/affineEquality/matrix.ml index 33a622d81a..3b45c12f91 100644 --- a/src/cdomains/affineEquality/matrix.ml +++ b/src/cdomains/affineEquality/matrix.ml @@ -71,4 +71,6 @@ sig val copy: t -> t + val swap_rows: t -> int -> int -> t + end \ No newline at end of file diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/sparseMatrix.ml index d961b2a59c..658e8b4c7e 100644 --- a/src/cdomains/affineEquality/sparseImplementation/sparseMatrix.ml +++ b/src/cdomains/affineEquality/sparseImplementation/sparseMatrix.ml @@ -184,75 +184,54 @@ module ListMatrix: AbstractMatrix = failwith "deprecated" let normalize_with m = Timing.wrap "normalize_with" normalize_with m - + + + let sub_rows (minu : V.t) (subt : V.t) : V.t = + V.map2_preserve_zero (-:) minu subt + + let div_row (row : V.t) (pivot : A.t) : V.t = + V.map_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 k else row) m + let normalize (m : t) : t Option.t = - let entries = m in let col_count = num_cols m in - let swap_rows (m : t) (r1_idx : int) (r2_idx : int) : t = - failwith "TODO" - (* - List.mapi (fun i row -> - if i = r1_idx then List.nth m r2_idx - else if i = r2_idx then List.nth m r1_idx - else row - ) entries*) - in - let rec sub_rows (minu : V.t) (subt : V.t) : (int * A.t) list = - failwith "TODO" - (* - match minu, subt with - | ((xidx, xv)::xs, (yidx,yv)::ys) -> ( - match xidx - yidx with - | d when d = 0 && xv <> yv -> (xidx, xv -: yv)::(sub_rows xs ys) - | d when d < 0 -> (xidx, xv)::(sub_rows xs ((yidx, yv)::ys)) - | d when d > 0 -> (yidx, A.zero -: yv)::(sub_rows ((xidx, xv)::xs) ys) - | _ -> sub_rows xs ys ) (* remove row when is (0, 0) *) - | ([], (yidx, yv)::ys) -> (yidx, A.zero -: yv)::(sub_rows [] ys) - | ((xidx, xv)::xs, []) -> (xidx, xv)::(sub_rows xs []) - | ([],[]) -> [] - *) - in - let div_row (row : V.t) (pivot : A.t) : V.t = - failwith "TODO" - (* - List.map (fun (idx, value) -> (idx, value /: pivot)) row - *) - in - let dec_mat_2D (m : t) : t = + + let dec_mat_2D (m : t) (row_idx : int) (col_idx : int) : t = m in - let rec find_pivot_in_col (m : t) (row_idx : int) (col_idx : int) : (int * A.t) Option.t = - failwith "TODO" - (* - match m with - | ((idx, value)::_)::xs -> if idx = col_idx then Some (row_idx, value) else find_pivot_in_col xs (row_idx + 1) col_idx - | ([])::xs -> find_pivot_in_col xs (row_idx + 1) col_idx - | [] -> None - *) - in - (* let rec find_pivot m col_idx row_idx = - if col_idx >= col_count then None else - match find_pivot_in_col m col_idx row_idx with - | Some (row_idx, value) -> Some (row_idx, value) - | None -> find_pivot m (col_idx + 1) row_idx - in *) + (* Function for finding a pivot in an extracted part of the matrix (row_idx and col_idx indicate which part of the original matrix) *) + let rec find_pivot (m : t) (row_idx : int) (col_idx : int) : (int * int * A.t) Option.t = + if col_idx >= col_count then None else + let get_first_non_zero v = (* Returns (col_idx, value) of first non-zero row*) + let v' = V.to_sparse_list v in + match v' with + | [] -> None + | (idx, value)::_ -> Some (idx, value) + in + (* 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 = get_first_non_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 (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 *) + in + if piv_col = (num_cols m) then None else Some (piv_row, piv_col, piv_val) + in let rec main_loop (m : t) (m' : t) (row_idx : int) (col_idx : int) : t = - failwith "TODO" - (* - if col_idx = (col_count - 1) (* In this case the whole bottom of the matrix starting from row_index is Zero, so it is normalized *) - then m + if col_idx = (col_count - 1) then m (* In this case the whole bottom of the matrix starting from row_index is Zero, so it is normalized *) else - match find_pivot_in_col m' row_idx col_idx with - | None -> main_loop m m' row_idx (col_idx + 1) - | Some (piv_row_idx, piv_val) -> ( + match find_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 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 m' = dec_mat_2D m in - main_loop subtracted_m m' (row_idx + 1) (col_idx + 1) - ) - *) + 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 let m' = main_loop m m 0 0 in Some m' diff --git a/src/cdomains/affineEquality/vector.ml b/src/cdomains/affineEquality/vector.ml index 9da0729cc5..0412c05356 100644 --- a/src/cdomains/affineEquality/vector.ml +++ b/src/cdomains/affineEquality/vector.ml @@ -19,7 +19,9 @@ sig val insert_val_at: int -> num -> t -> t val map_preserve_zero: (num -> num) -> t -> t + val map2_preserve_zero: (num -> num -> num) -> t -> t -> t + val apply_with_c: (num -> num -> num) -> num -> t -> t val apply_with_c_with: (num -> num -> num) -> num -> t -> unit