is_cons_vec

src/cdomains/affineEquality/arrayImplementation/arrayVector.ml

@@ -57,6 +57,8 @@ 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 nth = Array.get
 
     let map2i f v1 v2 =
@@ -104,29 +106,29 @@ module ArrayVector: AbstractVector =
 
 
     let find_opt f v =
-      failwith "TODO"
+      failwith "Never implemented!"
 
-    let map_f_preserves_zero f v = failwith "TODO"
-    let map2_f_preserves_zero f v1 v2 = failwith "TODO"
+    let map_f_preserves_zero f v = failwith "Never implemented!"
+    let map2_f_preserves_zero f v1 v2 = failwith "Never implemented!"
 
     let fold_left_f_preserves_zero f acc v =
-      failwith "TODO"
+      failwith "Never implemented!"
 
     let fold_left2_f_preserves_zero f acc v v' =
-      failwith "TODO"
+      failwith "Never implemented!"
 
     let findi_val_opt f v =
-      failwith "TODO"
+      failwith "Never implemented!"
 
     let exists2 f v1 v1 =
-      failwith "TODO / deprecated"
+      failwith "Never implemented!"
 
     let starting_from_nth n v =
-      failwith "TODO / deprecated"
+      failwith "Never implemented!"
 
     let find_first_non_zero v =
-      failwith "TODO"
+      failwith "Never implemented!"
 
     let apply_with_c_f_preserves_zero f c v =
-      failwith "TODO"
+      failwith "Never implemented!"
   end

src/cdomains/affineEquality/sparseImplementation/sparseVector.ml

@@ -149,6 +149,12 @@ module SparseVector: AbstractVector =
 
     let is_zero_vec v = (v.entries = [])
 
+    let is_const_vec v = 
+      match v.entries with 
+      | [] -> false
+      | (xi,xv)::[] -> if xi = v.len - 1 then false else true 
+      | _ -> false 
+
     let nth v n = (* Note: This exception HAS TO BE THROWN! It is expected by the domain *)
       if n >= v.len then raise (Invalid_argument "Cannot access vector element (out of bounds)")
       else

src/cdomains/affineEquality/vector.ml

@@ -34,6 +34,8 @@ sig
 
   val is_zero_vec: t -> bool
 
+  val is_const_vec: t -> bool
+
   val nth: t -> int -> num
 
   val length: t -> int

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -66,9 +66,8 @@ struct
     let open Apron.Texpr1 in
     let exception NotLinear in
     let zero_vec = Vector.zero_vec @@ Environment.size t.env + 1 in
-    let neg v = Vector.map Mpqf.neg v in
-    let is_const_vec v = Vector.compare_length_with (Vector.filteri (fun i x -> (*Inefficient*)
-        Vector.compare_length_with v (i + 1) > 0 && x <>: Mpqf.zero) v) 1 = 0
+    let neg v = Vector.map_f_preserves_zero Mpqf.neg v in
+    let is_const_vec = Vector.is_const_vec 
     in
     let rec convert_texpr = function
       (*If x is a constant, replace it with its const. val. immediately*)