From bd81ac15d0726adc1207c0cc04121ff7ccf27568 Mon Sep 17 00:00:00 2001 From: Kevin Adameit Date: Thu, 28 Nov 2024 18:00:42 +0100 Subject: [PATCH] Implement vector findi and minor bugfix in ListMatrix normalize --- .../affineEquality/sparseImplementation/listMatrix.ml | 2 +- .../affineEquality/sparseImplementation/sparseVector.ml | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml index a4b66bf4b2..4fb1f80969 100644 --- a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml +++ b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml @@ -198,7 +198,7 @@ module ListMatrix: AbstractMatrix = 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) + | 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 *) in if piv_col = (num_cols m) then None else Some (piv_row, piv_col, piv_val) diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml index f8b65afb9a..1fefe8e545 100644 --- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml +++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml @@ -151,7 +151,10 @@ module SparseVector: AbstractVector = failwith "deprecated" let findi f v = - failwith "TODO" + if f A.zero then + fst @@ List.findi (fun i (idx, value) -> if idx > i then true else f value) v.entries (* Here fst is the iteration variable i, not the tuple idx *) + else + fst @@ List.find (fun (idx, value) -> f value) v.entries (* Here fst is the idx contained in the found tuple *) let map f v = failwith "TODO"