Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
  • Loading branch information
charlotte-brandt committed Dec 17, 2024
2 parents fd5689a + 1ea8040 commit 335d4ea
Show file tree
Hide file tree
Showing 6 changed files with 3 additions and 111 deletions.
17 changes: 3 additions & 14 deletions src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml
Original file line number Diff line number Diff line change
Expand Up @@ -265,13 +265,13 @@ module ArrayMatrix: AbstractMatrix =
(*m must be in rref form and contain the same num of cols as v*)
(*If m is empty then v is simply normalized and returned*)
(*let v = V.to_array v in
if is_empty m then
if is_empty m then
match Array.findi (fun x -> x <>: A.zero) v with
| exception Not_found -> None
| i -> if i = Array.length v - 1 then None else
let v_i = v.(i) in
Array.iteri (fun j x -> v.(j) <- x /: v_i) v; Some (init_with_vec @@ V.of_array v)
else
else
let pivot_elements = get_pivot_positions m in
rref_vec_helper m pivot_elements v*)
normalize @@ append_row m v
Expand Down Expand Up @@ -355,10 +355,7 @@ module ArrayMatrix: AbstractMatrix =
m.(i) <- V.to_array @@ f (V.of_array m.(i)) (V.nth v i)
done

(* Deprecated
let map2 f m v =
let f' x y = V.to_array @@ f (V.of_array x) y in Array.map2 f' m (V.to_array v)
*)
let map2_with f m v = Timing.wrap "map2_with" (map2_with f m) v

