Skip to content

Commit

Permalink
Stdcompat and other fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
@bclement-ocp
bclement-ocp committed May 13, 2024
1 parent e25f82b commit f3c754c
Show file tree
Hide file tree
Showing 5 changed files with 32 additions and 17 deletions.
7 changes: 5 additions & 2 deletions src/lib/reasoners/intervals.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2024 --- OCamlPro SAS *)
(* Copyright (C) 2013-2023 --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand All @@ -19,6 +19,9 @@
(* *)
(* CNRS - INRIA - Universite Paris Sud *)
(* *)
(* Until 2013, some parts of this code were released under *)
(* the Apache Software License version 2.0. *)
(* *)
(* --------------------------------------------------------------- *)
(* *)
(* More details can be found in the directory licenses/ *)
Expand Down Expand Up @@ -1030,5 +1033,5 @@ module DebugExplanations : Explanations with type t = string list = struct
List.rev_append l1 l2 |> List.sort_uniq String.compare

let compare l1 l2 =
List.compare String.compare l1 l2
Stdcompat.List.compare String.compare l1 l2
end
13 changes: 8 additions & 5 deletions src/lib/reasoners/intervals.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2024 --- OCamlPro SAS *)
(* Copyright (C) 2013-2023 --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand All @@ -19,6 +19,9 @@
(* *)
(* CNRS - INRIA - Universite Paris Sud *)
(* *)
(* Until 2013, some parts of this code were released under *)
(* the Apache Software License version 2.0. *)
(* *)
(* --------------------------------------------------------------- *)
(* *)
(* More details can be found in the directory licenses/ *)
Expand Down Expand Up @@ -93,14 +96,14 @@ module Legacy : sig

val affine_scale : const:Numbers.Q.t -> coef:Numbers.Q.t -> t -> t
(** Perform an affine transformation on the given bounds.
Suposing input bounds (b1, b2), this will return
Supposing input bounds (b1, b2), this will return
(const + coef * b1, const + coef * b2).
This function is useful to avoid the incorrect roundings that
can take place when scaling down an integer range. *)

val pretty_print : Format.formatter -> t -> unit
val pretty_print : t Fmt.t

val print : Format.formatter -> t -> unit
val print : t Fmt.t

val finite_size : t -> Numbers.Q.t option

Expand Down Expand Up @@ -134,7 +137,7 @@ module Legacy : sig
val equal : t -> t -> bool

val pick : is_max:bool -> t -> Numbers.Q.t
(** [pick ~is_max t] returns an elements of the set of intervals [t]. If
(** [pick ~is_max t] returns an element of the union of intervals [t]. If
[is_max] is [true], we pick the largest element of [t], if it exists.
We look for the smallest element if [is_max] is [false]. *)

Expand Down
19 changes: 11 additions & 8 deletions src/lib/reasoners/intervals_core.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2024 --- OCamlPro SAS *)
(* Copyright (C) 2013-2023 --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand All @@ -19,6 +19,9 @@
(* *)
(* CNRS - INRIA - Universite Paris Sud *)
(* *)
(* Until 2013, some parts of this code were released under *)
(* the Apache Software License version 2.0. *)
(* *)
(* --------------------------------------------------------------- *)
(* *)
(* More details can be found in the directory licenses/ *)
Expand All @@ -30,16 +33,16 @@ open Intervals_intf
(** Pretty-printer for a bound when used as a lower bound. *)
let pp_lower_bound pp_a ppf lb =
match lb with
| Unbounded -> Format.fprintf ppf "]-oo"
| Open x -> Format.fprintf ppf "]%a" pp_a x
| Closed x -> Format.fprintf ppf "[%a" pp_a x
| Unbounded -> Fmt.pf ppf "]-oo"
| Open x -> Fmt.pf ppf "]%a" pp_a x
| Closed x -> Fmt.pf ppf "[%a" pp_a x

(** Pretty-printer for a bound when used as an upper bound. *)
let pp_upper_bound pp_a ppf ub =
match ub with
| Unbounded -> Format.fprintf ppf "+oo["
| Open x -> Format.fprintf ppf "%a[" pp_a x
| Closed x -> Format.fprintf ppf "%a]" pp_a x
| Unbounded -> Fmt.pf ppf "+oo["
| Open x -> Fmt.pf ppf "%a[" pp_a x
| Closed x -> Fmt.pf ppf "%a]" pp_a x

module EqLtLeNotations(OT : OrderedType) = struct
(** This module contains convenient redefinitions of [=], [<], [<=], [min] and
Expand All @@ -64,7 +67,7 @@ module Interval(OT : OrderedType) = struct
type t = OT.t interval

let pp ppf i =
Format.fprintf ppf "@[%a;@ %a@]"
Fmt.pf ppf "@[%a;@ %a@]"
(pp_lower_bound OT.pp_finite) (OT.view i.lb)
(pp_upper_bound OT.pp_finite) (OT.view i.ub)

Expand Down
5 changes: 4 additions & 1 deletion src/lib/reasoners/intervals_core.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2024 --- OCamlPro SAS *)
(* Copyright (C) 2013-2023 --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand All @@ -19,6 +19,9 @@
(* *)
(* CNRS - INRIA - Universite Paris Sud *)
(* *)
(* Until 2013, some parts of this code were released under *)
(* the Apache Software License version 2.0. *)
(* *)
(* --------------------------------------------------------------- *)
(* *)
(* More details can be found in the directory licenses/ *)
Expand Down
5 changes: 4 additions & 1 deletion src/lib/reasoners/intervals_intf.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2024 --- OCamlPro SAS *)
(* Copyright (C) 2013-2023 --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand All @@ -19,6 +19,9 @@
(* *)
(* CNRS - INRIA - Universite Paris Sud *)
(* *)
(* Until 2013, some parts of this code were released under *)
(* the Apache Software License version 2.0. *)
(* *)
(* --------------------------------------------------------------- *)
(* *)
(* More details can be found in the directory licenses/ *)
Expand Down

0 comments on commit f3c754c

Please sign in to comment.