From d71d7bde130bff32b930e5407504f5be27817b1b Mon Sep 17 00:00:00 2001 From: Charlotte Brandt Date: Tue, 10 Dec 2024 10:05:05 +0100 Subject: [PATCH] bugfix in add_empty_columns, behavious still differs from arraymatrix --- .../arrayImplementation/arrayMatrix.ml | 6 ++--- .../arrayImplementation/arrayVector.ml | 2 +- .../sparseImplementation/listMatrix.ml | 23 +++++++++++-------- .../sparseImplementation/sparseVector.ml | 4 ++-- src/cdomains/affineEquality/vector.ml | 2 +- 5 files changed, 20 insertions(+), 17 deletions(-) diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml index b9bd503ddc..eec27c0c48 100644 --- a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml +++ b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml @@ -39,7 +39,7 @@ module ArrayMatrix: AbstractMatrix = let copy m = Timing.wrap "copy" (copy) m let add_empty_columns m cols = - let () = Printf.printf "Before add_empty_columns m:\n%s\n" (show m) in + let () = Printf.printf "Before add_empty_columns m:\n%sindices: %s\n" (show m) (Array.fold_right (fun x s -> s ^ (Int.to_string x) ^ ",") cols "") in let nnc = Array.length cols in if is_empty m || nnc = 0 then m else let nr, nc = num_rows m, num_cols m in @@ -82,7 +82,7 @@ module ArrayMatrix: AbstractMatrix = Array.blit m (n + 1) new_matrix n (num_rows new_matrix - n)); new_matrix let get_col m n = - let () = Printf.printf "get_col %i of m:\n%s\n%s\n" n (show m) (V.show (V.of_array @@ Array.init (Array.length m) (fun i -> m.(i).(n)))) in + (*let () = Printf.printf "get_col %i of m:\n%s\n%s\n" n (show m) (V.show (V.of_array @@ Array.init (Array.length m) (fun i -> m.(i).(n)))) in*) V.of_array @@ Array.init (Array.length m) (fun i -> m.(i).(n)) let get_col m n = Timing.wrap "get_col" (get_col m) n @@ -286,7 +286,7 @@ module ArrayMatrix: AbstractMatrix = match rref_vec_with m' v' with | Some res -> let () = Printf.printf "After rref_vec we have m:\n%s\n" (show res) in Some (remove_zero_rows res) - | None -> None + | None -> let () = Printf.printf "After rref_vec there is no normalization\n" in None let rref_matrix_with m1 m2 = (*Similar to rref_vec_with but takes two matrices instead.*) diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml b/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml index 3bf873df78..622a12e328 100644 --- a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml +++ b/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml @@ -36,7 +36,7 @@ module ArrayVector: AbstractVector = let remove_at_indices v idx = failwith "TODO" - let insert_zero_at_indices v idx = failwith "TODO" + let insert_zero_at_indices v idx count = failwith "TODO" let set_nth_with v n new_val = if n >= Array.length v then failwith "n outside of Array range" else diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml index 3c67dfec02..ee200f1923 100644 --- a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml +++ b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml @@ -39,18 +39,21 @@ module ListMatrix: AbstractMatrix = Timing.wrap "copy" (copy) m let add_empty_columns m cols = - let () = Printf.printf "Before add_empty_columns m:\n%s\n" (show m) in + let () = Printf.printf "Before add_empty_columns m:\n%sindices: %s\n" (show m) (Array.fold_right (fun x s -> s ^ (Int.to_string x) ^ ",") cols "") in let cols = Array.to_list cols in let sorted_cols = List.sort Stdlib.compare cols in - let rec count_sorted_occ acc cols last count = + let rec count_sorted_occ acc cols last count = match cols with - | [] -> acc - | (x :: xs) when x = last -> count_sorted_occ acc xs x (count + 1) - | (x :: xs) -> count_sorted_occ ((last, count) :: acc) xs x 1 + | [] -> if count > 0 then (last, count) :: acc else acc + | x :: xs when x = last -> count_sorted_occ acc xs x (count + 1) + | x :: xs -> let acc = if count > 0 then (last, count) :: acc else acc in + count_sorted_occ acc xs x 1 in - let occ_cols = count_sorted_occ [] sorted_cols (-1) 0 in - let () = Printf.printf "After add_empty_columns m:\n%s\n" (show (List.map (fun row -> V.insert_zero_at_indices row occ_cols) m)) in - List.map (fun row -> V.insert_zero_at_indices row occ_cols) m + let occ_cols = List.rev @@ count_sorted_occ [] sorted_cols 0 0 in + (*let () = Printf.printf "sorted cols is: %s\n" (List.fold_right (fun x s -> (Int.to_string x) ^ s) sorted_cols "") in + let () = Printf.printf "sorted_occ is: %s\n" (List.fold_right (fun (i, count) s -> "(" ^ (Int.to_string i) ^ "," ^ (Int.to_string count) ^ ")" ^ s) occ_cols "") in*) + let () = Printf.printf "After add_empty_columns m:\n%s\n" (show (List.map (fun row -> V.insert_zero_at_indices row occ_cols (List.length cols)) m)) in + List.map (fun row -> V.insert_zero_at_indices row occ_cols (List.length cols)) m let add_empty_columns m cols = Timing.wrap "add_empty_cols" (add_empty_columns m) cols @@ -68,7 +71,7 @@ module ListMatrix: AbstractMatrix = List.remove_at n m let get_col m n = - let () = Printf.printf "get_col %i of m:\n%s\n%s\n" n (show m) (V.show (V.of_list @@ List.map (fun row -> V.nth row n) m)) in + (*let () = Printf.printf "get_col %i of m:\n%s\n%s\n" n (show m) (V.show (V.of_list @@ List.map (fun row -> V.nth row n) m)) in*) V.of_list @@ List.map (fun row -> V.nth row n) m (* builds full col including zeros, maybe use sparselist instead? *) let get_col m n = @@ -246,7 +249,7 @@ module ListMatrix: AbstractMatrix = match normalize @@ append_matrices m (init_with_vec v) with | Some res -> let () = Printf.printf "After rref_vec we have m:\n%s\n" (show res) in Some (remove_zero_rows res) - | None -> None + | None -> let () = Printf.printf "After rref_vec there is no normalization\n " in None (*Similar to rref_vec_with but takes two matrices instead.*) (*ToDo Could become inefficient for large matrices since pivot_elements are always recalculated + many row additions*) diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml index 76646527ed..51753475e6 100644 --- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml +++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml @@ -80,7 +80,7 @@ module SparseVector: AbstractVector = in {entries = remove_indices_helper v.entries idx 0; len = v.len - List.length idx} - let insert_zero_at_indices v idx = + let insert_zero_at_indices v idx count = let rec add_indices_helper vec idx added_count = match vec, idx with | [], [] -> [] @@ -90,7 +90,7 @@ module SparseVector: AbstractVector = | ((col_idx, value) :: xs), ((i, count) :: ys) when i < col_idx -> (col_idx + added_count + count, value) :: add_indices_helper xs ys (added_count + count) | ((col_idx, value) :: xs), ((i, count) :: ys) -> (col_idx + added_count, value) :: add_indices_helper xs idx added_count in - {entries = add_indices_helper v.entries idx 0; len = v.len + List.length idx} + {entries = add_indices_helper v.entries idx 0; len = v.len + count} let set_nth v n num = (* TODO: Optimize! *) if n >= v.len then failwith "Out of bounds" diff --git a/src/cdomains/affineEquality/vector.ml b/src/cdomains/affineEquality/vector.ml index 15215b5512..f52f6eadbb 100644 --- a/src/cdomains/affineEquality/vector.ml +++ b/src/cdomains/affineEquality/vector.ml @@ -12,7 +12,7 @@ sig val remove_at_indices: t -> int list -> t - val insert_zero_at_indices: t -> (int * int) list -> t + val insert_zero_at_indices: t -> (int * int) list -> int -> t val set_nth: t -> int -> num -> t