let map2 f m v =
let () = Printf.printf "Before map2 we have m:\n%s\n" (show m) in
Expand All @@ -367,8 +364,6 @@ module ArrayMatrix: AbstractMatrix =
let () = Printf.printf "After map2 we have m:\n%s\n" (show m') in
m'

let map2_with f m v = Timing.wrap "map2_with" (map2_with f m) v

let map2i_with f m v =
if num_rows m = V.length v then
Array.iter2i (fun i x y -> m.(i) <- V.to_array @@ f i (V.of_array x) y) m (V.to_array v)
Expand All @@ -379,12 +374,6 @@ module ArrayMatrix: AbstractMatrix =

let map2i_with f m v = Timing.wrap "map2i_with" (map2i_with f m) v

(* Deprecated
let map2i f m v =
let f' x (i,y) = V.to_array @@ f i (V.of_array x) y in
let range_array = Array.init (V.length v) Fun.id in
Array.map2 f' m (Array.combine range_array (V.to_array v))
*)
let map2i f m v =
let () = Printf.printf "Before map2i m:\n%sv:%s\n" (show m) (V.show v) in
let m' = copy m in
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -63,23 +63,15 @@ module ArrayVector: AbstractVector =
let f' i = uncurry (f i) in
Array.mapi f' (Array.combine v1 v2) (* TODO: iter2i? *)

let map2i_with f v1 v2 = Array.iter2i (fun i x y -> v1.(i) <- f i x y) v1 v2

let find2i f v1 v2 =
Array.findi (uncurry f) (Array.combine v1 v2) (* TODO: iter2i? *)

let to_array v = v

let of_array v = v

let apply_with_c_with f c v = Array.modify (fun x -> f x c) v

let rev_with v = Array.rev_in_place v

let rev v = Array.rev v

let map_with f v = Array.modify f v

let map f v = Array.map f v

let map2_with f v1 v2 = Array.iter2i (fun i x y -> v1.(i) <- f x y) v1 v2
Expand Down
14 changes: 0 additions & 14 deletions src/cdomains/affineEquality/matrix.ml
Original file line number Diff line number Diff line change
Expand Up @@ -33,36 +33,22 @@ sig

val reduce_col: t -> int -> t

val reduce_col_with: t -> int -> unit

val normalize: t -> t Option.t (*Gauss-Jordan Elimination to get matrix in reduced row echelon form (rref) + deletion of zero rows. None matrix has no solution*)

val normalize_with: t -> bool

val rref_vec: t -> vec -> t Option.t (* added to remove side effects in affineEqualityDomain*)

val rref_vec_with: t -> vec -> t Option.t

val rref_matrix: t -> t -> t Option.t (* this as well *)

val rref_matrix_with: t -> t -> t Option.t

val find_opt: (vec -> bool) -> t -> vec option

val map2: (vec -> num -> vec) -> t -> vec -> t

val map2_with: (vec -> num -> vec) -> t -> vec -> unit

val map2: (vec -> num -> vec) -> t -> vec -> t (* why is this here twice??*)

val map2i: (int -> vec-> num -> vec) -> t -> vec -> t

val map2i_with: (int -> vec -> num -> vec) -> t -> vec -> unit

val set_col: t -> vec -> int -> t

val set_col_with: t -> vec -> int -> t

val init_with_vec: vec -> t

val remove_zero_rows: t -> t
Expand Down
32 changes: 0 additions & 32 deletions src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
Original file line number Diff line number Diff line change
Expand Up @@ -299,36 +299,4 @@ module ListMatrix: AbstractMatrix =
let map2 f m v =
let vector_length = V.length v in
List.mapi (fun index row -> if index < vector_length then f row (V.nth v index) else row ) m


(* ------------------------- Deprecated ------------------------*)

let rref_vec_with m v =
(*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.*)
(*m must be in rref form and contain the same num of cols as v*)
(*If m is empty then v is simply normalized and returned*)
failwith "deprecated"

let rref_with m =
failwith "deprecated"

let reduce_col_with m j =
failwith "deprecated"

let normalize_with m =
failwith "deprecated"

let set_col_with m new_col n =
failwith "deprecated"

let map2_with f m v =
failwith "deprecated"

let map2i_with f m v =
failwith "deprecated"

let rref_matrix_with m1 m2 =
(*Similar to rref_vec_with but takes two matrices instead.*)
(*ToDo Could become inefficient for large matrices since pivot_elements are always recalculated + many row additions*)
failwith "deprecated"
end
25 changes: 0 additions & 25 deletions src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
Original file line number Diff line number Diff line change
Expand Up @@ -270,29 +270,4 @@ module SparseVector: AbstractVector =
| x :: xs -> (A.to_string x) ^ " " ^ (list_str xs)
in
"["^list_str t^"\n"

(* ------------------- Deprecated ------------------- *)
let mapi_with f v =
failwith "mapi_with deprecated"

let map2i_with f v v' =
failwith "map2i_with deprecated"


let rev_with v =
failwith "rev_with deprecated"

let map_with f v =
failwith "map_with deprecated"


let map2_with f v v' =
failwith "map2_with deprecated"

let apply_with_c_with f m v =
failwith "apply_with_c_with deprecated"

let set_nth_with f n num = (
failwith "set_nth_with deprecated")

end
18 changes: 0 additions & 18 deletions src/cdomains/affineEquality/vector.ml
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,6 @@ sig

val set_nth: t -> int -> num -> t

val set_nth_with: t -> int -> num -> unit

val insert_val_at: int -> num -> t -> t

val map_f_preserves_zero: (num -> num) -> t -> t
Expand All @@ -32,8 +30,6 @@ sig

val apply_with_c_f_preserves_zero: (num -> num -> num) -> num -> t -> t

val apply_with_c_with: (num -> num -> num) -> num -> t -> unit

val zero_vec: int -> t

val is_zero_vec: t -> bool
Expand All @@ -44,8 +40,6 @@ sig

val map2: (num -> num -> num) -> t -> t -> t

val map2_with: (num -> num -> num) -> t -> t -> unit

val findi: (num -> bool) -> t -> int

(* Returns optional tuple of position and value which was found*)
Expand All @@ -57,8 +51,6 @@ sig

val map: (num -> num) -> t -> t

val map_with: (num -> num) -> t -> unit

val map: (num -> num) -> t -> t

val compare_length_with: t -> int -> int
Expand All @@ -74,21 +66,12 @@ sig
val exists: (num -> bool) -> t -> bool

val exists2: (num -> num -> bool) -> t -> t -> bool

val rev: t -> t

val rev_with: t -> unit

val rev: t -> t

val map2i: (int -> num -> num -> num) -> t -> t -> t

val map2i_with: (int -> num -> num -> num) -> t -> t -> unit

val mapi: (int -> num -> num) -> t -> t

val mapi_with: (int -> num -> num) -> t -> unit

val mapi: (int -> num -> num) -> t -> t

val find2i: (num -> num -> bool) -> t -> t -> int
Expand All @@ -105,5 +88,4 @@ sig

(* Returns the part of the vector starting from index n*)
val starting_from_nth : int -> t -> t

end

0 comments on commit 335d4ea

Please sign in to comment.