From 3b49ba558fe548af158450d4c8f755a0dcca8f1f Mon Sep 17 00:00:00 2001
From: Kevin Adameit <kevin.adameit@icloud.com>
Date: Sat, 21 Dec 2024 10:04:28 +0100
Subject: [PATCH] Organize Vector and Matrix interface

---
 .../apron/affineEqualityAnalysis.apron.ml     |  1 +
 src/cdomains/affineEquality/matrix.ml         | 48 ++++++-----
 .../sparseImplementation/listMatrix.ml        |  3 +
 .../sparseImplementation/sparseVector.ml      |  1 -
 src/cdomains/affineEquality/vector.ml         | 81 +++++++++----------
 5 files changed, 66 insertions(+), 68 deletions(-)

diff --git a/src/analyses/apron/affineEqualityAnalysis.apron.ml b/src/analyses/apron/affineEqualityAnalysis.apron.ml
index 80d3b32874..fcb12606da 100644
--- a/src/analyses/apron/affineEqualityAnalysis.apron.ml
+++ b/src/analyses/apron/affineEqualityAnalysis.apron.ml
@@ -15,6 +15,7 @@ include RelationAnalysis
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
     let module AD = AffineEqualityDomain.D2 (SparseVector) (ListMatrix) in
+    let module AD_A = AffineEqualityDomain.D2 (ArrayVector) (ArrayMatrix) in (* TODO: Remove this! Just to suppress warning *)
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct
diff --git a/src/cdomains/affineEquality/matrix.ml b/src/cdomains/affineEquality/matrix.ml
index 0dffe8c44e..b3433ee899 100644
--- a/src/cdomains/affineEquality/matrix.ml
+++ b/src/cdomains/affineEquality/matrix.ml
@@ -5,58 +5,56 @@ sig
   type vec
   type t [@@deriving eq, ord, hash]
 
+  val show: t -> string
+
+  val copy: t -> t
+
   val empty: unit -> t (* TODO: needs unit? *)
 
   val is_empty: t -> bool
 
-  val show: t -> string
+  val num_rows: t -> int
 
-  val add_empty_columns: t -> int array -> t
+  val num_cols: t -> int
+
+  val init_with_vec: vec -> t
 
   val append_row: t -> vec -> t
 
   val get_row: t -> int -> vec
 
-  val del_col: t -> int -> t
-
-  val del_cols: t -> int array -> t
-
   val remove_row: t -> int -> t
 
-  val get_col: t -> int -> vec
-
-  val append_matrices: t -> t -> t
-
-  val num_rows: t -> int
+  val remove_zero_rows: t -> t
 
-  val num_cols: t -> int
+  val swap_rows: t -> int -> int -> t
 
-  val reduce_col: t -> int -> t
+  val add_empty_columns: t -> int array -> t
 
-  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 get_col: t -> int -> vec
 
-  val rref_vec: t -> vec -> t Option.t (* added to remove side effects in affineEqualityDomain*)
+  val set_col: t -> vec -> int -> t
 
-  val rref_matrix: t -> t -> t Option.t (* this as well *)
+  val del_col: t -> int -> t
 
-  val find_opt: (vec -> bool) -> t -> vec option
+  val del_cols: t -> int array -> t
 
   val map2: (vec -> num -> vec) -> t -> vec -> t
 
-  val map2: (vec -> num -> vec) -> t -> vec -> t (* why is this here twice??*)
-
   val map2i: (int -> vec-> num -> vec) -> t -> vec -> t
 
-  val set_col: t -> vec -> int -> t
+  val find_opt: (vec -> bool) -> t -> vec option
 
-  val init_with_vec: vec -> t
+  val append_matrices: t -> t -> t
 
-  val remove_zero_rows: t -> t
+  val reduce_col: t -> int -> t
 
-  val is_covered_by: t -> t -> bool
+  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 copy: t -> t
+  val rref_vec: t -> vec -> t Option.t
 
-  val swap_rows: t -> int -> int -> t
+  val rref_matrix: t -> t -> t Option.t
+
+  val is_covered_by: t -> t -> bool
 
 end
\ No newline at end of file
diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
index 8d80aae50a..e8bc108d91 100644
--- a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
+++ b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
@@ -221,6 +221,9 @@ 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
 
