From 70dbf4de31d5ca9e4e86a4e7a23116d23bf0fa82 Mon Sep 17 00:00:00 2001 From: CopperCableIsolator Date: Thu, 28 Nov 2024 15:15:17 +0100 Subject: [PATCH] exists, vector interface --- .../sparseImplementation/sparseVector.ml | 13 +++++++++---- src/cdomains/affineEquality/vector.ml | 2 ++ 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml index 685fcbd22d..9fffacb57d 100644 --- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml +++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml @@ -143,7 +143,7 @@ module SparseVector: AbstractVector = failwith "TODO" let map2_with f v v' = - failwith "TODO" + failwith "deprecated" let findi f v = failwith "TODO" @@ -173,9 +173,14 @@ module SparseVector: AbstractVector = {entries = entries'; len = v.len + v'.len} let exists f v = - failwith "TODO" - - let rev v = + let c = v.len in + let rec exists_aux at f v = + match v with + | [] -> if at = 0 then false else f A.zero + | (xi, xv)::xs -> if f xv then true else exists_aux (at - 1) f xs + in (exists_aux c f v.entries) + + let rev v = failwith "TODO" let rev_with v = diff --git a/src/cdomains/affineEquality/vector.ml b/src/cdomains/affineEquality/vector.ml index a673b820c7..ce7558c05a 100644 --- a/src/cdomains/affineEquality/vector.ml +++ b/src/cdomains/affineEquality/vector.ml @@ -18,6 +18,8 @@ sig val insert_val_at: int -> num -> t -> t + val map_preserve_zero: ((int * num) -> (int * num)) -> t -> t + val map2_preserve_zero: ((int * num) -> (int * num) -> (int * num)) -> t -> t -> t val apply_with_c: (num -> num -> num) -> num -> t -> t val apply_with_c_with: (num -> num -> num) -> num -> t -> unit