@@ -555,26 +555,30 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct
555555 let to_int (x1 , x2 ) =
556556 if Ints_t. equal x1 x2 then Some x1 else None
557557
558+ let find_thresholds lower_or_upper =
559+ let ts = if get_interval_threshold_widening_constants () = " comparisons" then lower_or_upper else WideningThresholds. thresholds in
560+ ResettableLazy. force ts
561+
558562 let upper_threshold u max_ik =
559- let ts = if get_interval_threshold_widening_constants () = " comparisons " then WideningThresholds. upper_thresholds else WideningThresholds. thresholds in
563+ let ts = find_thresholds WideningThresholds. upper_thresholds in
560564 let u = Ints_t. to_bigint u in
561565 let max_ik' = Ints_t. to_bigint max_ik in
562- let t = WideningThresholds.Thresholds. find_first_opt (fun x -> Z. compare u x < = 0 && Z. compare x max_ik' < = 0 ) ( ResettableLazy. force ts) in
566+ let t = WideningThresholds.Thresholds. find_first_opt (fun x -> Z. compare u x < = 0 && Z. compare x max_ik' < = 0 ) ts in
563567 BatOption. map_default Ints_t. of_bigint max_ik t
564568 let lower_threshold l min_ik =
565- let ts = if get_interval_threshold_widening_constants () = " comparisons " then WideningThresholds. lower_thresholds else WideningThresholds. thresholds in
569+ let ts = find_thresholds WideningThresholds. lower_thresholds in
566570 let l = Ints_t. to_bigint l in
567571 let min_ik' = Ints_t. to_bigint min_ik in
568- let t = WideningThresholds.Thresholds. find_last_opt (fun x -> Z. compare l x > = 0 && Z. compare x min_ik' > = 0 ) ( ResettableLazy. force ts) in
572+ let t = WideningThresholds.Thresholds. find_last_opt (fun x -> Z. compare l x > = 0 && Z. compare x min_ik' > = 0 ) ts in
569573 BatOption. map_default Ints_t. of_bigint min_ik t
570- let is_upper_threshold u =
571- let ts = if get_interval_threshold_widening_constants () = " comparisons " then WideningThresholds. upper_thresholds else WideningThresholds. thresholds in
572- let u = Ints_t. to_bigint u in
573- WideningThresholds.Thresholds. exists ( Z. equal u) ( ResettableLazy. force ts)
574- let is_lower_threshold l =
575- let ts = if get_interval_threshold_widening_constants () = " comparisons " then WideningThresholds. lower_thresholds else WideningThresholds. thresholds in
576- let l = Ints_t. to_bigint l in
577- WideningThresholds.Thresholds. exists ( Z. equal l) ( ResettableLazy. force ts)
574+
575+ let is_threshold t ts =
576+ let ts = find_thresholds ts in
577+ let t = Ints_t. to_bigint t in
578+ WideningThresholds.Thresholds. exists ( Z. equal t) ts
579+
580+ let is_upper_threshold u = is_threshold u WideningThresholds. upper_thresholds
581+ let is_lower_threshold l = is_threshold l WideningThresholds. lower_thresholds
578582end
579583
580584module IntInvariant =
0 commit comments