coveredddd

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

@@ -257,28 +257,27 @@ module ListMatrix: AbstractMatrix =
       | Some m -> let () = Printf.printf "After rref_matrix m, before removing zero rows:\n %s\n" (show m) in Some (remove_zero_rows m)
       | None -> let () = Printf.printf "No normalization for rref_matrix found" in None
 
-
     let delete_row_with_pivots row pivots m2 = 
       failwith "TODO"
 
-    (* Assumes that the first row of the matrix is already the pivot row fitting to the vector. *)
-    let rec is_linearly_independent_rref v m = 
-      match m with
-      | [] -> not @@ V.is_zero_vec v
-      | x::xs ->
+    let is_covered_by m1 m2 =
+      let rec is_linearly_independent_rref v m = 
         let pivot_opt = V.findi_val_opt ((<>:) A.zero) v in
         match pivot_opt with
         | None -> false (* When we found no pivot, the vector is already A.zero. *)
         | Some (pivot_id, pivot) ->
-          let new_v = V.map2_f_preserves_zero (fun v1 v2 -> v1 -: (pivot *: v2)) v x in
-          is_linearly_independent_rref new_v xs
-
-    let is_covered_by m1 m2 =
-      Printf.printf "Is m1 covered by m2?\n m1:\n%sm2:\n%s" (show m1) (show m2);
-      match normalize @@ append_matrices m2 m1 with
-      | None -> false
-      | Some m -> let m2' = remove_zero_rows m in List.for_all2 (fun x y -> V.equal x y) m2 m2'
-    (*let () = Printf.printf "Is m1 covered by m2?\n m1:\n%sm2:\n%s" (show m1) (show m2) in
+          let m' = List.drop_while (fun v2 -> 
+              match V.findi_val_opt ((<>:) A.zero) v2 with
+              | None -> true  (* In this case, m2 only has zero rows after that *)
+              | Some (idx', _) -> idx' < pivot_id
+            ) m in 
+          match m' with
+          | [] -> not @@ V.is_zero_vec v
+          | x::xs ->
+            let new_v = V.map2_f_preserves_zero (fun v1 v2 -> v1 -: (pivot *: v2)) v x in
+            is_linearly_independent_rref new_v m'
+      in
+      let () = Printf.printf "Is m1 covered by m2?\n m1:\n%sm2:\n%s" (show m1) (show m2) in
       if num_rows m1 > num_rows m2 then false else
       let rec is_covered_by_helper m1 m2 = 
         match m1 with 
@@ -288,15 +287,10 @@ module ListMatrix: AbstractMatrix =
           match first_non_zero with
           | None -> true  (* vs1 must also be zero-vectors because of rref *)
           | Some (idx, _) -> 
-            let m' = List.drop_while (fun v2 -> 
-                match V.findi_val_opt ((<>:) A.zero) v2 with
-                | None -> true  (* In this case, m2 only has zero rows after that *)
-                | Some (idx', _) -> idx' < idx
-              ) m2 in (* Only consider the part of m2 where the pivot is at a position useful for deleting first_non_zero of v1*)
-            let linearly_indep = is_linearly_independent_rref v1 m' in 
-            if linearly_indep then false else is_covered_by_helper vs1 m'
-      in is_covered_by_helper m1 m2*)
-
+            let linearly_indep = is_linearly_independent_rref v1 m2 in
+            if linearly_indep then false else is_covered_by_helper vs1 m2
+      in is_covered_by_helper m1 m2
+
     let is_covered_by m1 m2 = Timing.wrap "is_covered_by" (is_covered_by m1) m2
 
     let find_opt f m =

src/cdomains/affineEquality/sparseImplementation/sparseVector.ml

@@ -191,6 +191,7 @@ module SparseVector: AbstractVector =
         fst @@ List.find (fun (idx, value) -> f value) v.entries (* Here fst is the idx contained in the found tuple *)
 
     (* Returns optional of (index * value) where f value evaluated to true *)
+    (*Can be optimized, dont check every zero cell*)
     let findi_val_opt f v =
       let rec find_zero_or_val vec last_col_idx =
         match vec, last_col_idx with

tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml

@@ -243,6 +243,18 @@ let is_covered_big _ =
   let result = Matrix.is_covered_by m1 m2 in
   assert_bool "Matrix m1 is covered by m2, but was false" (result)
 
+let is_covered_big2 _ = 
+  let m1 = make_matrix_of_2d_list @@
+    [[int 1; int 0; int 0; int 0; int 0; int 1; int 0]
+     ] in
+
+  let m2 = make_matrix_of_2d_list @@
+    [[int 1; int 0; int 0; int 0; int 0; int 0; int 0];
+     [int 0; int 1; int 0; int 0; int 0; int 0; int 0];
+     [int 0; int 0; int 0; int 0; int 0; int 1; int 0]] in
+
+  let result = Matrix.is_covered_by m1 m2 in
+  assert_bool "Matrix m1 is covered by m2, but was false" (result)
 (**
    Normalization works on an empty matrix.
 *)
@@ -310,6 +322,8 @@ let tests =
     "does not change an empty matrix" >:: normalize_empty;
     "can correctly normalize a two column matrix" >:: normalize_two_columns;
     "can handle a rational solution" >:: int_domain_to_rational;
+    "m1 is covered by m2 with big matrix2" >:: is_covered_big2;
+
   ]
 
 let () = run_test_tt_main tests