builds now + reduce_col

src/cdomains/affineEquality/arrayImplementation/arrayVector.ml

@@ -111,4 +111,7 @@ module ArrayVector: AbstractVector =
 
     let find_opt f v =
       failwith "TODO"
+
+    let map_preserve_zero f v = failwith "TODO"
+    let map2_preserve_zero f v1 v2 = failwith "TODO"
   end

src/cdomains/affineEquality/sparseImplementation/sparseMatrix.ml

@@ -106,44 +106,28 @@ module ListMatrix: AbstractMatrix =
       failwith "deprecated"
 
     let reduce_col_with m j  = Timing.wrap "reduce_col_with" (reduce_col_with m) j
-    let reduce_col m j =
+    let reduce_col m j = 
       if is_empty m then m 
       else
         let rec find_pivot idx entries = (* Finds non-zero element in column j and returns pair of row idx and the pivot value *)
           match entries with
           | [] -> None
-          | row :: rest -> match (List.assoc_opt j row) with
-            | None -> find_pivot (idx - 1) rest
-            | Some value -> Some (idx, value)
+          | row :: rest -> let value = V.nth row j in 
+            if value =: A.zero then find_pivot (idx - 1) rest else Some (idx, value)
         in
-        match (find_pivot (num_rows m - 1) (List.rev m.entries)) with
+        match (find_pivot (num_rows m - 1) (List.rev m)) with
         | None -> m (* column is already filled with zeroes *)
         | Some (row_idx, pivot) -> 
-          let pivot_row = List.nth m.entries row_idx in
-          let entries' = 
-            List.mapi(fun idx row ->
-                if idx = row_idx then 
-                  [] 
-                else
-                  match (List.assoc_opt j row) with (* Find column element in row and, if it exists, subtract row *)
-                  | None -> row
-                  | Some row_value -> (let s = row_value /: pivot in
-                                       let rec merge acc piv_row cur_row = 
-                                         match piv_row, cur_row with 
-                                         | [], [] -> acc 
-                                         | [], (i, value) :: rest -> merge ((i, value) :: acc) piv_row rest
-                                         | (i, value) :: rest, [] -> let new_value = A.zero -: s *: value in merge ((i, new_value) :: acc) rest cur_row
-                                         | (i, piv_val) :: piv_rest, (j, cur_val) :: cur_rest -> 
-                                           if i = j then 
-                                             let new_value = cur_val -: s *: piv_val in merge ((i, new_value) :: acc) piv_rest cur_rest 
-                                           else if i < j then 
-                                             let new_value = A.zero -: s *: piv_val in merge ((i, new_value) :: acc) piv_rest cur_row
-                                           else 
-                                             merge ((j, cur_val) :: acc) piv_row cur_rest
-                                       in List.rev @@ merge [] pivot_row row)
-              ) m.entries
-          in 
-          {entries = entries'; column_count = m.column_count}
+          let pivot_row = List.nth m row_idx in
+          List.mapi (fun idx row ->
+              if idx = row_idx then 
+                V.zero_vec (num_cols m)
+              else
+                let row_value = V.nth row j in 
+                if row_value = A.zero then row
+                else (let s = row_value /: pivot in
+                      V.map2_preserve_zero (fun x y -> x -: s *: y) row pivot_row)            
+            ) m
 
     let del_col m j =
       if num_cols m = 1 then empty () 

src/cdomains/affineEquality/sparseImplementation/sparseVector.ml

@@ -18,8 +18,6 @@ module SparseVector: AbstractVector =
     }[@@deriving eq, ord, hash]
 
     let tV e l = {entries=e; len=l}
-    let show v = 
-      failwith "TODO"
 
     let keep_vals v n = 
       let rec keep_vals_vec v n =
@@ -91,8 +89,13 @@ module SparseVector: AbstractVector =
           ) [] (List.rev v.entries) in
         {entries = entries'; len = v.len + 1}
 
-    let map_preserve_zero f v = tV ((List.map f) v.entries) v.len
+    let map_preserve_zero f v = (* map for functions f such that f 0 = 0 since f won't be applied to zero values. See also map *)
+      let entries' = List.filter_map (
+          fun (idx, value) -> let new_val = f value in 
+            if new_val = A.zero then None else Some (idx, new_val)) v.entries in 
+      {entries = entries'; len = v.len}
 
+    (* map for functions f such that f 0 0 = 0 since f won't be applied to if both values are zero. See also map *)
     let map2_preserve_zero f v1 v2 = 
       let rec map2_nonzero_aux v1 v2 =
         match v1, v2 with 
@@ -225,4 +228,13 @@ module SparseVector: AbstractVector =
     let find_opt f v =
       failwith "TODO: Do we need this?"
 
+    let show v = 
+      let t = to_list v in 
+      let rec list_str l =
+        match l with
+        | [] -> "]"
+        | x :: xs -> (A.to_string x) ^" "^(list_str xs)
+      in
+      "["^list_str t^"\n"
+
   end