package colibri2

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
include Colibri2_theories_LRA_stages_def.Interval_sig.S
include Colibri2_popop_lib.Popop_stdlib.Datatype
val hash_fold_t : t Base.Hash.folder
module S : Colibri2_popop_lib.Map_intf.Set with type 'a M.t = 'a M.t and type M.key = M.key
include Base.Hashtbl.Key.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
val sexp_of_t : t -> Sexplib0.Sexp.t
val hash : t -> int
val is_distinct : t -> t -> bool
type is_comparable =
  1. | Gt
  2. | Lt
  3. | Ge
  4. | Le
  5. | Eq
  6. | Uncomparable
val is_comparable : t -> t -> is_comparable
val is_included : t -> t -> bool
val mult_cst : Colibri2_stdlib.Std.A.t -> t -> t
val add_cst : Colibri2_stdlib.Std.A.t -> t -> t
val add : t -> t -> t
val mul : t -> t -> t
val div : t -> t -> t
val inv : t -> t
val minus : t -> t -> t
val neg : t -> t
val floor : t -> t
val ceil : t -> t
val truncate : t -> t
val relu : t -> t
val mem : Colibri2_stdlib.Std.A.t -> t -> bool
val singleton : Colibri2_stdlib.Std.A.t -> t

from A.t

val is_singleton : t -> Colibri2_stdlib.Std.A.t option
val except : t -> Colibri2_stdlib.Std.A.t -> t option
type split_heuristic =
  1. | Singleton of Colibri2_stdlib.Std.A.t
  2. | Splitted of t * t
  3. | NotSplitted
val split_heuristic : t -> split_heuristic
val absent : Colibri2_stdlib.Std.A.t -> t -> bool
val is_integer : t -> bool
val integers : t

> q, >= q, < q, <= q

val le' : t -> t
val lt' : t -> t
val ge' : t -> t
val gt' : t -> t
val union : t -> t -> t

union set

val inter : t -> t -> t option

intersection set. if the two arguments are equals, return the second

val zero : t
val reals : t
val is_reals : t -> bool

R

val choose : t -> Colibri2_stdlib.Std.A.t

Nothing smart in this choosing

val invariant : t -> bool
module Union : sig ... end
val get_union : t -> Union.t
val reduce_integers : t -> t option
OCaml

Innovation. Community. Security.