diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml b/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml index 24ad36323f..937c4ee36f 100644 --- a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml +++ b/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml @@ -129,4 +129,7 @@ module ArrayVector: AbstractVector = let exists2 f v1 v1 = failwith "TODO / deprecated" + let starting_from_nth n v = + failwith "TODO / deprecated" + end \ No newline at end of file diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml index 6cb170034e..e04fe6a174 100644 --- a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml +++ b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml @@ -148,17 +148,18 @@ module ListMatrix: AbstractMatrix = List.mapi (fun i row -> if i = j then List.nth m k else if i = k then List.nth m j else row) m let is_valid_affeq_matrix m = - failwith "TODO" - (* let col_count = num_cols m in - List.exists (fun row -> (* Invalid if row is zero, but coefficient is not zero *) - V.fold_left_preserve_zero (fun found_non_zero (col_idx, value) -> if col_idx = col_count - 1 && (not found_non_zero) && (value <>: A.zero) then false else found_non_zero) false row - *) + let row_is_invalid row = (* TODO: Vector findi_opt *) + match V.findi_val_opt ((<>:) A.zero) row with + | Some (idx, _) -> if idx = col_count - 1 then true else false (* If all cofactors of the affeq are zero, but the constant is non-zero, the row is invalid *) + | None -> false (* Full zero row is not invalid *) + in + List.exists row_is_invalid m let normalize m = let col_count = num_cols m in let dec_mat_2D (m : t) (row_idx : int) (col_idx : int) : t = - m + List.filteri_map (fun i row -> if i < row_idx then None else Some (V.starting_from_nth col_idx row)) m in (* Function for finding first pivot in an extracted part of the matrix (row_idx and col_idx indicate which part of the original matrix) *) let find_first_pivot m row_idx col_idx = @@ -187,7 +188,7 @@ module ListMatrix: AbstractMatrix = main_loop subtracted_m m' (row_idx + 1) (piv_col_idx + 1)) (* We start at piv_col_idx + 1 because every other col before that is zero at the bottom*) in let m' = main_loop m m 0 0 in - if is_valid_affeq_matrix m' then Some m' else None + if is_valid_affeq_matrix m' then Some m' else None (* TODO: We can check this for each row, using the helper function row_is_invalid *) (*This function yields the same result as appending vector v to m and normalizing it afterwards would. However, it is usually faster than performing those ops manually.*) diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml index 2c44f7c9fe..cad838a474 100644 --- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml +++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml @@ -215,7 +215,7 @@ module SparseVector: AbstractVector = let append v v' = let entries' = v.entries @ List.map (fun (idx, value) -> (idx + v.len), value) v'.entries in {entries = entries'; len = v.len + v'.len} - + let exists f v = let c = v.len in let rec exists_aux at f v = @@ -261,6 +261,10 @@ module SparseVector: AbstractVector = let find_opt f v = (* TODO: Do we need this? And optimize!!!*) List.find_opt f (to_list v) + let starting_from_nth n v = + let entries' = List.filter_map (fun (idx, value) -> if idx < n then None else Some (idx - n, value)) v.entries in + {entries = entries'; len = v.len - n} + let show v = let t = to_list v in let rec list_str l = @@ -293,4 +297,5 @@ module SparseVector: AbstractVector = let set_nth_with f n num = ( failwith "set_nth_with deprecated") + end diff --git a/src/cdomains/affineEquality/vector.ml b/src/cdomains/affineEquality/vector.ml index 623c338dcd..7b067018e4 100644 --- a/src/cdomains/affineEquality/vector.ml +++ b/src/cdomains/affineEquality/vector.ml @@ -99,4 +99,7 @@ sig val to_sparse_list: t -> (int * num) list + (* Returns the part of the vector starting from index n*) + val starting_from_nth : int -> t -> t + end \ No newline at end of file