Implement vector findi and minor bugfix in ListMatrix normalize

goblint · Nov 28, 2024 · bd81ac1 · bd81ac1
1 parent ad34bc7
commit bd81ac1
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git 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
@@ -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"