Skip to content

Commit

Permalink
Change order of functions because of compilation error
Browse files Browse the repository at this point in the history
  • Loading branch information
GollokG committed Dec 19, 2024
1 parent bb15181 commit 0678f66
Showing 1 changed file with 9 additions and 9 deletions.
18 changes: 9 additions & 9 deletions src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
Original file line number Diff line number Diff line change
Expand Up @@ -193,6 +193,15 @@ module ListMatrix: AbstractMatrix =
if affeq_rows_are_valid m' then Some m' else None (* TODO: We can check this for each row, using the helper function row_is_invalid *)


(* This function return a tuple of row index and pivot position (column) in m *)
(* TODO: maybe we could use a Hashmap instead of a list? *)
let get_pivot_positions (m : t) : (int * int) list =
List.rev @@ List.fold_lefti (
fun acc i row -> match V.find_first_non_zero row with
| None -> acc
| Some (pivot_col, _) -> (i, pivot_col) :: acc
) [] m

let assert_rref m =
let pivot_l = get_pivot_positions m in
let rec validate m i =
Expand All @@ -212,15 +221,6 @@ module ListMatrix: AbstractMatrix =
in if validate_vec pivot_l then validate vs (i+1) else raise (Invalid_argument "Matrix not in rref: pivot column not empty!")
in validate m 0

(* This function return a tuple of row index and pivot position (column) in m *)
(* TODO: maybe we could use a Hashmap instead of a list? *)
let get_pivot_positions (m : t) : (int * int) list =
List.rev @@ List.fold_lefti (
fun acc i row -> match V.find_first_non_zero row with
| None -> acc
| Some (pivot_col, _) -> (i, pivot_col) :: acc
) [] m

(* Sets the jth column to zero by subtracting multiples of v *)
let reduce_col_with_vec m j v =
let pivot_element = V.nth v j in
Expand Down

0 comments on commit 0678f66

Please sign in to comment.