findi_f_false_at_zero

src/cdomains/affineEquality/sparseImplementation/sparseVector.ml

@@ -252,7 +252,7 @@ module SparseVector: AbstractVector =
 
     let map2_f_preserves_zero f v1 v2 = Timing.wrap "map2_f_preserves_zero" (map2_f_preserves_zero f v1) v2
 
-    let map2i f v1 v2 = (* TODO: optimize! *)
+    let map2i f v1 v2 = (*might more memory efficient, but definitly not faster (asymptotically)*)
       if v1.len <> v2.len then raise (Invalid_argument "Unequal lengths") else
         (*of_list (List.map2i f (to_list v) (to_list v'))*)
         let f_rem_zero idx acc e1 e2 =
@@ -326,9 +326,24 @@ module SparseVector: AbstractVector =
       let entries' = List.rev @@ List.map (fun (idx, value) -> (v.len - 1 - idx, value)) v.entries in 
       {entries = entries'; len = v.len}
 
-    let find2i f v v' = (* TODO: optimize! *) (*"Franzisco should do this!":~Franzisco*)
+    let find2i f v v' =
       fst @@ List.findi (fun _ (val1, val2) -> (uncurry f) (val1, val2)) (List.combine (to_list v) (to_list v'))
 
+    let find2i_f_false_at_zero f v v' = (*Very welcome to change the name*)
+      let rec aux v1 v2 =
+        match v1, v2 with 
+        | [], [] -> raise Not_found
+        | [], (yidx, yval)::ys -> if f A.zero yval then yidx else aux [] ys
+        | (xidx, xval)::xs, [] -> if f xval A.zero then xidx else aux xs []
+        | (xidx, xval)::xs, (yidx, yval)::ys -> 
+          match xidx - yidx with
+          | d when d < 0 -> if f xval A.zero then xidx else aux xs v2
+          | d when d > 0 -> if f A.zero yval then yidx else aux v1 ys
+          | _            -> if f xval yval then xidx else aux xs ys
+      in
+      if v.len <> v'.len then raise (Invalid_argument "Unequal lengths") else 
+        aux v.entries v'.entries
+
     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

@@ -53,6 +53,8 @@ sig
 
   val find2i: (num -> num -> bool) -> t -> t -> int
 
+  val find2i_f_false_at_zero: (num -> num -> bool) -> t -> t -> int
+
   (* Returns optional tuple of position and value which was found*)
   val findi_val_opt: (num -> bool) ->  t -> (int * num) Option.t
 

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -297,7 +297,7 @@ struct
             (
               let col_a = Vector.rev col_a in
               let col_b = Vector.rev col_b in
-              let i = Vector.find2i (<>:) col_a col_b in
+              let i = Vector.find2i_f_false_at_zero (<>:) col_a col_b in
               let (x, y) = Vector.nth col_a i, Vector.nth col_b i in
               let r, diff = Vector.length col_a - (i + 1), x -: y  in
               let a_r, b_r = Matrix.get_row a r, Matrix.get_row b r in