Implement is_covered_by structure, but helper function still missing

src/cdomains/affineEquality/arrayImplementation/arrayVector.ml

@@ -126,4 +126,7 @@ module ArrayVector: AbstractVector =
     let findi_val_opt f v =
       failwith "TODO"
 
+    let exists2 f v1 v1 =
+      failwith "TODO / deprecated"
+
   end

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

@@ -129,7 +129,8 @@ module ListMatrix: AbstractMatrix =
       failwith "TODO"
 
     let get_pivot_positions m = 
-      failwith "TODO"
+      List.mapi (fun i row -> V.findi (fun z -> z =: A.one) row) m
+
 
     let sub_rows (minu : V.t) (subt : V.t) : V.t =
       V.map2_preserve_zero (-:) minu subt
@@ -197,9 +198,25 @@ module ListMatrix: AbstractMatrix =
     let rref_matrix m1 m2 =
       normalize @@ append_matrices m1 m2
 
-    let is_covered_by m1 m2 =
+
+    let delete_row_with_pivots row pivots m = 
       failwith "TODO"
 
+    let is_covered_by m1 m2 =
+      if num_rows m1 > num_rows m2 then false else
+        let pivots = get_pivot_positions m2 in (* TODO: Lazy? *)
+        try
+          let _ = List.map2i (fun i row1 row2 ->
+              if not @@ V.exists2 (<>:) row1 row2 
+              then V.zero_vec (V.length row1) else
+                let row1 = delete_row_with_pivots row1 pivots m2 in 
+                if V.nth row1 (V.length row1 - 1) <>: A.zero
+                then raise Stdlib.Exit 
+                else V.zero_vec (V.length row1)
+            ) m1 m2 in
+          true
+        with Stdlib.Exit -> false
+
     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

@@ -198,6 +198,7 @@ module SparseVector: AbstractVector =
       else
         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 evaluated to true *)
     let findi_val_opt f v =
       if f A.zero then  
         (
@@ -233,6 +234,9 @@ module SparseVector: AbstractVector =
         | (xi, xv)::xs -> if f xv then true else exists_aux (at - 1) f xs
       in (exists_aux c f v.entries)
 
+    let exists2 f v1 v2 =
+      failwith "TODO"
+
     let rev v = 
       let entries' = List.rev @@ List.map (fun (idx, value) -> (v.len - idx, value)) v.entries in 
       {entries = entries'; len = v.len}
@@ -254,6 +258,7 @@ module SparseVector: AbstractVector =
 
     let find2i f v v' = 
       failwith "TODO"
+
     let to_array v = 
       let vec = Array.make v.len A.zero in 
       List.iter (fun (idx, value) -> vec.(idx) <- value) v.entries;

src/cdomains/affineEquality/vector.ml

@@ -69,6 +69,8 @@ sig
 
   val exists: (num -> bool) -> t -> bool
 
+  val exists2: (num -> num -> bool) -> t -> t -> bool
+
   val rev: t -> t
 
   val rev_with: t -> unit