package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

include Colibri2_theories_LRA_stages_def.Interval_sig.S

include Colibri2_popop_lib.Popop_stdlib.Datatype

include Colibri2_popop_lib.Popop_stdlib.OrderedHashedType

type t

val equal : t -> t -> bool

val pp : t Colibri2_popop_lib.Pp.pp

val hash_fold_t : t Base.Hash.folder

module M : Colibri2_popop_lib.Map_intf.PMap with type key = t

module S : 
  Colibri2_popop_lib.Map_intf.Set
    with type 'a M.t = 'a M.t
     and type M.key = M.key

module H : Colibri2_popop_lib.Exthtbl.Hashtbl.S with type key = t

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 =

| Gt
| Lt
| Ge
| Le
| Eq
| 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 =

| Singleton of Colibri2_stdlib.Std.A.t
| Splitted of t * t
| NotSplitted

val split_heuristic : t -> split_heuristic

val absent : Colibri2_stdlib.Std.A.t -> t -> bool

val is_integer : t -> bool

val integers : t

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

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

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

val le : Colibri2_stdlib.Std.A.t -> 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

val get_convexe_hull : 
  t ->
  (Colibri2_stdlib.Std.A.t * Colibri2_theories_LRA_stages_def.Bound.t) option
  * (Colibri2_stdlib.Std.A.t * Colibri2_theories_LRA_stages_def.Bound.t) option

val from_convexe_hull : 
  ((Colibri2_stdlib.Std.A.t * Colibri2_theories_LRA_stages_def.Bound.t) option
   * (Colibri2_stdlib.Std.A.t * Colibri2_theories_LRA_stages_def.Bound.t)
       option) ->
  t