From b15b9d2dfec55c8ce7df595ce6c55468ab4a2c99 Mon Sep 17 00:00:00 2001 From: CopperCableIsolator Date: Thu, 12 Dec 2024 15:15:51 +0100 Subject: [PATCH] small tweak in findi_val_opt, could be even a tini tiny bit faster but not much --- .../affineEquality/sparseImplementation/sparseVector.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml index 2fc3e16e5f..1b31bfe2c7 100644 --- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml +++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml @@ -194,10 +194,11 @@ module SparseVector: AbstractVector = (*Can be optimized, dont check every zero cell*) let findi_val_opt f v = let rec find_zero_or_val vec last_col_idx = - match vec, last_col_idx with - | [], _ -> if f A.zero && v.len <> last_col_idx + 1 then Some (last_col_idx + 1, A.zero) else None - | (idx, value) :: xs, i -> - if f A.zero && idx <> last_col_idx + 1 then Some (last_col_idx + 1, A.zero) + let f0 = f A.zero in + match vec with + | [] -> if f0 && v.len <> last_col_idx + 1 then Some (last_col_idx + 1, A.zero) else None + | (idx, value) :: xs -> + if f0 && idx <> last_col_idx + 1 then Some (last_col_idx + 1, A.zero) else if f value then Some (idx, value) else find_zero_or_val xs idx in find_zero_or_val v.entries (-1)