+    (* TODO: Remove this! Just to suppress warning *)
+    let () = assert_rref (empty ())
+
     (* 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
diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
index aab73454a4..c300b22ceb 100644
--- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
+++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
@@ -3,7 +3,6 @@ open RatOps
 open ConvenienceOps
 
 open BatList
-open BatArray
 open Batteries
 
 module List = BatList
diff --git a/src/cdomains/affineEquality/vector.ml b/src/cdomains/affineEquality/vector.ml
index 956c6aa1ea..799df35c0e 100644
--- a/src/cdomains/affineEquality/vector.ml
+++ b/src/cdomains/affineEquality/vector.ml
@@ -6,29 +6,23 @@ sig
 
   val show: t -> string
 
-  val keep_vals: t -> int ->  t
-
-  val remove_nth: t -> int ->  t
-
-  val remove_at_indices: t -> int list -> t
-
-  val insert_zero_at_indices: t -> (int * int) list -> int -> t
+  val copy: t -> t
 
-  val set_nth: t -> int -> num ->  t
+  val of_list: num list -> t
 
-  val insert_val_at: int -> num ->  t ->  t
+  val of_array: num array -> t
 
-  val map_f_preserves_zero: (num -> num) -> t -> t
+  val of_sparse_list: int -> (int * num) list -> t
 
-  val map2_f_preserves_zero: (num -> num -> num) -> t ->  t -> t
+  val to_list: t -> num list
 
-  val fold_left_f_preserves_zero: ('acc -> num -> 'acc) -> 'acc -> t -> 'acc
+  val to_array: t -> num array
 
-  val fold_left2_f_preserves_zero: ('acc -> num -> num -> 'acc) -> 'acc -> t -> t -> 'acc
+  val to_sparse_list: t -> (int * num) list
 
-  val apply_with_c: (num -> num -> num) -> num ->  t ->  t
+  val length: t -> int
 
-  val apply_with_c_f_preserves_zero: (num -> num -> num) -> num ->  t ->  t
+  val compare_length_with: t -> int -> int
 
   val zero_vec: int -> t
 
@@ -38,60 +32,63 @@ sig
 
   val nth: t -> int -> num
 
-  val length: t -> int
-
-  val map2: (num -> num -> num) -> t -> t -> t
+  val set_nth: t -> int -> num ->  t
 
-  val findi: (num -> bool) ->  t -> int
+  val insert_val_at: int -> num ->  t ->  t
 
-  (* Returns optional tuple of position and value which was found*)
-  val findi_val_opt: (num -> bool) ->  t -> (int * num) Option.t
+  val insert_zero_at_indices: t -> (int * int) list -> int -> t
 
-  val find_first_non_zero : t -> (int * num) option
+  val remove_nth: t -> int ->  t
 
-  val find_opt: (num -> bool) -> t -> num Option.t
+  val remove_at_indices: t -> int list -> t
 
-  val map: (num -> num) -> t -> t
+  val keep_vals: t -> int ->  t
 
-  val map: (num -> num) -> t -> t
+  (* Returns the part of the vector starting from index n*)
+  val starting_from_nth : int -> t -> t
 
-  val compare_length_with: t -> int -> int
+  val find_opt: (num -> bool) -> t -> num Option.t
 
-  val of_list: num list -> t
+  val findi: (num -> bool) ->  t -> int
 
-  val to_list: t -> num list
+  val find2i: (num -> num -> bool) -> t -> t -> int
 
-  val filteri: (int -> num -> bool) -> t -> t
+  (* Returns optional tuple of position and value which was found*)
+  val findi_val_opt: (num -> bool) ->  t -> (int * num) Option.t
 
-  val append: t -> t -> t
+  val find_first_non_zero : t -> (int * num) option
 
   val exists: (num -> bool) -> t -> bool
 
   val exists2: (num -> num -> bool) -> t -> t -> bool
-  val rev: t -> t
 
-  val map2i: (int -> num -> num -> num) -> t -> t -> t
+  val filteri: (int -> num -> bool) -> t -> t
 
-  val map2i_f_preserves_zero: (int -> num -> num -> num) -> t -> t -> t
+  val map: (num -> num) -> t -> t
+
+  val map_f_preserves_zero: (num -> num) -> t -> t
 
   val mapi: (int -> num -> num) -> t -> t
 
   val mapi_f_preserves_zero: (int -> num -> num) -> t -> t
 
-  val mapi: (int -> num -> num) -> t -> t
+  val map2: (num -> num -> num) -> t -> t -> t
 
-  val find2i: (num -> num -> bool) -> t -> t -> int
+  val map2_f_preserves_zero: (num -> num -> num) -> t ->  t -> t
 
-  val to_array: t -> num array
+  val map2i: (int -> num -> num -> num) -> t -> t -> t
 
-  val of_array: num array -> t
+  val map2i_f_preserves_zero: (int -> num -> num -> num) -> t -> t -> t
 
-  val copy: t -> t
+  val fold_left_f_preserves_zero: ('acc -> num -> 'acc) -> 'acc -> t -> 'acc
 
-  val of_sparse_list: int -> (int * num) list -> t
+  val fold_left2_f_preserves_zero: ('acc -> num -> num -> 'acc) -> 'acc -> t -> t -> 'acc
 
-  val to_sparse_list: t -> (int * num) list
+  val apply_with_c: (num -> num -> num) -> num ->  t ->  t
 
-  (* Returns the part of the vector starting from index n*)
-  val starting_from_nth : int -> t -> t
+  val apply_with_c_f_preserves_zero: (num -> num -> num) -> num ->  t ->  t
+
+  val rev: t -> t
+
+  val append: t -> t -> t
 end
\ No newline at end of file