bugfix in add_empty_columns, behavious still differs from arraymatrix

Author: charlotte-brandt

src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml

@@ -39,7 +39,7 @@ module ArrayMatrix: AbstractMatrix =
     let copy m = Timing.wrap "copy" (copy) m
 
     let add_empty_columns m cols =
-      let () = Printf.printf "Before add_empty_columns m:\n%s\n" (show m) in
+      let () = Printf.printf "Before add_empty_columns m:\n%sindices: %s\n" (show m) (Array.fold_right (fun x s -> s ^ (Int.to_string x) ^ ",") cols "") in
       let nnc = Array.length cols in
       if is_empty m || nnc = 0 then m else
         let nr, nc = num_rows m, num_cols m in
@@ -82,7 +82,7 @@ module ArrayMatrix: AbstractMatrix =
              Array.blit m (n + 1) new_matrix n (num_rows new_matrix - n)); new_matrix
 
     let get_col m n =
-      let () = Printf.printf "get_col %i of m:\n%s\n%s\n" n (show m) (V.show (V.of_array @@ Array.init (Array.length m) (fun i -> m.(i).(n)))) in
+      (*let () = Printf.printf "get_col %i of m:\n%s\n%s\n" n (show m) (V.show (V.of_array @@ Array.init (Array.length m) (fun i -> m.(i).(n)))) in*)
       V.of_array @@ Array.init (Array.length m) (fun i -> m.(i).(n))
 
     let get_col m n = Timing.wrap "get_col" (get_col m) n
@@ -286,7 +286,7 @@ module ArrayMatrix: AbstractMatrix =
       match rref_vec_with m' v' with
       | Some res -> let () = Printf.printf "After rref_vec we have m:\n%s\n" (show res) in 
         Some (remove_zero_rows res)
-      | None -> None
+      | None -> let () = Printf.printf "After rref_vec there is no normalization\n" in None
 
     let rref_matrix_with m1 m2 =
       (*Similar to rref_vec_with but takes two matrices instead.*)

src/cdomains/affineEquality/arrayImplementation/arrayVector.ml

@@ -36,7 +36,7 @@ module ArrayVector: AbstractVector =
 
     let remove_at_indices v idx = failwith "TODO"
 
-    let insert_zero_at_indices v idx = failwith "TODO"
+    let insert_zero_at_indices v idx count = failwith "TODO"
 
     let set_nth_with v n new_val =
       if n >= Array.length v then failwith "n outside of Array range" else

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

@@ -39,18 +39,21 @@ module ListMatrix: AbstractMatrix =
       Timing.wrap "copy" (copy) m
 
     let add_empty_columns m cols = 
-      let () = Printf.printf "Before add_empty_columns m:\n%s\n" (show m) in
+      let () = Printf.printf "Before add_empty_columns m:\n%sindices: %s\n" (show m) (Array.fold_right (fun x s -> s ^ (Int.to_string x) ^ ",") cols "") in
       let cols = Array.to_list cols in 
       let sorted_cols = List.sort Stdlib.compare cols in
-      let rec count_sorted_occ acc cols last count = 
+      let rec count_sorted_occ acc cols last count =
         match cols with
-        | [] -> acc
-        | (x :: xs) when x = last -> count_sorted_occ acc xs x (count + 1)
-        | (x :: xs) -> count_sorted_occ ((last, count) :: acc) xs x 1
+        | [] -> if count > 0 then (last, count) :: acc else acc
+        | x :: xs when x = last -> count_sorted_occ acc xs x (count + 1)
+        | x :: xs -> let acc = if count > 0 then (last, count) :: acc else acc in
+          count_sorted_occ acc xs x 1      
       in
-      let occ_cols = count_sorted_occ [] sorted_cols (-1) 0 in
-      let () = Printf.printf "After add_empty_columns m:\n%s\n" (show (List.map (fun row -> V.insert_zero_at_indices row occ_cols) m)) in
-      List.map (fun row -> V.insert_zero_at_indices row occ_cols) m
+      let occ_cols = List.rev @@ count_sorted_occ [] sorted_cols 0 0 in
+      (*let () = Printf.printf "sorted cols is: %s\n" (List.fold_right (fun x s -> (Int.to_string x) ^ s) sorted_cols "") in 
+        let () = Printf.printf "sorted_occ is: %s\n" (List.fold_right (fun (i, count) s -> "(" ^ (Int.to_string i) ^ "," ^ (Int.to_string count) ^ ")" ^ s) occ_cols "") in*)
+      let () = Printf.printf "After add_empty_columns m:\n%s\n" (show (List.map (fun row -> V.insert_zero_at_indices row occ_cols (List.length cols)) m)) in
+      List.map (fun row -> V.insert_zero_at_indices row occ_cols (List.length cols)) m
 
     let add_empty_columns m cols =
       Timing.wrap "add_empty_cols" (add_empty_columns m) cols
@@ -68,7 +71,7 @@ module ListMatrix: AbstractMatrix =
       List.remove_at n m
 
     let get_col m n =
-      let () = Printf.printf "get_col %i of m:\n%s\n%s\n" n (show m) (V.show (V.of_list @@ List.map (fun row -> V.nth row n) m)) in
+      (*let () = Printf.printf "get_col %i of m:\n%s\n%s\n" n (show m) (V.show (V.of_list @@ List.map (fun row -> V.nth row n) m)) in*)
       V.of_list @@ List.map (fun row -> V.nth row n) m (* builds full col including zeros, maybe use sparselist instead? *)
 
     let get_col m n =
@@ -246,7 +249,7 @@ module ListMatrix: AbstractMatrix =
       match normalize @@ append_matrices m (init_with_vec v) with
       | Some res -> let () = Printf.printf "After rref_vec we have m:\n%s\n" (show res) in 
         Some (remove_zero_rows res) 
-      | None -> None
+      | None -> let () = Printf.printf "After rref_vec there is no normalization\n " in None
 
     (*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*)

src/cdomains/affineEquality/sparseImplementation/sparseVector.ml

@@ -80,7 +80,7 @@ module SparseVector: AbstractVector =
       in
       {entries = remove_indices_helper v.entries idx 0; len = v.len - List.length idx}
 
-    let insert_zero_at_indices v idx = 
+    let insert_zero_at_indices v idx count = 
       let rec add_indices_helper vec idx added_count = 
         match vec, idx with 
         | [], [] -> []
@@ -90,7 +90,7 @@ module SparseVector: AbstractVector =
         | ((col_idx, value) :: xs), ((i, count) :: ys) when i < col_idx -> (col_idx + added_count + count, value) :: add_indices_helper xs ys (added_count + count)
         | ((col_idx, value) :: xs), ((i, count) :: ys) -> (col_idx + added_count, value) :: add_indices_helper xs idx added_count
       in
-      {entries = add_indices_helper v.entries idx 0; len = v.len + List.length idx}
+      {entries = add_indices_helper v.entries idx 0; len = v.len + count}
 
     let set_nth v n num = (* TODO: Optimize! *)
       if n >= v.len then failwith "Out of bounds" 

src/cdomains/affineEquality/vector.ml

@@ -12,7 +12,7 @@ sig
 
   val remove_at_indices: t -> int list -> t
 
-  val insert_zero_at_indices: t -> (int * int) list -> t
+  val insert_zero_at_indices: t -> (int * int) list -> int -> t
 
   val set_nth: t -> int -> num ->  t