From 0c9eb46b98bdd0ee7ae209df6fabe7df0f551dc3 Mon Sep 17 00:00:00 2001 From: Kevin Adameit Date: Tue, 26 Nov 2024 19:40:47 +0100 Subject: [PATCH] Vector functions --- .../sparseImplementation/sparseMatrix.ml | 4 +- .../sparseImplementation/sparseVector.ml | 39 ++++++++++++------- src/cdomains/affineEquality/vector.ml | 2 +- 3 files changed, 28 insertions(+), 17 deletions(-) diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/sparseMatrix.ml index dbaeb5192a..1ba26f2771 100644 --- a/src/cdomains/affineEquality/sparseImplementation/sparseMatrix.ml +++ b/src/cdomains/affineEquality/sparseImplementation/sparseMatrix.ml @@ -146,7 +146,9 @@ module ListMatrix: AbstractMatrix = {entries = entries'; column_count = m.column_count} let del_col m j = - List.map (fun row -> V.remove_nth row j) m + if num_cols m = 1 then empty () + else + List.map (fun row -> V.remove_nth row j) m let del_cols m cols = if (Array.length cols) = num_cols m then empty() diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml index c8540cb121..4b1754d8f5 100644 --- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml +++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml @@ -41,6 +41,19 @@ module SparseVector: AbstractVector = if n >= v.len then v else (*could be left out but maybe performance??*) {entries = remove_nth_vec v.entries n; len = v.len - 1} + (* TODO: Which of both remmove_nth should we use *) + let remove_nth v n = + if n >= v.len then failwith "Out of bounds" + else + let new_entries = List.filter_map (fun (col_idx, value) -> + if col_idx = n + then None + else if col_idx > n + then Some (col_idx - 1, value) + else Some (col_idx, value) + ) v.entries in + {entries = new_entries; len = v.len - 1} + let remove_at_indices v idx = let rec remove_indices_helper vec idx deleted_count = match vec, idx with @@ -52,16 +65,14 @@ module SparseVector: AbstractVector = in {entries = remove_indices_helper v.entries idx 0; len = v.len - List.length idx} - let set_nth v n m = - let rec set_nth_vec v n m = - match v with - | x::xs -> if fst x = n then (n, m)::xs else - if fst x < n then x::(set_nth_vec xs n m) - else v - | [] -> [] - in - if n >= v.len then failwith "Out of bounds" else - {entries=set_nth_vec v.entries n m; len=v.len} + let set_nth v n num = + if n >= v.len then failwith "Out of bounds" + else + let new_entries = List.map (fun (col_idx, value) -> + if col_idx = n then (col_idx, num) else (col_idx, value) + ) v.entries + in + {entries= new_entries; len=v.len} let set_nth_with = failwith "deprecated" @@ -108,12 +119,13 @@ module SparseVector: AbstractVector = else let rec nth v = match v with | [] -> A.zero + | (col_idx, value) :: xs when col_idx > n -> A.zero | (col_idx, value) :: xs when col_idx = n -> value | (col_idx, value) :: xs -> nth xs in nth v.entries let length v = - failwith "TODO" + v.len let map2 f v v' = failwith "TODO" @@ -183,10 +195,7 @@ module SparseVector: AbstractVector = let to_sparse_list v = v.entries - let remove_nth v n = - failwith "TODO" - let find_opt f v = - failwith "TODO" + failwith "TODO: Do we need this?" end \ No newline at end of file diff --git a/src/cdomains/affineEquality/vector.ml b/src/cdomains/affineEquality/vector.ml index f374853b27..a673b820c7 100644 --- a/src/cdomains/affineEquality/vector.ml +++ b/src/cdomains/affineEquality/vector.ml @@ -36,7 +36,7 @@ sig val findi: (num -> bool) -> t -> int - val find_opt: (num -> bool) -> t -> t Option.t + val find_opt: (num -> bool) -> t -> num Option.t val map: (num -> num) -> t -> t