Implement zero preserving Array Vector functions by calling normal functions

Author: kadameit

src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml

@@ -318,7 +318,8 @@ module ArrayMatrix: AbstractMatrix =
     let is_covered_by m1 m2 =
       (*Performs a partial rref reduction to check if concatenating both matrices and afterwards normalizing them would yield a matrix <> m2 *)
       (*Both input matrices must be in rref form!*)
-      let () = Printf.printf "Is m1 covered by m2?\n m1:\n%sm2:\n%s" (show m1) (show m2) in
+      let () = Printf.printf "is_covered_by m1: \n%s " (show m1) in
+      let () = Printf.printf "is_covered_by m2 \n%s " (show m2) in
       if num_rows m1 > num_rows m2 then false else
         let p2 = lazy (get_pivot_positions m2) in
         try (

src/cdomains/affineEquality/arrayImplementation/arrayVector.ml

@@ -57,7 +57,9 @@ module ArrayVector: AbstractVector =
 
     let is_zero_vec v = not (Array.exists (fun x -> x <>: A.zero) v)
 
-    let is_const_vec v = failwith "Never implemented!"
+    let is_const_vec v =
+      compare_length_with (filteri (fun i x -> (*Inefficient*)
+        compare_length_with v (i + 1) > 0 && x <>: A.zero) v) 1 = 0
 
     let nth = Array.get
 
@@ -108,11 +110,17 @@ module ArrayVector: AbstractVector =
     let find_opt f v =
       failwith "Never implemented!"
 
-    let map_f_preserves_zero f v = failwith "Never implemented!"
-    let map2_f_preserves_zero f v1 v2 = failwith "Never implemented!"
+    let map_f_preserves_zero f v =
+      map f v
 
-    let mapi_f_preserves_zero f v = failwith "Never implemented!"
-    let map2i_f_preserves_zero f v v' = failwith "Never implemented!"
+    let map2_f_preserves_zero f v1 v2 =
+      map2 f v1 v2
+
+    let mapi_f_preserves_zero f v =
+      mapi f v
+
+    let map2i_f_preserves_zero f v v' =
+      map2i f v v'
 
     let fold_left_f_preserves_zero f acc v =
       failwith "Never implemented!"
@@ -133,5 +141,5 @@ module ArrayVector: AbstractVector =
       failwith "Never implemented!"
 
     let apply_with_c_f_preserves_zero f c v =
-      failwith "Never implemented!"
+      apply_with_c f c v
   end